author | wenzelm |
Tue, 03 Jul 2018 11:00:37 +0200 | |
changeset 68582 | b9b9e2985878 |
parent 68464 | 3ead36cbe6b7 |
child 68604 | 57721285d4ef |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Algebra/Ideal.thy |
35849 | 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 Ideal |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
6 |
imports Ring AbelCoset |
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>Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
10 |
|
61382 | 11 |
subsection \<open>Definitions\<close> |
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset
|
12 |
|
61382 | 13 |
subsubsection \<open>General definition\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
14 |
|
29240 | 15 |
locale ideal = additive_subgroup I R + ring R for I and R (structure) + |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
16 |
assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I" |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
17 |
and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
18 |
|
29237 | 19 |
sublocale ideal \<subseteq> abelian_subgroup I R |
68458 | 20 |
proof (intro abelian_subgroupI3 abelian_group.intro) |
21 |
show "additive_subgroup I R" |
|
22 |
by (simp add: is_additive_subgroup) |
|
23 |
show "abelian_monoid R" |
|
24 |
by (simp add: abelian_monoid_axioms) |
|
25 |
show "abelian_group_axioms R" |
|
26 |
using abelian_group_def is_abelian_group by blast |
|
27 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
28 |
|
44677 | 29 |
lemma (in ideal) is_ideal: "ideal I R" |
30 |
by (rule ideal_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 idealI: |
27611 | 33 |
fixes R (structure) |
34 |
assumes "ring R" |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
35 |
assumes a_subgroup: "subgroup I (add_monoid R)" |
44677 | 36 |
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I" |
37 |
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
38 |
shows "ideal I R" |
27611 | 39 |
proof - |
29237 | 40 |
interpret ring R by fact |
68464 | 41 |
show ?thesis |
42 |
by (auto simp: ideal.intro ideal_axioms.intro additive_subgroupI a_subgroup is_ring I_l_closed I_r_closed) |
|
27611 | 43 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
44 |
|
35849 | 45 |
|
61382 | 46 |
subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
47 |
|
44677 | 48 |
definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79) |
61952 | 49 |
where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
50 |
|
61382 | 51 |
subsubsection \<open>Principal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
52 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
53 |
locale principalideal = ideal + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
54 |
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
55 |
|
44677 | 56 |
lemma (in principalideal) is_principalideal: "principalideal I R" |
57 |
by (rule principalideal_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
58 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
59 |
lemma principalidealI: |
27611 | 60 |
fixes R (structure) |
61 |
assumes "ideal I R" |
|
47409 | 62 |
and generate: "\<exists>i \<in> carrier R. I = Idl {i}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
63 |
shows "principalideal I R" |
27611 | 64 |
proof - |
29237 | 65 |
interpret ideal I R by fact |
44677 | 66 |
show ?thesis |
67 |
by (intro principalideal.intro principalideal_axioms.intro) |
|
68 |
(rule is_ideal, rule generate) |
|
27611 | 69 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
70 |
|
35849 | 71 |
|
61382 | 72 |
subsubsection \<open>Maximal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
73 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
74 |
locale maximalideal = ideal + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
75 |
assumes I_notcarr: "carrier R \<noteq> I" |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
76 |
and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
77 |
|
44677 | 78 |
lemma (in maximalideal) is_maximalideal: "maximalideal I R" |
79 |
by (rule maximalideal_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
80 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
81 |
lemma maximalidealI: |
27611 | 82 |
fixes R |
83 |
assumes "ideal I R" |
|
47409 | 84 |
and I_notcarr: "carrier R \<noteq> I" |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
85 |
and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
86 |
shows "maximalideal I R" |
27611 | 87 |
proof - |
29237 | 88 |
interpret ideal I R by fact |
44677 | 89 |
show ?thesis |
90 |
by (intro maximalideal.intro maximalideal_axioms.intro) |
|
91 |
(rule is_ideal, rule I_notcarr, rule I_maximal) |
|
27611 | 92 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
93 |
|
35849 | 94 |
|
61382 | 95 |
subsubsection \<open>Prime Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
96 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
97 |
locale primeideal = ideal + cring + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
98 |
assumes I_notcarr: "carrier R \<noteq> I" |
44677 | 99 |
and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
100 |
|
63633 | 101 |
lemma (in primeideal) primeideal: "primeideal I R" |
44677 | 102 |
by (rule primeideal_axioms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
103 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
104 |
lemma primeidealI: |
27611 | 105 |
fixes R (structure) |
106 |
assumes "ideal I R" |
|
47409 | 107 |
and "cring R" |
108 |
and I_notcarr: "carrier R \<noteq> I" |
|
44677 | 109 |
and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
110 |
shows "primeideal I R" |
27611 | 111 |
proof - |
29237 | 112 |
interpret ideal I R by fact |
113 |
interpret cring R by fact |
|
44677 | 114 |
show ?thesis |
115 |
by (intro primeideal.intro primeideal_axioms.intro) |
|
116 |
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime) |
|
27611 | 117 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
118 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
119 |
lemma primeidealI2: |
27611 | 120 |
fixes R (structure) |
121 |
assumes "additive_subgroup I R" |
|
47409 | 122 |
and "cring R" |
123 |
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I" |
|
44677 | 124 |
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I" |
125 |
and I_notcarr: "carrier R \<noteq> I" |
|
126 |
and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
127 |
shows "primeideal I R" |
27611 | 128 |
proof - |
29240 | 129 |
interpret additive_subgroup I R by fact |
29237 | 130 |
interpret cring R by fact |
68464 | 131 |
show ?thesis apply intro_locales |
27611 | 132 |
apply (intro ideal_axioms.intro) |
133 |
apply (erule (1) I_l_closed) |
|
134 |
apply (erule (1) I_r_closed) |
|
68464 | 135 |
by (simp add: I_notcarr I_prime primeideal_axioms.intro) |
27611 | 136 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
137 |
|
35849 | 138 |
|
61382 | 139 |
subsection \<open>Special Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
140 |
|
44677 | 141 |
lemma (in ring) zeroideal: "ideal {\<zero>} R" |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
142 |
by (intro idealI subgroup.intro) (simp_all add: is_ring) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
143 |
|
44677 | 144 |
lemma (in ring) oneideal: "ideal (carrier R) R" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
145 |
by (rule idealI) (auto intro: is_ring add.subgroupI) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
146 |
|
44677 | 147 |
lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R" |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
148 |
proof - |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
149 |
have "carrier R \<noteq> {\<zero>}" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
150 |
by (simp add: carrier_one_not_zero) |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
151 |
then show ?thesis |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
152 |
by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
153 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
154 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
155 |
|
61382 | 156 |
subsection \<open>General Ideal Properies\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
157 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
158 |
lemma (in ideal) one_imp_carrier: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
159 |
assumes I_one_closed: "\<one> \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
160 |
shows "I = carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
161 |
proof |
68464 | 162 |
show "carrier R \<subseteq> I" |
163 |
using I_r_closed assms by fastforce |
|
164 |
show "I \<subseteq> carrier R" |
|
165 |
by (rule a_subset) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
166 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
167 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
168 |
lemma (in ideal) Icarr: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
169 |
assumes iI: "i \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
170 |
shows "i \<in> carrier R" |
44677 | 171 |
using iI by (rule a_Hcarr) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
172 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
173 |
|
61382 | 174 |
subsection \<open>Intersection of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
175 |
|
61506 | 176 |
paragraph \<open>Intersection of two ideals\<close> |
177 |
text \<open>The intersection of any two ideals is again an ideal in @{term R}\<close> |
|
178 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
179 |
lemma (in ring) i_intersect: |
27611 | 180 |
assumes "ideal I R" |
181 |
assumes "ideal J R" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
182 |
shows "ideal (I \<inter> J) R" |
27611 | 183 |
proof - |
29237 | 184 |
interpret ideal I R by fact |
29240 | 185 |
interpret ideal J R by fact |
68464 | 186 |
have IJ: "I \<inter> J \<subseteq> carrier R" |
187 |
by (force simp: a_subset) |
|
27611 | 188 |
show ?thesis |
44677 | 189 |
apply (intro idealI subgroup.intro) |
68464 | 190 |
apply (simp_all add: IJ is_ring I_l_closed assms ideal.I_l_closed ideal.I_r_closed flip: a_inv_def) |
44677 | 191 |
done |
27611 | 192 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
193 |
|
68464 | 194 |
text \<open>The intersection of any Number of Ideals is again an Ideal in @{term R}\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
195 |
|
68464 | 196 |
lemma (in ring) i_Intersect: |
197 |
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}" |
|
198 |
shows "ideal (\<Inter>S) R" |
|
199 |
proof - |
|
200 |
{ fix x y J |
|
201 |
assume "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S" |
|
202 |
interpret ideal J R by (rule Sideals[OF JS]) |
|
203 |
have "x \<oplus> y \<in> J" |
|
204 |
by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>) } |
|
205 |
moreover |
|
206 |
have "\<zero> \<in> J" if "J \<in> S" for J |
|
207 |
by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) |
|
208 |
moreover |
|
209 |
{ fix x J |
|
210 |
assume "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S" |
|
211 |
interpret ideal J R by (rule Sideals[OF JS]) |
|
212 |
have "\<ominus> x \<in> J" |
|
213 |
by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>) } |
|
214 |
moreover |
|
215 |
{ fix x y J |
|
216 |
assume "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S" |
|
217 |
interpret ideal J R by (rule Sideals[OF JS]) |
|
218 |
have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" |
|
219 |
using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+ } |
|
220 |
moreover |
|
221 |
{ fix x |
|
222 |
assume "\<forall>I\<in>S. x \<in> I" |
|
223 |
obtain I0 where I0S: "I0 \<in> S" |
|
224 |
using notempty by blast |
|
225 |
interpret ideal I0 R by (rule Sideals[OF I0S]) |
|
226 |
have "x \<in> I0" |
|
227 |
by (simp add: I0S \<open>\<forall>I\<in>S. x \<in> I\<close>) |
|
228 |
with a_subset have "x \<in> carrier R" by fast } |
|
229 |
ultimately show ?thesis |
|
230 |
by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
232 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
233 |
|
61382 | 234 |
subsection \<open>Addition of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
235 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
236 |
lemma (in ring) add_ideals: |
68464 | 237 |
assumes idealI: "ideal I R" and idealJ: "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
238 |
shows "ideal (I <+> J) R" |
68464 | 239 |
proof (rule ideal.intro) |
240 |
show "additive_subgroup (I <+> J) R" |
|
241 |
by (intro ideal.axioms[OF idealI] ideal.axioms[OF idealJ] add_additive_subgroups) |
|
242 |
show "ring R" |
|
243 |
by (rule is_ring) |
|
244 |
show "ideal_axioms (I <+> J) R" |
|
245 |
proof - |
|
246 |
{ fix x i j |
|
247 |
assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" |
|
248 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] |
|
249 |
have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k" |
|
250 |
by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) } |
|
251 |
moreover |
|
252 |
{ fix x i j |
|
253 |
assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" |
|
254 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] |
|
255 |
have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k" |
|
256 |
by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) } |
|
257 |
ultimately show "ideal_axioms (I <+> J) R" |
|
258 |
by (intro ideal_axioms.intro) (auto simp: set_add_defs) |
|
259 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
260 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
261 |
|
61382 | 262 |
subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
263 |
|
61382 | 264 |
text \<open>@{term genideal} generates an ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
265 |
lemma (in ring) genideal_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
266 |
assumes Scarr: "S \<subseteq> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
267 |
shows "ideal (Idl S) R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
268 |
unfolding genideal_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
269 |
proof (rule i_Intersect, fast, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
270 |
from oneideal and Scarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
271 |
show "\<exists>I. ideal I R \<and> S \<le> I" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
272 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
273 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
274 |
lemma (in ring) genideal_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
275 |
assumes "S \<subseteq> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
276 |
shows "S \<subseteq> Idl S" |
44677 | 277 |
unfolding genideal_def by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
278 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
279 |
lemma (in ring) genideal_self': |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
280 |
assumes carr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
281 |
shows "i \<in> Idl {i}" |
68464 | 282 |
by (simp add: genideal_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
283 |
|
61382 | 284 |
text \<open>@{term genideal} generates the minimal ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
285 |
lemma (in ring) genideal_minimal: |
68464 | 286 |
assumes "ideal I R" "S \<subseteq> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
287 |
shows "Idl S \<subseteq> I" |
68464 | 288 |
unfolding genideal_def by rule (elim InterD, simp add: assms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
289 |
|
61382 | 290 |
text \<open>Generated ideals and subsets\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
291 |
lemma (in ring) Idl_subset_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
292 |
assumes Iideal: "ideal I R" |
44677 | 293 |
and Hcarr: "H \<subseteq> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
shows "(Idl H \<subseteq> I) = (H \<subseteq> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
295 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
assume a: "Idl H \<subseteq> I" |
23350 | 297 |
from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self) |
44677 | 298 |
with a show "H \<subseteq> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
fix x |
47409 | 301 |
assume "H \<subseteq> I" |
302 |
with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast |
|
44677 | 303 |
then show "Idl H \<subseteq> I" unfolding genideal_def by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
304 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
305 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
306 |
lemma (in ring) subset_Idl_subset: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
307 |
assumes Icarr: "I \<subseteq> carrier R" |
44677 | 308 |
and HI: "H \<subseteq> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
309 |
shows "Idl H \<subseteq> Idl I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
310 |
proof - |
44677 | 311 |
from Icarr have Iideal: "ideal (Idl I) R" |
312 |
by (rule genideal_ideal) |
|
313 |
from HI and Icarr have "H \<subseteq> carrier R" |
|
314 |
by fast |
|
315 |
with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)" |
|
316 |
by (rule Idl_subset_ideal[symmetric]) |
|
68464 | 317 |
then show "Idl H \<subseteq> Idl I" |
318 |
by (meson HI Icarr genideal_self order_trans) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
319 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
320 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
321 |
lemma (in ring) Idl_subset_ideal': |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
322 |
assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" |
68464 | 323 |
shows "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> a \<in> Idl {b}" |
324 |
proof - |
|
325 |
have "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> {a} \<subseteq> Idl {b}" |
|
326 |
by (simp add: Idl_subset_ideal acarr bcarr genideal_ideal) |
|
327 |
also have "\<dots> \<longleftrightarrow> a \<in> Idl {b}" |
|
328 |
by blast |
|
329 |
finally show ?thesis . |
|
330 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
331 |
|
44677 | 332 |
lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}" |
68464 | 333 |
proof |
334 |
show "Idl {\<zero>} \<subseteq> {\<zero>}" |
|
335 |
by (simp add: genideal_minimal zeroideal) |
|
336 |
show "{\<zero>} \<subseteq> Idl {\<zero>}" |
|
337 |
by (simp add: genideal_self') |
|
338 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
|
44677 | 340 |
lemma (in ring) genideal_one: "Idl {\<one>} = carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
341 |
proof - |
44677 | 342 |
interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
343 |
show "Idl {\<one>} = carrier R" |
68464 | 344 |
using genideal_self' one_imp_carrier by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
346 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
347 |
|
61382 | 348 |
text \<open>Generation of Principal Ideals in Commutative Rings\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
349 |
|
44677 | 350 |
definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79) |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
351 |
where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
352 |
|
61382 | 353 |
text \<open>genhideal (?) really generates an ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
354 |
lemma (in cring) cgenideal_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
355 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
shows "ideal (PIdl a) R" |
68464 | 357 |
unfolding cgenideal_def |
358 |
proof (intro subgroup.intro idealI[OF is_ring], simp_all) |
|
359 |
show "{x \<otimes> a |x. x \<in> carrier R} \<subseteq> carrier R" |
|
360 |
by (blast intro: acarr) |
|
361 |
show "\<And>x y. \<lbrakk>\<exists>u. x = u \<otimes> a \<and> u \<in> carrier R; \<exists>x. y = x \<otimes> a \<and> x \<in> carrier R\<rbrakk> |
|
362 |
\<Longrightarrow> \<exists>v. x \<oplus> y = v \<otimes> a \<and> v \<in> carrier R" |
|
363 |
by (metis assms cring.cring_simprules(1) is_cring l_distr) |
|
364 |
show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" |
|
365 |
by (metis assms l_null zero_closed) |
|
366 |
show "\<And>x. \<exists>u. x = u \<otimes> a \<and> u \<in> carrier R |
|
367 |
\<Longrightarrow> \<exists>v. inv\<^bsub>add_monoid R\<^esub> x = v \<otimes> a \<and> v \<in> carrier R" |
|
368 |
by (metis a_inv_def add.inv_closed assms l_minus) |
|
369 |
show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk> |
|
370 |
\<Longrightarrow> \<exists>z. x \<otimes> b = z \<otimes> a \<and> z \<in> carrier R" |
|
371 |
by (metis assms m_assoc m_closed) |
|
372 |
show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk> |
|
373 |
\<Longrightarrow> \<exists>z. b \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" |
|
374 |
by (metis assms m_assoc m_comm m_closed) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
375 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
376 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
377 |
lemma (in ring) cgenideal_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
378 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
379 |
shows "i \<in> PIdl i" |
44677 | 380 |
unfolding cgenideal_def |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
381 |
proof simp |
44677 | 382 |
from icarr have "i = \<one> \<otimes> i" |
383 |
by simp |
|
384 |
with icarr show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R" |
|
385 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
386 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
387 |
|
61382 | 388 |
text \<open>@{const "cgenideal"} is minimal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
389 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
390 |
lemma (in ring) cgenideal_minimal: |
27611 | 391 |
assumes "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
392 |
assumes aJ: "a \<in> J" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
393 |
shows "PIdl a \<subseteq> J" |
27611 | 394 |
proof - |
29240 | 395 |
interpret ideal J R by fact |
44677 | 396 |
show ?thesis |
397 |
unfolding cgenideal_def |
|
68464 | 398 |
using I_l_closed aJ by blast |
27611 | 399 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
400 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
401 |
lemma (in cring) cgenideal_eq_genideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
402 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
403 |
shows "PIdl i = Idl {i}" |
68464 | 404 |
proof |
405 |
show "PIdl i \<subseteq> Idl {i}" |
|
406 |
by (simp add: cgenideal_minimal genideal_ideal genideal_self' icarr) |
|
407 |
show "Idl {i} \<subseteq> PIdl i" |
|
408 |
by (simp add: cgenideal_ideal cgenideal_self genideal_minimal icarr) |
|
409 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
410 |
|
44677 | 411 |
lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i" |
412 |
unfolding cgenideal_def r_coset_def by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
413 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
414 |
lemma (in cring) cgenideal_is_principalideal: |
68464 | 415 |
assumes "i \<in> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
416 |
shows "principalideal (PIdl i) R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
417 |
proof - |
68464 | 418 |
have "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" |
419 |
using cgenideal_eq_genideal assms by auto |
|
420 |
then show ?thesis |
|
421 |
by (simp add: cgenideal_ideal assms principalidealI) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
422 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
423 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
424 |
|
61382 | 425 |
subsection \<open>Union of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
426 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
427 |
lemma (in ring) union_genideal: |
68464 | 428 |
assumes idealI: "ideal I R" and idealJ: "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
429 |
shows "Idl (I \<union> J) = I <+> J" |
68464 | 430 |
proof |
431 |
show "Idl (I \<union> J) \<subseteq> I <+> J" |
|
432 |
proof (rule ring.genideal_minimal [OF is_ring]) |
|
433 |
show "ideal (I <+> J) R" |
|
434 |
by (rule add_ideals[OF idealI idealJ]) |
|
435 |
have "\<And>x. x \<in> I \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb" |
|
436 |
by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def local.idealI r_zero) |
|
437 |
moreover have "\<And>x. x \<in> J \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb" |
|
438 |
by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def l_zero local.idealI) |
|
439 |
ultimately show "I \<union> J \<subseteq> I <+> J" |
|
440 |
by (auto simp: set_add_defs) |
|
441 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
442 |
next |
68464 | 443 |
show "I <+> J \<subseteq> Idl (I \<union> J)" |
444 |
by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
445 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
446 |
|
61382 | 447 |
subsection \<open>Properties of Principal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
448 |
|
61382 | 449 |
text \<open>The zero ideal is a principal ideal\<close> |
44677 | 450 |
corollary (in ring) zeropideal: "principalideal {\<zero>} R" |
68464 | 451 |
using genideal_zero principalidealI zeroideal by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
452 |
|
61382 | 453 |
text \<open>The unit ideal is a principal ideal\<close> |
44677 | 454 |
corollary (in ring) onepideal: "principalideal (carrier R) R" |
68464 | 455 |
using genideal_one oneideal principalidealI by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
456 |
|
61382 | 457 |
text \<open>Every principal ideal is a right coset of the carrier\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
458 |
lemma (in principalideal) rcos_generate: |
27611 | 459 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
460 |
shows "\<exists>x\<in>I. I = carrier R #> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
461 |
proof - |
29237 | 462 |
interpret cring R by fact |
44677 | 463 |
from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}" |
464 |
by fast+ |
|
68464 | 465 |
then have "I = PIdl i" |
44677 | 466 |
by (simp add: cgenideal_eq_genideal) |
68464 | 467 |
moreover have "i \<in> I" |
468 |
by (simp add: I1 genideal_self' icarr) |
|
469 |
moreover have "PIdl i = carrier R #> i" |
|
44677 | 470 |
unfolding cgenideal_def r_coset_def by fast |
68464 | 471 |
ultimately show "\<exists>x\<in>I. I = carrier R #> x" |
44677 | 472 |
by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
473 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
474 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
475 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
476 |
(* Next lemma contributed by Paulo Emílio de Vilhena. *) |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
477 |
|
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
478 |
text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing, |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
479 |
but it makes more sense to have it here (easier to find and coherent with the |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
480 |
previous developments).\<close> |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
481 |
|
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
482 |
lemma (in cring) cgenideal_prod: |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
483 |
assumes "a \<in> carrier R" "b \<in> carrier R" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
484 |
shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
485 |
proof - |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
486 |
have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
487 |
proof |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
488 |
show "(carrier R #> a) <#> (carrier R #> b) \<subseteq> carrier R #> a \<otimes> b" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
489 |
proof |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
490 |
fix x assume "x \<in> (carrier R #> a) <#> (carrier R #> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
491 |
then obtain r1 r2 where r1: "r1 \<in> carrier R" and r2: "r2 \<in> carrier R" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
492 |
and "x = (r1 \<otimes> a) \<otimes> (r2 \<otimes> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
493 |
unfolding set_mult_def r_coset_def by blast |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
494 |
hence "x = (r1 \<otimes> r2) \<otimes> (a \<otimes> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
495 |
by (simp add: assms local.ring_axioms m_lcomm ring.ring_simprules(11)) |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
496 |
thus "x \<in> carrier R #> a \<otimes> b" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
497 |
unfolding r_coset_def using r1 r2 assms by blast |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
498 |
qed |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
499 |
next |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
500 |
show "carrier R #> a \<otimes> b \<subseteq> (carrier R #> a) <#> (carrier R #> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
501 |
proof |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
502 |
fix x assume "x \<in> carrier R #> a \<otimes> b" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
503 |
then obtain r where r: "r \<in> carrier R" "x = r \<otimes> (a \<otimes> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
504 |
unfolding r_coset_def by blast |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
505 |
hence "x = (r \<otimes> a) \<otimes> (\<one> \<otimes> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
506 |
using assms by (simp add: m_assoc) |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
507 |
thus "x \<in> (carrier R #> a) <#> (carrier R #> b)" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
508 |
unfolding set_mult_def r_coset_def using assms r by blast |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
509 |
qed |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
510 |
qed |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
511 |
thus ?thesis |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
512 |
using cgenideal_eq_rcos[of a] cgenideal_eq_rcos[of b] cgenideal_eq_rcos[of "a \<otimes> b"] by simp |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
513 |
qed |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
514 |
|
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
515 |
|
61382 | 516 |
subsection \<open>Prime Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
517 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
518 |
lemma (in ideal) primeidealCD: |
27611 | 519 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
520 |
assumes notprime: "\<not> primeideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
521 |
shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
522 |
proof (rule ccontr, clarsimp) |
29237 | 523 |
interpret cring R by fact |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
524 |
assume InR: "carrier R \<noteq> I" |
44677 | 525 |
and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)" |
526 |
then have I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" |
|
527 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
528 |
have "primeideal I R" |
68464 | 529 |
by (simp add: I_prime InR is_cring is_ideal primeidealI) |
44677 | 530 |
with notprime show False by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
531 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
532 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
533 |
lemma (in ideal) primeidealCE: |
27611 | 534 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
535 |
assumes notprime: "\<not> primeideal I R" |
23383 | 536 |
obtains "carrier R = I" |
537 |
| "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I" |
|
27611 | 538 |
proof - |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30363
diff
changeset
|
539 |
interpret R: cring R by fact |
27611 | 540 |
assume "carrier R = I ==> thesis" |
541 |
and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis" |
|
542 |
then show thesis using primeidealCD [OF R.is_cring notprime] by blast |
|
543 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
544 |
|
63167 | 545 |
text \<open>If \<open>{\<zero>}\<close> is a prime ideal of a commutative ring, the ring is a domain\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
546 |
lemma (in cring) zeroprimeideal_domainI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
547 |
assumes pi: "primeideal {\<zero>} R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
548 |
shows "domain R" |
68464 | 549 |
proof (intro domain.intro is_cring domain_axioms.intro) |
550 |
show "\<one> \<noteq> \<zero>" |
|
551 |
using genideal_one genideal_zero pi primeideal.I_notcarr by force |
|
552 |
show "a = \<zero> \<or> b = \<zero>" if ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R" for a b |
|
553 |
proof - |
|
554 |
interpret primeideal "{\<zero>}" "R" by (rule pi) |
|
555 |
show "a = \<zero> \<or> b = \<zero>" |
|
556 |
using I_prime ab carr by blast |
|
557 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
558 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
559 |
|
44677 | 560 |
corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
561 |
using domain.zeroprimeideal zeroprimeideal_domainI by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
562 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
563 |
|
61382 | 564 |
subsection \<open>Maximal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
565 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
566 |
lemma (in ideal) helper_I_closed: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
567 |
assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R" |
44677 | 568 |
and axI: "a \<otimes> x \<in> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
569 |
shows "a \<otimes> (x \<otimes> y) \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
570 |
proof - |
44677 | 571 |
from axI and carr have "(a \<otimes> x) \<otimes> y \<in> I" |
572 |
by (simp add: I_r_closed) |
|
573 |
also from carr have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)" |
|
574 |
by (simp add: m_assoc) |
|
575 |
finally show "a \<otimes> (x \<otimes> y) \<in> I" . |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
576 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
577 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
578 |
lemma (in ideal) helper_max_prime: |
27611 | 579 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
580 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
581 |
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R" |
27611 | 582 |
proof - |
29237 | 583 |
interpret cring R by fact |
68464 | 584 |
show ?thesis |
585 |
proof (rule idealI, simp_all) |
|
586 |
show "ring R" |
|
587 |
by (simp add: local.ring_axioms) |
|
588 |
show "subgroup {x \<in> carrier R. a \<otimes> x \<in> I} (add_monoid R)" |
|
589 |
by (rule subgroup.intro) (auto simp: r_distr acarr r_minus simp flip: a_inv_def) |
|
590 |
show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk> |
|
591 |
\<Longrightarrow> a \<otimes> (x \<otimes> b) \<in> I" |
|
592 |
using acarr helper_I_closed m_comm by auto |
|
593 |
show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk> |
|
594 |
\<Longrightarrow> a \<otimes> (b \<otimes> x) \<in> I" |
|
595 |
by (simp add: acarr helper_I_closed) |
|
27611 | 596 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
597 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
598 |
|
61382 | 599 |
text \<open>In a cring every maximal ideal is prime\<close> |
63633 | 600 |
lemma (in cring) maximalideal_prime: |
27611 | 601 |
assumes "maximalideal I R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
602 |
shows "primeideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
603 |
proof - |
29237 | 604 |
interpret maximalideal I R by fact |
68464 | 605 |
show ?thesis |
606 |
proof (rule ccontr) |
|
607 |
assume neg: "\<not> primeideal I R" |
|
608 |
then obtain a b where acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" |
|
609 |
and abI: "a \<otimes> b \<in> I" and anI: "a \<notin> I" and bnI: "b \<notin> I" |
|
610 |
using primeidealCE [OF is_cring] |
|
611 |
by (metis I_notcarr) |
|
63040 | 612 |
define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}" |
44677 | 613 |
from is_cring and acarr have idealJ: "ideal J R" |
614 |
unfolding J_def by (rule helper_max_prime) |
|
27611 | 615 |
have IsubJ: "I \<subseteq> J" |
68464 | 616 |
using I_l_closed J_def a_Hcarr acarr by blast |
44677 | 617 |
from abI and acarr bcarr have "b \<in> J" |
618 |
unfolding J_def by fast |
|
619 |
with bnI have JnI: "J \<noteq> I" by fast |
|
68464 | 620 |
have "\<one> \<notin> J" |
621 |
unfolding J_def by (simp add: acarr anI) |
|
44677 | 622 |
then have Jncarr: "J \<noteq> carrier R" by fast |
68464 | 623 |
interpret ideal J R by (rule idealJ) |
27611 | 624 |
have "J = I \<or> J = carrier R" |
68464 | 625 |
by (simp add: I_maximal IsubJ a_subset is_ideal) |
44677 | 626 |
with JnI and Jncarr show False by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
627 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
628 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
629 |
|
35849 | 630 |
|
61382 | 631 |
subsection \<open>Derived Theorems\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
632 |
|
68464 | 633 |
text \<open>A non-zero cring that has only the two trivial ideals is a field\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
634 |
lemma (in cring) trivialideals_fieldI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
635 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}" |
44677 | 636 |
and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
637 |
shows "field R" |
68464 | 638 |
proof (intro cring_fieldI equalityI) |
639 |
show "Units R \<subseteq> carrier R - {\<zero>}" |
|
640 |
by (metis Diff_empty Units_closed Units_r_inv_ex carrnzero l_null one_zeroD subsetI subset_Diff_insert) |
|
641 |
show "carrier R - {\<zero>} \<subseteq> Units R" |
|
642 |
proof |
|
643 |
fix x |
|
644 |
assume xcarr': "x \<in> carrier R - {\<zero>}" |
|
645 |
then have xcarr: "x \<in> carrier R" and xnZ: "x \<noteq> \<zero>" by auto |
|
646 |
from xcarr have xIdl: "ideal (PIdl x) R" |
|
647 |
by (intro cgenideal_ideal) fast |
|
648 |
have "PIdl x \<noteq> {\<zero>}" |
|
649 |
using xcarr xnZ cgenideal_self by blast |
|
650 |
with haveideals have "PIdl x = carrier R" |
|
651 |
by (blast intro!: xIdl) |
|
652 |
then have "\<one> \<in> PIdl x" by simp |
|
653 |
then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" |
|
654 |
unfolding cgenideal_def by blast |
|
655 |
then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x" |
|
656 |
by fast |
|
657 |
have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" |
|
658 |
using m_comm xcarr ycarr ylinv by auto |
|
659 |
with xcarr show "x \<in> Units R" |
|
660 |
unfolding Units_def by fast |
|
661 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
662 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
663 |
|
44677 | 664 |
lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}" |
68464 | 665 |
proof (intro equalityI subsetI) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
666 |
fix I |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
667 |
assume a: "I \<in> {I. ideal I R}" |
44677 | 668 |
then interpret ideal I R by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
669 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
670 |
show "I \<in> {{\<zero>}, carrier R}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
671 |
proof (cases "\<exists>a. a \<in> I - {\<zero>}") |
44677 | 672 |
case True |
673 |
then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>" |
|
674 |
by fast+ |
|
68464 | 675 |
have aUnit: "a \<in> Units R" |
676 |
by (simp add: aI anZ field_Units) |
|
44677 | 677 |
then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv) |
678 |
from aI and aUnit have "a \<otimes> inv a \<in> I" |
|
679 |
by (simp add: I_r_closed del: Units_r_inv) |
|
680 |
then have oneI: "\<one> \<in> I" by (simp add: a[symmetric]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
681 |
have "carrier R \<subseteq> I" |
68464 | 682 |
using oneI one_imp_carrier by auto |
44677 | 683 |
with a_subset have "I = carrier R" by fast |
684 |
then show "I \<in> {{\<zero>}, carrier R}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
685 |
next |
44677 | 686 |
case False |
687 |
then have IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
688 |
have a: "I \<subseteq> {\<zero>}" |
68464 | 689 |
using False by auto |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
690 |
have "\<zero> \<in> I" by simp |
44677 | 691 |
with a have "I = {\<zero>}" by fast |
692 |
then show "I \<in> {{\<zero>}, carrier R}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
693 |
qed |
68464 | 694 |
qed (auto simp: zeroideal oneideal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
695 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
696 |
\<comment>\<open>"Jacobson Theorem 2.2"\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
697 |
lemma (in cring) trivialideals_eq_field: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
698 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
699 |
shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R" |
44677 | 700 |
by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
701 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
702 |
|
61382 | 703 |
text \<open>Like zeroprimeideal for domains\<close> |
44677 | 704 |
lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R" |
68464 | 705 |
proof (intro maximalidealI zeroideal) |
44677 | 706 |
from one_not_zero have "\<one> \<notin> {\<zero>}" by simp |
707 |
with one_closed show "carrier R \<noteq> {\<zero>}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
708 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
709 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
710 |
assume Jideal: "ideal J R" |
44677 | 711 |
then have "J \<in> {I. ideal I R}" by fast |
712 |
with all_ideals show "J = {\<zero>} \<or> J = carrier R" |
|
713 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
714 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
715 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
716 |
lemma (in cring) zeromaximalideal_fieldI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
717 |
assumes zeromax: "maximalideal {\<zero>} R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
718 |
shows "field R" |
68464 | 719 |
proof (intro trivialideals_fieldI maximalideal.I_notcarr[OF zeromax]) |
720 |
have "J = carrier R" if Jn0: "J \<noteq> {\<zero>}" and idealJ: "ideal J R" for J |
|
721 |
proof - |
|
722 |
interpret ideal J R by (rule idealJ) |
|
723 |
have "{\<zero>} \<subseteq> J" |
|
724 |
by force |
|
725 |
from zeromax idealJ this a_subset |
|
726 |
have "J = {\<zero>} \<or> J = carrier R" |
|
727 |
by (rule maximalideal.I_maximal) |
|
728 |
with Jn0 show "J = carrier R" |
|
729 |
by simp |
|
730 |
qed |
|
731 |
then show "{I. ideal I R} = {{\<zero>}, carrier R}" |
|
732 |
by (auto simp: zeroideal oneideal) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
733 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
734 |
|
44677 | 735 |
lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
736 |
using field.zeromaximalideal zeromaximalideal_fieldI by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
737 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
738 |
end |