author | desharna |
Thu, 24 Nov 2022 10:02:26 +0100 | |
changeset 76574 | 7bc934b99faf |
parent 75963 | 884dbbc8e1b3 |
permissions | -rw-r--r-- |
35849 | 1 |
(* Title: HOL/Algebra/RingHom.thy |
2 |
Author: Stephan Hohe, TU Muenchen |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
3 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
4 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
5 |
theory RingHom |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
6 |
imports Ideal |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
7 |
begin |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
8 |
|
61382 | 9 |
section \<open>Homomorphisms of Non-Commutative Rings\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
10 |
|
63167 | 11 |
text \<open>Lifting existing lemmas in a \<open>ring_hom_ring\<close> locale\<close> |
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61382
diff
changeset
|
12 |
locale ring_hom_ring = R?: ring R + S?: ring S |
29240 | 13 |
for R (structure) and S (structure) + |
29237 | 14 |
fixes h |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
15 |
assumes homh: "h \<in> ring_hom R S" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
16 |
notes hom_mult [simp] = ring_hom_mult [OF homh] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
17 |
and hom_one [simp] = ring_hom_one [OF homh] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
18 |
|
29246 | 19 |
sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring |
61169 | 20 |
by standard (rule homh) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
21 |
|
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61382
diff
changeset
|
22 |
sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S |
68687 | 23 |
proof |
24 |
show "h \<in> hom (add_monoid R) (add_monoid S)" |
|
25 |
using homh by (simp add: hom_def ring_hom_def) |
|
26 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
28 |
lemma (in ring_hom_ring) is_ring_hom_ring: |
27611 | 29 |
"ring_hom_ring R S h" |
30 |
by (rule ring_hom_ring_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
31 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
32 |
lemma ring_hom_ringI: |
27611 | 33 |
fixes R (structure) and S (structure) |
34 |
assumes "ring R" "ring S" |
|
68687 | 35 |
assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S" |
67613 | 36 |
and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
37 |
and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
38 |
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
39 |
shows "ring_hom_ring R S h" |
27611 | 40 |
proof - |
29237 | 41 |
interpret ring R by fact |
42 |
interpret ring S by fact |
|
68687 | 43 |
show ?thesis |
44 |
proof |
|
45 |
show "h \<in> ring_hom R S" |
|
46 |
unfolding ring_hom_def |
|
47 |
by (auto simp: compatible_mult compatible_add compatible_one hom_closed) |
|
48 |
qed |
|
27611 | 49 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
50 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
51 |
lemma ring_hom_ringI2: |
27611 | 52 |
assumes "ring R" "ring S" |
23350 | 53 |
assumes h: "h \<in> ring_hom R S" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
54 |
shows "ring_hom_ring R S h" |
27611 | 55 |
proof - |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29246
diff
changeset
|
56 |
interpret R: ring R by fact |
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29246
diff
changeset
|
57 |
interpret S: ring S by fact |
68687 | 58 |
show ?thesis |
59 |
proof |
|
60 |
show "h \<in> ring_hom R S" |
|
61 |
using h . |
|
62 |
qed |
|
27611 | 63 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
64 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
65 |
lemma ring_hom_ringI3: |
27611 | 66 |
fixes R (structure) and S (structure) |
67 |
assumes "abelian_group_hom R S h" "ring R" "ring S" |
|
67613 | 68 |
assumes compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
69 |
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
70 |
shows "ring_hom_ring R S h" |
27611 | 71 |
proof - |
29237 | 72 |
interpret abelian_group_hom R S h by fact |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29246
diff
changeset
|
73 |
interpret R: ring R by fact |
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29246
diff
changeset
|
74 |
interpret S: ring S by fact |
68687 | 75 |
show ?thesis |
76 |
proof |
|
77 |
show "h \<in> ring_hom R S" |
|
78 |
unfolding ring_hom_def by (auto simp: compatible_one compatible_mult) |
|
79 |
qed |
|
27611 | 80 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
81 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
82 |
lemma ring_hom_cringI: |
27611 | 83 |
assumes "ring_hom_ring R S h" "cring R" "cring S" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
84 |
shows "ring_hom_cring R S h" |
27611 | 85 |
proof - |
29237 | 86 |
interpret ring_hom_ring R S h by fact |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29246
diff
changeset
|
87 |
interpret R: cring R by fact |
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29246
diff
changeset
|
88 |
interpret S: cring S by fact |
68687 | 89 |
show ?thesis |
90 |
proof |
|
91 |
show "h \<in> ring_hom R S" |
|
92 |
by (simp add: homh) |
|
93 |
qed |
|
27611 | 94 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
95 |
|
35849 | 96 |
|
61382 | 97 |
subsection \<open>The Kernel of a Ring Homomorphism\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
98 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
99 |
\<comment> \<open>the kernel of a ring homomorphism is an ideal\<close> |
68687 | 100 |
lemma (in ring_hom_ring) kernel_is_ideal: "ideal (a_kernel R S h) R" |
75963
884dbbc8e1b3
avoid duplicate fact error on global_interpretation of residues
haftmann
parents:
70019
diff
changeset
|
101 |
apply (rule idealI [OF R.ring_axioms]) |
68687 | 102 |
apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel]) |
103 |
apply (auto simp: a_kernel_def') |
|
104 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
105 |
|
61382 | 106 |
text \<open>Elements of the kernel are mapped to zero\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
107 |
lemma (in abelian_group_hom) kernel_zero [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
108 |
"i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
109 |
by (simp add: a_kernel_defs) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
110 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
111 |
|
61382 | 112 |
subsection \<open>Cosets\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
113 |
|
61382 | 114 |
text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
115 |
lemma (in ring_hom_ring) rcos_imp_homeq: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
116 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
117 |
and xrcos: "x \<in> a_kernel R S h +> a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
118 |
shows "h x = h a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
119 |
proof - |
29237 | 120 |
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
121 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
122 |
from xrcos |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
123 |
have "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
124 |
from this obtain i |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
125 |
where iker: "i \<in> a_kernel R S h" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
126 |
and x: "x = i \<oplus> a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
127 |
by fast+ |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
128 |
note carr = acarr iker[THEN a_Hcarr] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
129 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
130 |
from x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
131 |
have "h x = h (i \<oplus> a)" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
132 |
also from carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
133 |
have "\<dots> = h i \<oplus>\<^bsub>S\<^esub> h a" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
134 |
also from iker |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
135 |
have "\<dots> = \<zero>\<^bsub>S\<^esub> \<oplus>\<^bsub>S\<^esub> h a" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
136 |
also from carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
137 |
have "\<dots> = h a" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
138 |
finally |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
139 |
show "h x = h a" . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
140 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
141 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
142 |
lemma (in ring_hom_ring) homeq_imp_rcos: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
143 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
144 |
and xcarr: "x \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
145 |
and hx: "h x = h a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
146 |
shows "x \<in> a_kernel R S h +> a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
147 |
proof - |
29237 | 148 |
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
149 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
150 |
note carr = acarr xcarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
151 |
note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
152 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
153 |
from hx and hcarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
154 |
have a: "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = \<zero>\<^bsub>S\<^esub>" by algebra |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
155 |
from carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
156 |
have "h x \<oplus>\<^bsub>S\<^esub> \<ominus>\<^bsub>S\<^esub>h a = h (x \<oplus> \<ominus>a)" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
157 |
from a and this |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
158 |
have b: "h (x \<oplus> \<ominus>a) = \<zero>\<^bsub>S\<^esub>" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
159 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
160 |
from carr have "x \<oplus> \<ominus>a \<in> carrier R" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
161 |
from this and b |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
162 |
have "x \<oplus> \<ominus>a \<in> a_kernel R S h" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
163 |
unfolding a_kernel_def' |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
164 |
by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
165 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
166 |
from this and carr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
167 |
show "x \<in> a_kernel R S h +> a" by (simp add: a_rcos_module_rev) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
168 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
169 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
170 |
corollary (in ring_hom_ring) rcos_eq_homeq: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
171 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
172 |
shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}" |
68687 | 173 |
proof - |
29237 | 174 |
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) |
68687 | 175 |
show ?thesis |
176 |
using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
177 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
178 |
|
70019
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
179 |
lemma (in ring_hom_ring) hom_nat_pow: |
68664
bd0df72c16d5
updated material concerning Algebra
paulson <lp15@cam.ac.uk>
parents:
68551
diff
changeset
|
180 |
"x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n" |
bd0df72c16d5
updated material concerning Algebra
paulson <lp15@cam.ac.uk>
parents:
68551
diff
changeset
|
181 |
by (induct n) (auto) |
bd0df72c16d5
updated material concerning Algebra
paulson <lp15@cam.ac.uk>
parents:
68551
diff
changeset
|
182 |
|
bd0df72c16d5
updated material concerning Algebra
paulson <lp15@cam.ac.uk>
parents:
68551
diff
changeset
|
183 |
|
69895
6b03a8cf092d
more formal contributors (with the help of the history);
wenzelm
parents:
68687
diff
changeset
|
184 |
lemma (in ring_hom_ring) inj_on_domain: \<^marker>\<open>contributor \<open>Paulo EmÃlio de Vilhena\<close>\<close> |
68551
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
185 |
assumes "inj_on h (carrier R)" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
186 |
shows "domain S \<Longrightarrow> domain R" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
187 |
proof - |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
188 |
assume A: "domain S" show "domain R" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
189 |
proof |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
190 |
have "h \<one> = \<one>\<^bsub>S\<^esub> \<and> h \<zero> = \<zero>\<^bsub>S\<^esub>" by simp |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
191 |
hence "h \<one> \<noteq> h \<zero>" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
192 |
using domain.one_not_zero[OF A] by simp |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
193 |
thus "\<one> \<noteq> \<zero>" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
194 |
using assms unfolding inj_on_def by fastforce |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
195 |
next |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
196 |
fix a b |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
197 |
assume a: "a \<in> carrier R" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
198 |
and b: "b \<in> carrier R" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
199 |
have "h (a \<otimes> b) = (h a) \<otimes>\<^bsub>S\<^esub> (h b)" by (simp add: a b) |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
200 |
also have " ... = (h b) \<otimes>\<^bsub>S\<^esub> (h a)" using a b A cringE(1)[of S] |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
201 |
by (simp add: cring.cring_simprules(14) domain_def) |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
202 |
also have " ... = h (b \<otimes> a)" by (simp add: a b) |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
203 |
finally have "h (a \<otimes> b) = h (b \<otimes> a)" . |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
204 |
thus "a \<otimes> b = b \<otimes> a" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
205 |
using assms a b unfolding inj_on_def by simp |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
206 |
|
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
207 |
assume ab: "a \<otimes> b = \<zero>" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
208 |
hence "h (a \<otimes> b) = \<zero>\<^bsub>S\<^esub>" by simp |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
209 |
hence "(h a) \<otimes>\<^bsub>S\<^esub> (h b) = \<zero>\<^bsub>S\<^esub>" using a b by simp |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
210 |
hence "h a = \<zero>\<^bsub>S\<^esub> \<or> h b = \<zero>\<^bsub>S\<^esub>" using a b domain.integral[OF A] by simp |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
211 |
thus "a = \<zero> \<or> b = \<zero>" |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
212 |
using a b assms unfolding inj_on_def by force |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
213 |
qed |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
214 |
qed |
b680e74eb6f2
More on Algebra by Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
215 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
216 |
end |