equal
deleted
inserted
replaced
|
1 (* Title: HOL/GroupTheory/Homomorphism |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 Copyright 1998-2001 University of Cambridge |
|
5 |
|
6 Homomorphisms of groups, rings, and automorphisms. |
|
7 Sigma version with Locales |
|
8 *) |
|
9 |
|
10 Homomorphism = Ring + Bij + |
|
11 |
|
12 consts |
|
13 Hom :: "('a grouptype * 'b grouptype * ('a => 'b)) set" |
|
14 |
|
15 defs |
|
16 Hom_def "Hom == \\<Sigma>G \\<in> Group. \\<Sigma>H \\<in> Group. {Phi. Phi \\<in> (G.<cr>) \\<rightarrow> (H.<cr>) & |
|
17 (\\<forall>x \\<in> (G.<cr>) . \\<forall>y \\<in> (G.<cr>) . (Phi((G.<f>) x y) = (H.<f>) (Phi x)(Phi y)))}" |
|
18 |
|
19 consts |
|
20 RingHom :: "(('a ringtype) * ('b ringtype) * ('a => 'b))set" |
|
21 defs |
|
22 RingHom_def "RingHom == \\<Sigma>R1 \\<in> Ring. \\<Sigma>R2 \\<in> Ring. {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) & |
|
23 (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) & |
|
24 (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}" |
|
25 |
|
26 consts |
|
27 GroupAuto :: "('a grouptype * ('a => 'a)) set" |
|
28 |
|
29 defs |
|
30 GroupAuto_def "GroupAuto == \\<Sigma>G \\<in> Group. {Phi. (G,G,Phi)\\<in>Hom & |
|
31 inj_on Phi (G.<cr>) & Phi ` (G.<cr>) = (G.<cr>)}" |
|
32 |
|
33 consts |
|
34 RingAuto :: "(('a ringtype) * ('a => 'a))set" |
|
35 |
|
36 defs |
|
37 RingAuto_def "RingAuto == \\<Sigma>R \\<in> Ring. {Phi. (R,R,Phi)\\<in>RingHom & |
|
38 inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}" |
|
39 |
|
40 end |