|
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 Open_locale "bij"; |
|
11 |
|
12 Addsimps [B_def, o'_def, inv'_def]; |
|
13 |
|
14 Goal "[|x \\<in> S; f \\<in> B|] ==> EX x'. x = f x'"; |
|
15 by (dtac BijE2 1); |
|
16 by Auto_tac; |
|
17 |
|
18 |
|
19 Goal "[| f \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S;\ |
|
20 \ \\<forall>x \\<in> S. \\<forall>y \\<in> S. f(g x y) = g (f x) (f y) |] \ |
|
21 \ ==> inv' f (g x y) = g (inv' f x) (inv' f y)"; |
|
22 by (subgoal_tac "EX x':S. EX y':S. x = f x' & y = f y'" 1); |
|
23 by (blast_tac (claset() addDs [BijE2]) 2); |
|
24 by (Clarify_tac 1); |
|
25 (*the next step could be avoided if we could re-orient the quanitifed |
|
26 assumption, to rewrite g (f x') (f y') ...*) |
|
27 by (rtac inj_onD 1); |
|
28 by (etac BijE3 1); |
|
29 by (asm_full_simp_tac (simpset() addsimps [f_Inv_f, Inv_f_f, BijE2, BijE3, |
|
30 funcset_mem RS funcset_mem]) 1); |
|
31 by (ALLGOALS |
|
32 (asm_full_simp_tac |
|
33 (simpset() addsimps [funcset_mem RS funcset_mem, BijE2, Inv_mem]))); |
|
34 qed "Bij_op_lemma"; |
|
35 |
|
36 Goal "[| a \\<in> B; b \\<in> B; g \\<in> S \\<rightarrow> S \\<rightarrow> S; x \\<in> S; y \\<in> S; \ |
|
37 \ \\<forall>x \\<in> S. \\<forall>y \\<in> S. a (b (g x y)) = g (a (b x)) (a (b y)) |] \ |
|
38 \ ==> (a o' b) (g x y) = g ((a o' b) x) ((a o' b) y)"; |
|
39 by (afs [o'_def, compose_eq, B_def, |
|
40 funcset_mem RS funcset_mem] 1); |
|
41 qed "Bij_comp_lemma"; |
|
42 |
|
43 |
|
44 Goal "[| R1 \\<in> Ring; R2 \\<in> Ring |] \ |
|
45 \ ==> RingHom `` {R1} `` {R2} = \ |
|
46 \ {Phi. Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>) & \ |
|
47 \ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \ |
|
48 \ (Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y))) &\ |
|
49 \ (\\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \ |
|
50 \ (Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)))}"; |
|
51 by (afs [Image_def,RingHom_def] 1); |
|
52 qed "RingHom_apply"; |
|
53 |
|
54 (* derive the defining properties as single lemmas *) |
|
55 Goal "(R1,R2,Phi) \\<in> RingHom ==> Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>)"; |
|
56 by (afs [RingHom_def] 1); |
|
57 qed "RingHom_imp_funcset"; |
|
58 |
|
59 Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |] \ |
|
60 \ ==> Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y)"; |
|
61 by (afs [RingHom_def] 1); |
|
62 qed "RingHom_preserves_rplus"; |
|
63 |
|
64 Goal "[| (R1,R2,Phi) \\<in> RingHom; x \\<in> (R1.<cr>); y \\<in> (R1.<cr>) |] \ |
|
65 \ ==> Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)"; |
|
66 by (afs [RingHom_def] 1); |
|
67 qed "RingHom_preserves_rmult"; |
|
68 |
|
69 Goal "[| R1 \\<in> Ring; R2 \\<in> Ring; Phi \\<in> (R1.<cr>) \\<rightarrow> (R2.<cr>); \ |
|
70 \ \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \ |
|
71 \ Phi((R1.<f>) x y) = (R2.<f>) (Phi x) (Phi y);\ |
|
72 \ \\<forall>x \\<in> (R1.<cr>). \\<forall>y \\<in> (R1.<cr>). \ |
|
73 \ Phi((R1.<m>) x y) = (R2.<m>) (Phi x) (Phi y)|]\ |
|
74 \ ==> (R1,R2,Phi) \\<in> RingHom"; |
|
75 by (afs [RingHom_def] 1); |
|
76 qed "RingHomI"; |
|
77 |
|
78 Open_locale "ring"; |
|
79 |
|
80 val Ring_R = thm "Ring_R"; |
|
81 val rmult_def = thm "rmult_def"; |
|
82 |
|
83 Addsimps [simp_R, Ring_R]; |
|
84 |
|
85 |
|
86 |
|
87 (* RingAutomorphisms *) |
|
88 Goal "RingAuto `` {R} = \ |
|
89 \ {Phi. (R,R,Phi) \\<in> RingHom & inj_on Phi (R.<cr>) & Phi ` (R.<cr>) = (R.<cr>)}"; |
|
90 by (rewtac RingAuto_def); |
|
91 by (afs [Image_def] 1); |
|
92 qed "RingAuto_apply"; |
|
93 |
|
94 Goal "(R,Phi) \\<in> RingAuto ==> (R, R, Phi) \\<in> RingHom"; |
|
95 by (afs [RingAuto_def] 1); |
|
96 qed "RingAuto_imp_RingHom"; |
|
97 |
|
98 Goal "(R,Phi) \\<in> RingAuto ==> inj_on Phi (R.<cr>)"; |
|
99 by (afs [RingAuto_def] 1); |
|
100 qed "RingAuto_imp_inj_on"; |
|
101 |
|
102 Goal "(R,Phi) \\<in> RingAuto ==> Phi ` (R.<cr>) = (R.<cr>)"; |
|
103 by (afs [RingAuto_def] 1); |
|
104 qed "RingAuto_imp_preserves_R"; |
|
105 |
|
106 Goal "(R,Phi) \\<in> RingAuto ==> Phi \\<in> (R.<cr>) \\<rightarrow> (R.<cr>)"; |
|
107 by (etac (RingAuto_imp_RingHom RS RingHom_imp_funcset) 1); |
|
108 qed "RingAuto_imp_funcset"; |
|
109 |
|
110 Goal "[| (R,R,Phi) \\<in> RingHom; \ |
|
111 \ inj_on Phi (R.<cr>); \ |
|
112 \ Phi ` (R.<cr>) = (R.<cr>) |]\ |
|
113 \ ==> (R,Phi) \\<in> RingAuto"; |
|
114 by (afs [RingAuto_def] 1); |
|
115 qed "RingAutoI"; |
|
116 |
|
117 |
|
118 (* major result: RingAutomorphism builds a group *) |
|
119 (* We prove that they are a subgroup of the bijection group. |
|
120 Note!!! Here we need "RingAuto `` {R} ~= {}", (as a result from the |
|
121 resolution with subgroupI). That is, this is an example where one might say |
|
122 the discipline of Pi types pays off, because there we have the proof basically |
|
123 already there (compare the Pi-version). |
|
124 Here in the Sigma version, we have to redo now the proofs (or slightly |
|
125 adapted verisions) of promoteRingHom and promoteRingAuto *) |
|
126 |
|
127 Goal "RingAuto `` {R} ~= {}"; |
|
128 by (stac RingAuto_apply 1); |
|
129 by Auto_tac; |
|
130 by (res_inst_tac [("x","lam y: (R.<cr>). y")] exI 1); |
|
131 by (auto_tac (claset(), simpset() addsimps [inj_on_def])); |
|
132 by (asm_full_simp_tac (simpset() addsimps [RingHom_def, restrictI, |
|
133 R_binop_def, symmetric (rmult_def), rplus_closed, rmult_closed]) 1); |
|
134 qed "RingAutoEx"; |
|
135 |
|
136 Goal "(R,f) \\<in> RingAuto ==> f \\<in> Bij (R.<cr>)"; |
|
137 by (afs [RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on, |
|
138 RingAuto_imp_preserves_R, export BijI] 1); |
|
139 qed "RingAuto_Bij"; |
|
140 Addsimps [RingAuto_Bij]; |
|
141 |
|
142 Goal "[| (R,a) \\<in> RingAuto; (R,b) \\<in> RingAuto; \ |
|
143 \ g \\<in> (R.<cr>) \\<rightarrow> (R.<cr>) \\<rightarrow> (R.<cr>); x \\<in> carrier R; y \\<in> carrier R; \ |
|
144 \ \\<forall>Phi. (R,Phi) \\<in> RingAuto --> \ |
|
145 \ (\\<forall>x \\<in> (R.<cr>). \\<forall>y \\<in> (R.<cr>). Phi(g x y) = g(Phi x) (Phi y)) |] \ |
|
146 \ ==> compose (R.<cr>) a b (g x y) = \ |
|
147 \ g (compose (R.<cr>) a b x) (compose (R.<cr>) a b y)"; |
|
148 by (asm_simp_tac (simpset() addsimps [export Bij_comp_lemma, |
|
149 RingAuto_imp_funcset RS funcset_mem]) 1); |
|
150 qed "Auto_comp_lemma"; |
|
151 |
|
152 Goal "[|(R, a) \\<in> RingAuto; x \\<in> carrier R; y \\<in> carrier R|] \ |
|
153 \ ==> Inv (carrier R) a (x ## y) = \ |
|
154 \ Inv (carrier R) a x ## Inv (carrier R) a y"; |
|
155 by (rtac (export Bij_op_lemma) 1); |
|
156 by (etac RingAuto_Bij 1); |
|
157 by (rtac rplus_funcset 1); |
|
158 by (assume_tac 1); |
|
159 by (assume_tac 1); |
|
160 by (asm_simp_tac (simpset() addsimps [R_binop_def RS sym, |
|
161 RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1); |
|
162 qed "Inv_rplus_lemma"; |
|
163 |
|
164 Goal "(R,a) \\<in> RingAuto \ |
|
165 \ ==> (R, grouptype.inverse (BijGroup (carrier R)) a) \\<in> RingAuto"; |
|
166 by (rtac RingAutoI 1); |
|
167 by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE3)] 2); |
|
168 by (afs [BijGroup_def, export (restrict_Inv_Bij RS BijE2)] 2); |
|
169 by (rtac RingHomI 1); |
|
170 by (rtac (Ring_R) 1); |
|
171 by (rtac (Ring_R) 1); |
|
172 (* ... ==> (BijGroup (R .<R>) .<inv>) a \\<in> (R .<R>) \\<rightarrow> (R .<R>) *) |
|
173 by (asm_simp_tac (simpset() addsimps [BijGroup_def, |
|
174 export restrict_Inv_Bij RS export BijE1]) 1); |
|
175 by (asm_simp_tac (simpset() addsimps [BijGroup_def, R_binop_def, rplus_closed, Inv_rplus_lemma]) 1); |
|
176 by (afs [BijGroup_def, symmetric (rmult_def), rmult_closed] 1); |
|
177 by (afs [export Bij_op_lemma, rmult_funcset, rmult_def, |
|
178 RingAuto_imp_RingHom RS RingHom_preserves_rmult] 1); |
|
179 qed "inverse_BijGroup_lemma"; |
|
180 |
|
181 Goal "[|(R, a) \\<in> RingAuto; (R, b) \\<in> RingAuto|] \ |
|
182 \ ==> (R, bin_op (BijGroup (carrier R)) a b) \\<in> RingAuto"; |
|
183 by (afs [BijGroup_def] 1); |
|
184 by (rtac RingAutoI 1); |
|
185 by (rtac RingHomI 1); |
|
186 by (rtac (Ring_R) 1); |
|
187 by (rtac (Ring_R) 1); |
|
188 by (afs [RingAuto_Bij,export compose_Bij,export BijE1] 1); |
|
189 by (Clarify_tac 1); |
|
190 by (rtac Auto_comp_lemma 1); |
|
191 by (ALLGOALS Asm_full_simp_tac); |
|
192 by (asm_full_simp_tac (simpset() addsimps [R_binop_def, rplus_funcset]) 1); |
|
193 by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rplus]) 1); |
|
194 by (Clarify_tac 1); |
|
195 by (rtac Auto_comp_lemma 1); |
|
196 by (assume_tac 1); |
|
197 by (assume_tac 1); |
|
198 by (asm_full_simp_tac (simpset() addsimps [rmult_funcset]) 1); |
|
199 by (assume_tac 1); |
|
200 by (assume_tac 1); |
|
201 by (blast_tac (claset() addIs [RingAuto_imp_RingHom RS RingHom_preserves_rmult]) 1); |
|
202 (* ==> inj_on (compose (R .<R>) a b) (R .<R>) *) |
|
203 by (blast_tac (claset() delrules [equalityI] |
|
204 addIs [inj_on_compose, RingAuto_imp_inj_on, |
|
205 RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1); |
|
206 (* ==> compose (R .<R>) a b ` (R .<R>) = (R .<R>) *) |
|
207 by (blast_tac (claset() delrules [equalityI] |
|
208 addIs [surj_compose, RingAuto_imp_funcset, RingAuto_imp_preserves_R]) 1); |
|
209 qed "binop_BijGroup_lemma"; |
|
210 |
|
211 |
|
212 (* Ring automorphisms are a subgroup of the group of bijections over the |
|
213 ring's carrier, and thus a group *) |
|
214 Goal "RingAuto `` {R} <<= BijGroup (R.<cr>)"; |
|
215 by (rtac SubgroupI 1); |
|
216 by (rtac (export Bij_are_Group) 1); |
|
217 (* 1. RingAuto `` {R} <= (BijGroup (R .<R>) .<cr>) *) |
|
218 by (afs [subset_def, BijGroup_def, Bij_def, |
|
219 RingAuto_imp_RingHom RS RingHom_imp_funcset, RingAuto_imp_inj_on, |
|
220 RingAuto_imp_preserves_R, Image_def] 1); |
|
221 (* 1. !!R. R \\<in> Ring ==> RingAuto `` {R} ~= {} *) |
|
222 by (rtac RingAutoEx 1); |
|
223 by (auto_tac (claset(), |
|
224 simpset() addsimps [inverse_BijGroup_lemma, binop_BijGroup_lemma])); |
|
225 qed "RingAuto_SG_BijGroup"; |
|
226 |
|
227 Delsimps [simp_R, Ring_R]; |
|
228 |
|
229 Close_locale "ring"; |
|
230 Close_locale "group"; |
|
231 |
|
232 val RingAuto_are_Group = (export RingAuto_SG_BijGroup) RS (export Bij_are_Group RS SubgroupE2); |
|
233 (* So far: |
|
234 "[| ?R2 \\<in> Ring; group_of ?R2 \\<in> Group |] |
|
235 ==> (| carrier = RingAuto `` {?R2}, |
|
236 bin_op = |
|
237 lam x:RingAuto `` {?R2}. |
|
238 restrict ((BijGroup (?R2 .<cr>) .<f>) x) (RingAuto `` {?R2}), |
|
239 inverse = restrict (BijGroup (?R2 .<cr>) .<inv>) (RingAuto `` {?R2}), |
|
240 unit = BijGroup (?R2 .<cr>) .<e> |) \\<in> Group" *) |
|
241 |
|
242 (* Unfortunately we have to eliminate the extra assumptions |
|
243 Now only group_of R \\<in> Group *) |
|
244 |
|
245 Goal "R \\<in> Ring ==> group_of R \\<in> Group"; |
|
246 by (asm_full_simp_tac (simpset() addsimps [group_of_def]) 1); |
|
247 by (rtac Abel_imp_Group 1); |
|
248 by (etac (export R_Abel) 1); |
|
249 qed "R_Group"; |
|
250 |
|
251 Goal "R \\<in> Ring ==> (| carrier = RingAuto `` {R},\ |
|
252 \ bin_op = lam x:RingAuto `` {R}. lam y: RingAuto `` {R}.\ |
|
253 \ (BijGroup (R.<cr>) .<f>) x y ,\ |
|
254 \ inverse = lam x: RingAuto `` {R}. (BijGroup (R.<cr>) .<inv>) x,\ |
|
255 \ unit = BijGroup (R.<cr>) .<e> |) \\<in> Group"; |
|
256 by (rtac (R_Group RSN (2, RingAuto_are_Group)) 1); |
|
257 by (assume_tac 1); |
|
258 by (assume_tac 1); |
|
259 qed "RingAuto_are_Groupf"; |
|
260 |
|
261 (* "?R \\<in> Ring |
|
262 ==> (| carrier = RingAuto `` {?R}, |
|
263 bin_op = |
|
264 lam x:RingAuto `` {?R}. |
|
265 restrict ((BijGroup (?R .<cr>) .<f>) x) (RingAuto `` {?R}), |
|
266 inverse = restrict (BijGroup (?R .<cr>) .<inv>) (RingAuto `` {?R}), |
|
267 unit = BijGroup (?R .<cr>) .<e> |) \\<in> Group" *) |