homomorphisms[T1: TYPE,
              *: [T1,T1 -> T1],
              one1: T1,
              T2: TYPE,
              o: [T2,T2 -> T2],
              one2: T2]: THEORY
%-----------------------------------------------------------------------------
%  Experimental theory 
%
%     Author: Rick Butler
%
%-----------------------------------------------------------------------------
BEGIN

  
   ASSUMING IMPORTING group_def

       T1_is_group: ASSUMPTION group?[T1,*,one1](fullset[T1])
       T2_is_group: ASSUMPTION group?[T2,o,one2](fullset[T2])

   ENDASSUMING


   IMPORTING group[T1,*,one1], group[T2,o,one2]


   homomorphism?(G1: group[T1,*,one1],
                 G2: group[T2,o,one2],
                  phi: [(G1) -> (G2)]): bool  =
                    (FORALL (a,b: (G1)): phi(a*b) = phi(a) o phi(b))


   isomorphism?(G1: group[T1,*,one1],
                G2: group[T2,o,one2],
                  phi: [(G1) -> (G2)]): bool  = bijective?(phi) AND
                                                homomorphism?(G1,G2,phi)

   homomorphic?(G1: group[T1,*,one1],
                G2: group[T2,o,one2]): bool = 
                    EXISTS (phi: [(G1) -> (G2)]): homomorphism?(G1,G2,phi)



   isomorphic?(G1: group[T1,*,one1],
               G2: group[T2,o,one2]): bool = 
                    EXISTS (phi: [(G1) -> (G2)]): isomorphism?(G1,G2,phi)




   G:  VAR group[T1,*,one1]
   GP: VAR group[T2,o,one2]

   homomorphism(G,GP): TYPE = {phi:[(G) -> (GP)] | homomorphism?(G,GP,phi)}
   isomorphism (G,GP): TYPE = {phi:[(G) -> (GP)] |  isomorphism?(G,GP,phi)}


   homo_one: LEMMA FORALL (phi: homomorphism(G,GP)): phi(one1) = one2


   kernel(G: group[T1,*,one1],
          GP: group[T2,o,one2])(phi: homomorphism(G,GP)): subgroup[T1,*,one1](G) =
              {a: T1 | G(a) AND phi(a) = one2}
  
END homomorphisms