|
%%-------------------** First Isomorphism Theorem **-------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%---------------------------------------------------------------------
homomorphism_lemmas[T1: TYPE, *: [T1,T1 -> T1], one1: T1,
T2: TYPE, o: [T2,T2 -> T2], one2: T2]: THEORY
BEGIN
ASSUMING IMPORTING algebra@group_def
T1_is_group: ASSUMPTION group?[T1,*,one1](fullset[T1])
T2_is_group: ASSUMPTION group?[T2,o,one2](fullset[T2])
ENDASSUMING
IMPORTING products_subgroups,
algebra@homomorphisms,
algebra@factor_groups
G: VAR group[T1,*,one1]
GP: VAR group[T2,o,one2]
x,y,z: VAR T1
natural_homo: LEMMA FORALL (K: normal_subgroup(G)):
EXISTS (pi: [(G) -> (G/K)]):
pi = (LAMBDA (x:(G)): *[T1, *, one1](x, K)) AND
homomorphism?(G,G/K,pi) AND
surjective?(pi) AND
K = kernel(G,G/K)(pi)
homo_inv: LEMMA FORALL (phi: homomorphism(G,GP), x: (G)):
phi(inv[T1, *, one1](x)) = inv[T2, o, one2](phi(x))
kernel_normal: LEMMA FORALL (phi: homomorphism(G,GP)):
LET K = kernel(G,GP)(phi) IN
normal_subgroup?(K, G)
homo_image: LEMMA FORALL (phi: homomorphism(G,GP),H: subgroup(G)):
subgroup?[T2, o, one2](image(phi, H), GP)
homo_image_normal: LEMMA FORALL (phi: homomorphism(G,GP),H: normal_subgroup(G)):
surjective?(phi) IMPLIES normal_subgroup?[T2, o, one2](image(phi, H), GP)
homo_inv_image: LEMMA FORALL (phi: homomorphism(G,GP),K: subgroup(GP)):
subgroup?[T1, *, one1](inverse_image(phi, K), G)
homo_inv_image_normal: LEMMA FORALL (phi: homomorphism(G,GP),K: normal_subgroup(GP)):
normal_subgroup?[T1, *, one1](inverse_image(phi, K), G)
kernel_in_inv_image: LEMMA FORALL (phi: homomorphism(G,GP),S: subgroup(GP)):
LET K = kernel(G,GP)(phi) IN
subset?(K, inverse_image(phi, S))
homo_inv_image_image: LEMMA FORALL (phi: homomorphism(G,GP),H: subgroup(G)):
LET K = kernel(G,GP)(phi) IN
inverse_image(phi, image(phi, H)) = prod[T1,*,one1](H,K)
homo_inv_image_image_cor: LEMMA FORALL (phi: homomorphism(G,GP),H: subgroup(G)):
LET K = kernel(G,GP)(phi) IN
inverse_image(phi, image(phi, H)) = H IFF subgroup?[T1, *, one1](K,H)
first_isomorphism_th: LEMMA FORALL (phi: homomorphism(G,GP)):
LET K = kernel(G,GP)(phi) IN
isomorphic?[left_cosets(G,K),mult(G,K),K, T2, o, one2](G/K, image(phi, G))
END homomorphism_lemmas
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
