src/HOL/GroupTheory/Homomorphism.thy

Final version of Florian Kammueller's examples

(*  Title:      HOL/GroupTheory/Homomorphism
    ID:         $Id$
    Author:     Florian Kammueller, with new proofs by L C Paulson
    Copyright   1998-2001  University of Cambridge

Homomorphisms of groups, rings, and automorphisms.
Sigma version with Locales
*)

Homomorphism = Ring + Bij +

consts
  Hom :: "('a grouptype * 'b grouptype * ('a => 'b)) set"

defs
  Hom_def "Hom == \\<Sigma>G \\<in> Group. \\<Sigma>H \\<in> Group. {Phi. Phi \\<in> (G.<cr>) \\<rightarrow> (H.<cr>) & 
                  (\\<forall>x \\<in> (G.<cr>) . \\<forall>y \\<in> (G.<cr>) . (Phi((G.<f>) x y) = (H.<f>) (Phi x)(Phi y)))}"

consts
  RingHom :: "(('a ringtype) * ('b ringtype) * ('a => 'b))set"
defs
  RingHom_def "RingHom == \\<Sigma>R1 \\<in> Ring. \\<Sigma>R2 \\<in> Ring. {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) &
                   (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &
                   (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}"

consts
  GroupAuto :: "('a grouptype * ('a => 'a)) set"

defs
  GroupAuto_def "GroupAuto == \\<Sigma>G \\<in> Group. {Phi. (G,G,Phi)\\<in>Hom  &
                    inj_on Phi (G.<cr>) & Phi ` (G.<cr>) = (G.<cr>)}"

consts
  RingAuto :: "(('a ringtype) * ('a => 'a))set"

defs
  RingAuto_def "RingAuto == \\<Sigma>R \\<in> Ring. {Phi. (R,R,Phi)\\<in>RingHom &
                    inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}"

end