%%-------------------** 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