author | eberlm <eberlm@in.tum.de> |
Fri, 22 Jul 2016 17:35:54 +0200 | |
changeset 63537 | 831816778409 |
parent 63167 | 0909deb8059b |
child 63633 | 2accfb71e33b |
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" |
44677 | 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 |
44677 | 20 |
apply (intro abelian_subgroupI3 abelian_group.intro) |
21 |
apply (rule ideal.axioms, rule ideal_axioms) |
|
22 |
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms) |
|
23 |
apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms) |
|
24 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
25 |
|
44677 | 26 |
lemma (in ideal) is_ideal: "ideal I R" |
27 |
by (rule ideal_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
28 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
29 |
lemma idealI: |
27611 | 30 |
fixes R (structure) |
31 |
assumes "ring R" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
32 |
assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>" |
44677 | 33 |
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I" |
34 |
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
|
35 |
shows "ideal I R" |
27611 | 36 |
proof - |
29237 | 37 |
interpret ring R by fact |
27611 | 38 |
show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI) |
23463 | 39 |
apply (rule a_subgroup) |
40 |
apply (rule is_ring) |
|
41 |
apply (erule (1) I_l_closed) |
|
42 |
apply (erule (1) I_r_closed) |
|
43 |
done |
|
27611 | 44 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
45 |
|
35849 | 46 |
|
61382 | 47 |
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
|
48 |
|
44677 | 49 |
definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79) |
61952 | 50 |
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
|
51 |
|
61382 | 52 |
subsubsection \<open>Principal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
53 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
54 |
locale principalideal = ideal + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
55 |
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
56 |
|
44677 | 57 |
lemma (in principalideal) is_principalideal: "principalideal I R" |
58 |
by (rule principalideal_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
59 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
60 |
lemma principalidealI: |
27611 | 61 |
fixes R (structure) |
62 |
assumes "ideal I R" |
|
47409 | 63 |
and generate: "\<exists>i \<in> carrier R. I = Idl {i}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
64 |
shows "principalideal I R" |
27611 | 65 |
proof - |
29237 | 66 |
interpret ideal I R by fact |
44677 | 67 |
show ?thesis |
68 |
by (intro principalideal.intro principalideal_axioms.intro) |
|
69 |
(rule is_ideal, rule generate) |
|
27611 | 70 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
71 |
|
35849 | 72 |
|
61382 | 73 |
subsubsection \<open>Maximal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
74 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
75 |
locale maximalideal = ideal + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
76 |
assumes I_notcarr: "carrier R \<noteq> I" |
44677 | 77 |
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
|
78 |
|
44677 | 79 |
lemma (in maximalideal) is_maximalideal: "maximalideal I R" |
80 |
by (rule maximalideal_axioms) |
|
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 maximalidealI: |
27611 | 83 |
fixes R |
84 |
assumes "ideal I R" |
|
47409 | 85 |
and I_notcarr: "carrier R \<noteq> I" |
44677 | 86 |
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
|
87 |
shows "maximalideal I R" |
27611 | 88 |
proof - |
29237 | 89 |
interpret ideal I R by fact |
44677 | 90 |
show ?thesis |
91 |
by (intro maximalideal.intro maximalideal_axioms.intro) |
|
92 |
(rule is_ideal, rule I_notcarr, rule I_maximal) |
|
27611 | 93 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
94 |
|
35849 | 95 |
|
61382 | 96 |
subsubsection \<open>Prime Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
97 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
98 |
locale primeideal = ideal + cring + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
99 |
assumes I_notcarr: "carrier R \<noteq> I" |
44677 | 100 |
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
|
101 |
|
44677 | 102 |
lemma (in primeideal) is_primeideal: "primeideal I R" |
103 |
by (rule primeideal_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
104 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
105 |
lemma primeidealI: |
27611 | 106 |
fixes R (structure) |
107 |
assumes "ideal I R" |
|
47409 | 108 |
and "cring R" |
109 |
and I_notcarr: "carrier R \<noteq> I" |
|
44677 | 110 |
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
|
111 |
shows "primeideal I R" |
27611 | 112 |
proof - |
29237 | 113 |
interpret ideal I R by fact |
114 |
interpret cring R by fact |
|
44677 | 115 |
show ?thesis |
116 |
by (intro primeideal.intro primeideal_axioms.intro) |
|
117 |
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime) |
|
27611 | 118 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
119 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
120 |
lemma primeidealI2: |
27611 | 121 |
fixes R (structure) |
122 |
assumes "additive_subgroup I R" |
|
47409 | 123 |
and "cring R" |
124 |
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I" |
|
44677 | 125 |
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I" |
126 |
and I_notcarr: "carrier R \<noteq> I" |
|
127 |
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
|
128 |
shows "primeideal I R" |
27611 | 129 |
proof - |
29240 | 130 |
interpret additive_subgroup I R by fact |
29237 | 131 |
interpret cring R by fact |
27611 | 132 |
show ?thesis apply (intro_locales) |
133 |
apply (intro ideal_axioms.intro) |
|
134 |
apply (erule (1) I_l_closed) |
|
135 |
apply (erule (1) I_r_closed) |
|
136 |
apply (intro primeideal_axioms.intro) |
|
137 |
apply (rule I_notcarr) |
|
138 |
apply (erule (2) I_prime) |
|
139 |
done |
|
140 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
141 |
|
35849 | 142 |
|
61382 | 143 |
subsection \<open>Special Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
144 |
|
44677 | 145 |
lemma (in ring) zeroideal: "ideal {\<zero>} R" |
146 |
apply (intro idealI subgroup.intro) |
|
147 |
apply (rule is_ring) |
|
148 |
apply simp+ |
|
149 |
apply (fold a_inv_def, simp) |
|
150 |
apply simp+ |
|
151 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
152 |
|
44677 | 153 |
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
|
154 |
by (rule idealI) (auto intro: is_ring add.subgroupI) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
155 |
|
44677 | 156 |
lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R" |
157 |
apply (intro primeidealI) |
|
158 |
apply (rule zeroideal) |
|
159 |
apply (rule domain.axioms, rule domain_axioms) |
|
160 |
defer 1 |
|
161 |
apply (simp add: integral) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
162 |
proof (rule ccontr, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
163 |
assume "carrier R = {\<zero>}" |
44677 | 164 |
then have "\<one> = \<zero>" by (rule one_zeroI) |
165 |
with one_not_zero show False by simp |
|
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 |
|
61382 | 169 |
subsection \<open>General Ideal Properies\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
170 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
171 |
lemma (in ideal) one_imp_carrier: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
172 |
assumes I_one_closed: "\<one> \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
173 |
shows "I = carrier R" |
44677 | 174 |
apply (rule) |
175 |
apply (rule) |
|
176 |
apply (rule a_Hcarr, simp) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
177 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
178 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
179 |
assume xcarr: "x \<in> carrier R" |
44677 | 180 |
with I_one_closed have "x \<otimes> \<one> \<in> I" by (intro I_l_closed) |
181 |
with xcarr show "x \<in> I" by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
182 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
183 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
184 |
lemma (in ideal) Icarr: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
185 |
assumes iI: "i \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
186 |
shows "i \<in> carrier R" |
44677 | 187 |
using iI by (rule a_Hcarr) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
188 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
189 |
|
61382 | 190 |
subsection \<open>Intersection of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
191 |
|
61506 | 192 |
paragraph \<open>Intersection of two ideals\<close> |
193 |
text \<open>The intersection of any two ideals is again an ideal in @{term R}\<close> |
|
194 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
195 |
lemma (in ring) i_intersect: |
27611 | 196 |
assumes "ideal I R" |
197 |
assumes "ideal J R" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
198 |
shows "ideal (I \<inter> J) R" |
27611 | 199 |
proof - |
29237 | 200 |
interpret ideal I R by fact |
29240 | 201 |
interpret ideal J R by fact |
27611 | 202 |
show ?thesis |
44677 | 203 |
apply (intro idealI subgroup.intro) |
204 |
apply (rule is_ring) |
|
205 |
apply (force simp add: a_subset) |
|
206 |
apply (simp add: a_inv_def[symmetric]) |
|
207 |
apply simp |
|
208 |
apply (simp add: a_inv_def[symmetric]) |
|
209 |
apply (clarsimp, rule) |
|
210 |
apply (fast intro: ideal.I_l_closed ideal.intro assms)+ |
|
211 |
apply (clarsimp, rule) |
|
212 |
apply (fast intro: ideal.I_r_closed ideal.intro assms)+ |
|
213 |
done |
|
27611 | 214 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
215 |
|
61382 | 216 |
text \<open>The intersection of any Number of Ideals is again |
217 |
an Ideal in @{term R}\<close> |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
218 |
lemma (in ring) i_Intersect: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
219 |
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
220 |
and notempty: "S \<noteq> {}" |
61952 | 221 |
shows "ideal (\<Inter>S) R" |
44677 | 222 |
apply (unfold_locales) |
223 |
apply (simp_all add: Inter_eq) |
|
224 |
apply rule unfolding mem_Collect_eq defer 1 |
|
225 |
apply rule defer 1 |
|
226 |
apply rule defer 1 |
|
227 |
apply (fold a_inv_def, rule) defer 1 |
|
228 |
apply rule defer 1 |
|
229 |
apply rule defer 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
230 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
232 |
assume "\<forall>I\<in>S. x \<in> I" |
44677 | 233 |
then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
assume "\<forall>I\<in>S. y \<in> I" |
44677 | 235 |
then have yI: "\<And>I. I \<in> S \<Longrightarrow> y \<in> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
236 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
237 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
238 |
assume JS: "J \<in> S" |
29237 | 239 |
interpret ideal J R by (rule Sideals[OF JS]) |
44677 | 240 |
from xI[OF JS] and yI[OF JS] show "x \<oplus> y \<in> J" by (rule a_closed) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
241 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
242 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
243 |
assume JS: "J \<in> S" |
29237 | 244 |
interpret ideal J R by (rule Sideals[OF JS]) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
245 |
show "\<zero> \<in> J" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
246 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
247 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
248 |
assume "\<forall>I\<in>S. x \<in> I" |
44677 | 249 |
then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
250 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
251 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
252 |
assume JS: "J \<in> S" |
29237 | 253 |
interpret ideal J R by (rule Sideals[OF JS]) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
254 |
|
44677 | 255 |
from xI[OF JS] show "\<ominus> x \<in> J" by (rule a_inv_closed) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
256 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
258 |
assume "\<forall>I\<in>S. x \<in> I" |
44677 | 259 |
then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
260 |
assume ycarr: "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
261 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
263 |
assume JS: "J \<in> S" |
29237 | 264 |
interpret ideal J R by (rule Sideals[OF JS]) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
265 |
|
44677 | 266 |
from xI[OF JS] and ycarr show "y \<otimes> x \<in> J" by (rule I_l_closed) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
267 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
268 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
269 |
assume "\<forall>I\<in>S. x \<in> I" |
44677 | 270 |
then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
271 |
assume ycarr: "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
272 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
273 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
274 |
assume JS: "J \<in> S" |
29237 | 275 |
interpret ideal J R by (rule Sideals[OF JS]) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
276 |
|
44677 | 277 |
from xI[OF JS] and ycarr show "x \<otimes> y \<in> J" by (rule I_r_closed) |
44106 | 278 |
next |
279 |
fix x |
|
280 |
assume "\<forall>I\<in>S. x \<in> I" |
|
44677 | 281 |
then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp |
44106 | 282 |
|
283 |
from notempty have "\<exists>I0. I0 \<in> S" by blast |
|
44677 | 284 |
then obtain I0 where I0S: "I0 \<in> S" by auto |
44106 | 285 |
|
286 |
interpret ideal I0 R by (rule Sideals[OF I0S]) |
|
287 |
||
288 |
from xI[OF I0S] have "x \<in> I0" . |
|
44677 | 289 |
with a_subset show "x \<in> carrier R" by fast |
44106 | 290 |
next |
291 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
292 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
293 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
|
61382 | 295 |
subsection \<open>Addition of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
297 |
lemma (in ring) add_ideals: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
298 |
assumes idealI: "ideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
and idealJ: "ideal J R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
shows "ideal (I <+> J) R" |
44677 | 301 |
apply (rule ideal.intro) |
302 |
apply (rule add_additive_subgroups) |
|
303 |
apply (intro ideal.axioms[OF idealI]) |
|
304 |
apply (intro ideal.axioms[OF idealJ]) |
|
305 |
apply (rule is_ring) |
|
306 |
apply (rule ideal_axioms.intro) |
|
307 |
apply (simp add: set_add_defs, clarsimp) defer 1 |
|
308 |
apply (simp add: set_add_defs, clarsimp) defer 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
309 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
310 |
fix x i j |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
311 |
assume xcarr: "x \<in> carrier R" |
44677 | 312 |
and iI: "i \<in> I" |
313 |
and jJ: "j \<in> J" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] |
44677 | 315 |
have c: "(i \<oplus> j) \<otimes> x = (i \<otimes> x) \<oplus> (j \<otimes> x)" |
316 |
by algebra |
|
317 |
from xcarr and iI have a: "i \<otimes> x \<in> I" |
|
318 |
by (simp add: ideal.I_r_closed[OF idealI]) |
|
319 |
from xcarr and jJ have b: "j \<otimes> x \<in> J" |
|
320 |
by (simp add: ideal.I_r_closed[OF idealJ]) |
|
321 |
from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. (i \<oplus> j) \<otimes> x = ha \<oplus> ka" |
|
322 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
323 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
324 |
fix x i j |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
assume xcarr: "x \<in> carrier R" |
44677 | 326 |
and iI: "i \<in> I" |
327 |
and jJ: "j \<in> J" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
328 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] |
44677 | 329 |
have c: "x \<otimes> (i \<oplus> j) = (x \<otimes> i) \<oplus> (x \<otimes> j)" by algebra |
330 |
from xcarr and iI have a: "x \<otimes> i \<in> I" |
|
331 |
by (simp add: ideal.I_l_closed[OF idealI]) |
|
332 |
from xcarr and jJ have b: "x \<otimes> j \<in> J" |
|
333 |
by (simp add: ideal.I_l_closed[OF idealJ]) |
|
334 |
from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. x \<otimes> (i \<oplus> j) = ha \<oplus> ka" |
|
335 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
336 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
337 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
338 |
|
61382 | 339 |
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
|
340 |
|
61382 | 341 |
text \<open>@{term genideal} generates an ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
342 |
lemma (in ring) genideal_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
343 |
assumes Scarr: "S \<subseteq> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
344 |
shows "ideal (Idl S) R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
unfolding genideal_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
346 |
proof (rule i_Intersect, fast, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
347 |
from oneideal and Scarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
348 |
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
|
349 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
350 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
351 |
lemma (in ring) genideal_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
352 |
assumes "S \<subseteq> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
353 |
shows "S \<subseteq> Idl S" |
44677 | 354 |
unfolding genideal_def by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
355 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
lemma (in ring) genideal_self': |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
357 |
assumes carr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
358 |
shows "i \<in> Idl {i}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
359 |
proof - |
44677 | 360 |
from carr have "{i} \<subseteq> Idl {i}" by (fast intro!: genideal_self) |
361 |
then show "i \<in> Idl {i}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
362 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
363 |
|
61382 | 364 |
text \<open>@{term genideal} generates the minimal ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
365 |
lemma (in ring) genideal_minimal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
366 |
assumes a: "ideal I R" |
44677 | 367 |
and b: "S \<subseteq> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
368 |
shows "Idl S \<subseteq> I" |
44677 | 369 |
unfolding genideal_def by rule (elim InterD, simp add: a b) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
370 |
|
61382 | 371 |
text \<open>Generated ideals and subsets\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
372 |
lemma (in ring) Idl_subset_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
373 |
assumes Iideal: "ideal I R" |
44677 | 374 |
and Hcarr: "H \<subseteq> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
375 |
shows "(Idl H \<subseteq> I) = (H \<subseteq> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
376 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
377 |
assume a: "Idl H \<subseteq> I" |
23350 | 378 |
from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self) |
44677 | 379 |
with a show "H \<subseteq> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
380 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
381 |
fix x |
47409 | 382 |
assume "H \<subseteq> I" |
383 |
with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast |
|
44677 | 384 |
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
|
385 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
386 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
387 |
lemma (in ring) subset_Idl_subset: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
388 |
assumes Icarr: "I \<subseteq> carrier R" |
44677 | 389 |
and HI: "H \<subseteq> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
390 |
shows "Idl H \<subseteq> Idl I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
391 |
proof - |
44677 | 392 |
from HI and genideal_self[OF Icarr] have HIdlI: "H \<subseteq> Idl I" |
393 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
394 |
|
44677 | 395 |
from Icarr have Iideal: "ideal (Idl I) R" |
396 |
by (rule genideal_ideal) |
|
397 |
from HI and Icarr have "H \<subseteq> carrier R" |
|
398 |
by fast |
|
399 |
with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)" |
|
400 |
by (rule Idl_subset_ideal[symmetric]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
401 |
|
44677 | 402 |
with HIdlI show "Idl H \<subseteq> Idl I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
403 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
404 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
405 |
lemma (in ring) Idl_subset_ideal': |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
406 |
assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
407 |
shows "(Idl {a} \<subseteq> Idl {b}) = (a \<in> Idl {b})" |
44677 | 408 |
apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"]) |
409 |
apply (fast intro: bcarr, fast intro: acarr) |
|
410 |
apply fast |
|
411 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
412 |
|
44677 | 413 |
lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}" |
414 |
apply rule |
|
415 |
apply (rule genideal_minimal[OF zeroideal], simp) |
|
416 |
apply (simp add: genideal_self') |
|
417 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
418 |
|
44677 | 419 |
lemma (in ring) genideal_one: "Idl {\<one>} = carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
420 |
proof - |
44677 | 421 |
interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
422 |
show "Idl {\<one>} = carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
423 |
apply (rule, rule a_subset) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
424 |
apply (simp add: one_imp_carrier genideal_self') |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
425 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
426 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
427 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
428 |
|
61382 | 429 |
text \<open>Generation of Principal Ideals in Commutative Rings\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
430 |
|
44677 | 431 |
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
|
432 |
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
|
433 |
|
61382 | 434 |
text \<open>genhideal (?) really generates an ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
435 |
lemma (in cring) cgenideal_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
436 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
437 |
shows "ideal (PIdl a) R" |
44677 | 438 |
apply (unfold cgenideal_def) |
439 |
apply (rule idealI[OF is_ring]) |
|
440 |
apply (rule subgroup.intro) |
|
441 |
apply simp_all |
|
442 |
apply (blast intro: acarr) |
|
443 |
apply clarsimp defer 1 |
|
444 |
defer 1 |
|
445 |
apply (fold a_inv_def, clarsimp) defer 1 |
|
446 |
apply clarsimp defer 1 |
|
447 |
apply clarsimp defer 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
448 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
449 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
450 |
assume xcarr: "x \<in> carrier R" |
44677 | 451 |
and ycarr: "y \<in> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
452 |
note carr = acarr xcarr ycarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
453 |
|
44677 | 454 |
from carr have "x \<otimes> a \<oplus> y \<otimes> a = (x \<oplus> y) \<otimes> a" |
455 |
by (simp add: l_distr) |
|
456 |
with carr show "\<exists>z. x \<otimes> a \<oplus> y \<otimes> a = z \<otimes> a \<and> z \<in> carrier R" |
|
457 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
458 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
459 |
from l_null[OF acarr, symmetric] and zero_closed |
44677 | 460 |
show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
461 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
462 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
463 |
assume xcarr: "x \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
464 |
note carr = acarr xcarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
465 |
|
44677 | 466 |
from carr have "\<ominus> (x \<otimes> a) = (\<ominus> x) \<otimes> a" |
467 |
by (simp add: l_minus) |
|
468 |
with carr show "\<exists>z. \<ominus> (x \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" |
|
469 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
470 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
471 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
472 |
assume xcarr: "x \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
473 |
and ycarr: "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
474 |
note carr = acarr xcarr ycarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
475 |
|
44677 | 476 |
from carr have "y \<otimes> a \<otimes> x = (y \<otimes> x) \<otimes> a" |
477 |
by (simp add: m_assoc) (simp add: m_comm) |
|
478 |
with carr show "\<exists>z. y \<otimes> a \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" |
|
479 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
480 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
481 |
fix x y |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
482 |
assume xcarr: "x \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
483 |
and ycarr: "y \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
484 |
note carr = acarr xcarr ycarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
485 |
|
44677 | 486 |
from carr have "x \<otimes> (y \<otimes> a) = (x \<otimes> y) \<otimes> a" |
487 |
by (simp add: m_assoc) |
|
488 |
with carr show "\<exists>z. x \<otimes> (y \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" |
|
489 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
490 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
491 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
492 |
lemma (in ring) cgenideal_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
493 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
494 |
shows "i \<in> PIdl i" |
44677 | 495 |
unfolding cgenideal_def |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
496 |
proof simp |
44677 | 497 |
from icarr have "i = \<one> \<otimes> i" |
498 |
by simp |
|
499 |
with icarr show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R" |
|
500 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
501 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
502 |
|
61382 | 503 |
text \<open>@{const "cgenideal"} is minimal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
504 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
505 |
lemma (in ring) cgenideal_minimal: |
27611 | 506 |
assumes "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
507 |
assumes aJ: "a \<in> J" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
508 |
shows "PIdl a \<subseteq> J" |
27611 | 509 |
proof - |
29240 | 510 |
interpret ideal J R by fact |
44677 | 511 |
show ?thesis |
512 |
unfolding cgenideal_def |
|
27611 | 513 |
apply rule |
514 |
apply clarify |
|
515 |
using aJ |
|
516 |
apply (erule I_l_closed) |
|
517 |
done |
|
518 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
519 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
520 |
lemma (in cring) cgenideal_eq_genideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
521 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
522 |
shows "PIdl i = Idl {i}" |
44677 | 523 |
apply rule |
524 |
apply (intro cgenideal_minimal) |
|
525 |
apply (rule genideal_ideal, fast intro: icarr) |
|
526 |
apply (rule genideal_self', fast intro: icarr) |
|
527 |
apply (intro genideal_minimal) |
|
528 |
apply (rule cgenideal_ideal [OF icarr]) |
|
529 |
apply (simp, rule cgenideal_self [OF icarr]) |
|
530 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
531 |
|
44677 | 532 |
lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i" |
533 |
unfolding cgenideal_def r_coset_def by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
534 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
535 |
lemma (in cring) cgenideal_is_principalideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
536 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
537 |
shows "principalideal (PIdl i) R" |
44677 | 538 |
apply (rule principalidealI) |
539 |
apply (rule cgenideal_ideal [OF icarr]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
540 |
proof - |
44677 | 541 |
from icarr have "PIdl i = Idl {i}" |
542 |
by (rule cgenideal_eq_genideal) |
|
543 |
with icarr show "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" |
|
544 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
545 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
546 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
547 |
|
61382 | 548 |
subsection \<open>Union of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
549 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
550 |
lemma (in ring) union_genideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
551 |
assumes idealI: "ideal I R" |
44677 | 552 |
and idealJ: "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
553 |
shows "Idl (I \<union> J) = I <+> J" |
44677 | 554 |
apply rule |
555 |
apply (rule ring.genideal_minimal) |
|
556 |
apply (rule is_ring) |
|
557 |
apply (rule add_ideals[OF idealI idealJ]) |
|
558 |
apply (rule) |
|
559 |
apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1 |
|
560 |
apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
561 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
562 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
563 |
assume xI: "x \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
564 |
have ZJ: "\<zero> \<in> J" |
44677 | 565 |
by (intro additive_subgroup.zero_closed) (rule ideal.axioms[OF idealJ]) |
566 |
from ideal.Icarr[OF idealI xI] have "x = x \<oplus> \<zero>" |
|
567 |
by algebra |
|
568 |
with xI and ZJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" |
|
569 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
570 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
571 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
572 |
assume xJ: "x \<in> J" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
573 |
have ZI: "\<zero> \<in> I" |
44677 | 574 |
by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI]) |
575 |
from ideal.Icarr[OF idealJ xJ] have "x = \<zero> \<oplus> x" |
|
576 |
by algebra |
|
577 |
with ZI and xJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" |
|
578 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
579 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
580 |
fix i j K |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
581 |
assume iI: "i \<in> I" |
44677 | 582 |
and jJ: "j \<in> J" |
583 |
and idealK: "ideal K R" |
|
584 |
and IK: "I \<subseteq> K" |
|
585 |
and JK: "J \<subseteq> K" |
|
586 |
from iI and IK have iK: "i \<in> K" by fast |
|
587 |
from jJ and JK have jK: "j \<in> K" by fast |
|
588 |
from iK and jK show "i \<oplus> j \<in> K" |
|
589 |
by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
590 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
591 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
592 |
|
61382 | 593 |
subsection \<open>Properties of Principal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
594 |
|
63167 | 595 |
text \<open>\<open>\<zero>\<close> generates the zero ideal\<close> |
44677 | 596 |
lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}" |
597 |
apply rule |
|
598 |
apply (simp add: genideal_minimal zeroideal) |
|
599 |
apply (fast intro!: genideal_self) |
|
600 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
601 |
|
63167 | 602 |
text \<open>\<open>\<one>\<close> generates the unit ideal\<close> |
44677 | 603 |
lemma (in ring) one_genideal: "Idl {\<one>} = carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
604 |
proof - |
44677 | 605 |
have "\<one> \<in> Idl {\<one>}" |
606 |
by (simp add: genideal_self') |
|
607 |
then show "Idl {\<one>} = carrier R" |
|
608 |
by (intro ideal.one_imp_carrier) (fast intro: genideal_ideal) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
609 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
610 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
611 |
|
61382 | 612 |
text \<open>The zero ideal is a principal ideal\<close> |
44677 | 613 |
corollary (in ring) zeropideal: "principalideal {\<zero>} R" |
614 |
apply (rule principalidealI) |
|
615 |
apply (rule zeroideal) |
|
616 |
apply (blast intro!: zero_genideal[symmetric]) |
|
617 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
618 |
|
61382 | 619 |
text \<open>The unit ideal is a principal ideal\<close> |
44677 | 620 |
corollary (in ring) onepideal: "principalideal (carrier R) R" |
621 |
apply (rule principalidealI) |
|
622 |
apply (rule oneideal) |
|
623 |
apply (blast intro!: one_genideal[symmetric]) |
|
624 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
625 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
626 |
|
61382 | 627 |
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
|
628 |
lemma (in principalideal) rcos_generate: |
27611 | 629 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
630 |
shows "\<exists>x\<in>I. I = carrier R #> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
631 |
proof - |
29237 | 632 |
interpret cring R by fact |
44677 | 633 |
from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}" |
634 |
by fast+ |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
635 |
|
44677 | 636 |
from icarr and genideal_self[of "{i}"] have "i \<in> Idl {i}" |
637 |
by fast |
|
638 |
then have iI: "i \<in> I" by (simp add: I1) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
639 |
|
44677 | 640 |
from I1 icarr have I2: "I = PIdl i" |
641 |
by (simp add: cgenideal_eq_genideal) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
642 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
643 |
have "PIdl i = carrier R #> i" |
44677 | 644 |
unfolding cgenideal_def r_coset_def by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
645 |
|
44677 | 646 |
with I2 have "I = carrier R #> i" |
647 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
648 |
|
44677 | 649 |
with iI show "\<exists>x\<in>I. I = carrier R #> x" |
650 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
651 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
652 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
653 |
|
61382 | 654 |
subsection \<open>Prime Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
655 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
656 |
lemma (in ideal) primeidealCD: |
27611 | 657 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
658 |
assumes notprime: "\<not> primeideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
659 |
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
|
660 |
proof (rule ccontr, clarsimp) |
29237 | 661 |
interpret cring R by fact |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
662 |
assume InR: "carrier R \<noteq> I" |
44677 | 663 |
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)" |
664 |
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" |
|
665 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
666 |
have "primeideal I R" |
44677 | 667 |
apply (rule primeideal.intro [OF is_ideal is_cring]) |
668 |
apply (rule primeideal_axioms.intro) |
|
669 |
apply (rule InR) |
|
670 |
apply (erule (2) I_prime) |
|
671 |
done |
|
672 |
with notprime show False by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
673 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
674 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
675 |
lemma (in ideal) primeidealCE: |
27611 | 676 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
677 |
assumes notprime: "\<not> primeideal I R" |
23383 | 678 |
obtains "carrier R = I" |
679 |
| "\<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 | 680 |
proof - |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30363
diff
changeset
|
681 |
interpret R: cring R by fact |
27611 | 682 |
assume "carrier R = I ==> thesis" |
683 |
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" |
|
684 |
then show thesis using primeidealCD [OF R.is_cring notprime] by blast |
|
685 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
686 |
|
63167 | 687 |
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
|
688 |
lemma (in cring) zeroprimeideal_domainI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
689 |
assumes pi: "primeideal {\<zero>} R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
690 |
shows "domain R" |
44677 | 691 |
apply (rule domain.intro, rule is_cring) |
692 |
apply (rule domain_axioms.intro) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
693 |
proof (rule ccontr, simp) |
29237 | 694 |
interpret primeideal "{\<zero>}" "R" by (rule pi) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
695 |
assume "\<one> = \<zero>" |
44677 | 696 |
then have "carrier R = {\<zero>}" by (rule one_zeroD) |
697 |
from this[symmetric] and I_notcarr show False |
|
698 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
699 |
next |
29237 | 700 |
interpret primeideal "{\<zero>}" "R" by (rule pi) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
701 |
fix a b |
44677 | 702 |
assume ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R" |
703 |
from ab have abI: "a \<otimes> b \<in> {\<zero>}" |
|
704 |
by fast |
|
705 |
with carr have "a \<in> {\<zero>} \<or> b \<in> {\<zero>}" |
|
706 |
by (rule I_prime) |
|
707 |
then show "a = \<zero> \<or> b = \<zero>" by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
708 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
709 |
|
44677 | 710 |
corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R" |
711 |
apply rule |
|
712 |
apply (erule domain.zeroprimeideal) |
|
713 |
apply (erule zeroprimeideal_domainI) |
|
714 |
done |
|
20318
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 |
|
61382 | 717 |
subsection \<open>Maximal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
718 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
719 |
lemma (in ideal) helper_I_closed: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
720 |
assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R" |
44677 | 721 |
and axI: "a \<otimes> x \<in> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
722 |
shows "a \<otimes> (x \<otimes> y) \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
723 |
proof - |
44677 | 724 |
from axI and carr have "(a \<otimes> x) \<otimes> y \<in> I" |
725 |
by (simp add: I_r_closed) |
|
726 |
also from carr have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)" |
|
727 |
by (simp add: m_assoc) |
|
728 |
finally show "a \<otimes> (x \<otimes> y) \<in> I" . |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
729 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
730 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
731 |
lemma (in ideal) helper_max_prime: |
27611 | 732 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
733 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
734 |
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R" |
27611 | 735 |
proof - |
29237 | 736 |
interpret cring R by fact |
27611 | 737 |
show ?thesis apply (rule idealI) |
738 |
apply (rule cring.axioms[OF is_cring]) |
|
739 |
apply (rule subgroup.intro) |
|
740 |
apply (simp, fast) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
741 |
apply clarsimp apply (simp add: r_distr acarr) |
27611 | 742 |
apply (simp add: acarr) |
743 |
apply (simp add: a_inv_def[symmetric], clarify) defer 1 |
|
744 |
apply clarsimp defer 1 |
|
745 |
apply (fast intro!: helper_I_closed acarr) |
|
746 |
proof - |
|
747 |
fix x |
|
748 |
assume xcarr: "x \<in> carrier R" |
|
749 |
and ax: "a \<otimes> x \<in> I" |
|
750 |
from ax and acarr xcarr |
|
751 |
have "\<ominus>(a \<otimes> x) \<in> I" by simp |
|
752 |
also from acarr xcarr |
|
753 |
have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra |
|
44677 | 754 |
finally show "a \<otimes> (\<ominus>x) \<in> I" . |
755 |
from acarr have "a \<otimes> \<zero> = \<zero>" by simp |
|
27611 | 756 |
next |
757 |
fix x y |
|
758 |
assume xcarr: "x \<in> carrier R" |
|
759 |
and ycarr: "y \<in> carrier R" |
|
760 |
and ayI: "a \<otimes> y \<in> I" |
|
44677 | 761 |
from ayI and acarr xcarr ycarr have "a \<otimes> (y \<otimes> x) \<in> I" |
762 |
by (simp add: helper_I_closed) |
|
763 |
moreover |
|
764 |
from xcarr ycarr have "y \<otimes> x = x \<otimes> y" |
|
765 |
by (simp add: m_comm) |
|
27611 | 766 |
ultimately |
767 |
show "a \<otimes> (x \<otimes> y) \<in> I" by simp |
|
768 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
769 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
770 |
|
61382 | 771 |
text \<open>In a cring every maximal ideal is prime\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
772 |
lemma (in cring) maximalideal_is_prime: |
27611 | 773 |
assumes "maximalideal I R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
774 |
shows "primeideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
775 |
proof - |
29237 | 776 |
interpret maximalideal I R by fact |
27611 | 777 |
show ?thesis apply (rule ccontr) |
778 |
apply (rule primeidealCE) |
|
779 |
apply (rule is_cring) |
|
780 |
apply assumption |
|
781 |
apply (simp add: I_notcarr) |
|
782 |
proof - |
|
783 |
assume "\<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" |
|
44677 | 784 |
then obtain a b where |
785 |
acarr: "a \<in> carrier R" and |
|
786 |
bcarr: "b \<in> carrier R" and |
|
787 |
abI: "a \<otimes> b \<in> I" and |
|
788 |
anI: "a \<notin> I" and |
|
789 |
bnI: "b \<notin> I" by fast |
|
63040 | 790 |
define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}" |
27611 | 791 |
|
44677 | 792 |
from is_cring and acarr have idealJ: "ideal J R" |
793 |
unfolding J_def by (rule helper_max_prime) |
|
27611 | 794 |
|
795 |
have IsubJ: "I \<subseteq> J" |
|
796 |
proof |
|
797 |
fix x |
|
798 |
assume xI: "x \<in> I" |
|
44677 | 799 |
with acarr have "a \<otimes> x \<in> I" |
800 |
by (intro I_l_closed) |
|
801 |
with xI[THEN a_Hcarr] show "x \<in> J" |
|
802 |
unfolding J_def by fast |
|
27611 | 803 |
qed |
804 |
||
44677 | 805 |
from abI and acarr bcarr have "b \<in> J" |
806 |
unfolding J_def by fast |
|
807 |
with bnI have JnI: "J \<noteq> I" by fast |
|
27611 | 808 |
from acarr |
809 |
have "a = a \<otimes> \<one>" by algebra |
|
44677 | 810 |
with anI have "a \<otimes> \<one> \<notin> I" by simp |
811 |
with one_closed have "\<one> \<notin> J" |
|
812 |
unfolding J_def by fast |
|
813 |
then have Jncarr: "J \<noteq> carrier R" by fast |
|
27611 | 814 |
|
29237 | 815 |
interpret ideal J R by (rule idealJ) |
27611 | 816 |
|
817 |
have "J = I \<or> J = carrier R" |
|
818 |
apply (intro I_maximal) |
|
819 |
apply (rule idealJ) |
|
820 |
apply (rule IsubJ) |
|
821 |
apply (rule a_subset) |
|
822 |
done |
|
823 |
||
44677 | 824 |
with JnI and Jncarr show False by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
825 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
826 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
827 |
|
35849 | 828 |
|
61382 | 829 |
subsection \<open>Derived Theorems\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
830 |
|
63167 | 831 |
\<comment>"A non-zero cring that has only the two trivial ideals is a field" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
832 |
lemma (in cring) trivialideals_fieldI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
833 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}" |
44677 | 834 |
and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
835 |
shows "field R" |
44677 | 836 |
apply (rule cring_fieldI) |
837 |
apply (rule, rule, rule) |
|
838 |
apply (erule Units_closed) |
|
839 |
defer 1 |
|
840 |
apply rule |
|
841 |
defer 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
842 |
proof (rule ccontr, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
843 |
assume zUnit: "\<zero> \<in> Units R" |
44677 | 844 |
then have a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv) |
845 |
from zUnit have "\<zero> \<otimes> inv \<zero> = \<zero>" |
|
846 |
by (intro l_null) (rule Units_inv_closed) |
|
847 |
with a[symmetric] have "\<one> = \<zero>" by simp |
|
848 |
then have "carrier R = {\<zero>}" by (rule one_zeroD) |
|
849 |
with carrnzero show False by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
850 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
851 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
852 |
assume xcarr': "x \<in> carrier R - {\<zero>}" |
44677 | 853 |
then have xcarr: "x \<in> carrier R" by fast |
854 |
from xcarr' have xnZ: "x \<noteq> \<zero>" by fast |
|
855 |
from xcarr have xIdl: "ideal (PIdl x) R" |
|
856 |
by (intro cgenideal_ideal) fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
857 |
|
44677 | 858 |
from xcarr have "x \<in> PIdl x" |
859 |
by (intro cgenideal_self) fast |
|
860 |
with xnZ have "PIdl x \<noteq> {\<zero>}" by fast |
|
861 |
with haveideals have "PIdl x = carrier R" |
|
862 |
by (blast intro!: xIdl) |
|
863 |
then have "\<one> \<in> PIdl x" by simp |
|
864 |
then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" |
|
865 |
unfolding cgenideal_def by blast |
|
866 |
then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x" |
|
867 |
by fast+ |
|
868 |
from ylinv and xcarr ycarr have yrinv: "\<one> = x \<otimes> y" |
|
869 |
by (simp add: m_comm) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
870 |
from ycarr and ylinv[symmetric] and yrinv[symmetric] |
44677 | 871 |
have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast |
872 |
with xcarr show "x \<in> Units R" |
|
873 |
unfolding Units_def by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
874 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
875 |
|
44677 | 876 |
lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}" |
877 |
apply (rule, rule) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
878 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
879 |
fix I |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
880 |
assume a: "I \<in> {I. ideal I R}" |
44677 | 881 |
then interpret ideal I R by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
882 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
883 |
show "I \<in> {{\<zero>}, carrier R}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
884 |
proof (cases "\<exists>a. a \<in> I - {\<zero>}") |
44677 | 885 |
case True |
886 |
then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>" |
|
887 |
by fast+ |
|
888 |
from aI[THEN a_Hcarr] anZ have aUnit: "a \<in> Units R" |
|
889 |
by (simp add: field_Units) |
|
890 |
then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv) |
|
891 |
from aI and aUnit have "a \<otimes> inv a \<in> I" |
|
892 |
by (simp add: I_r_closed del: Units_r_inv) |
|
893 |
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
|
894 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
895 |
have "carrier R \<subseteq> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
896 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
897 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
898 |
assume xcarr: "x \<in> carrier R" |
44677 | 899 |
with oneI have "\<one> \<otimes> x \<in> I" by (rule I_r_closed) |
900 |
with xcarr show "x \<in> I" by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
901 |
qed |
44677 | 902 |
with a_subset have "I = carrier R" by fast |
903 |
then show "I \<in> {{\<zero>}, carrier R}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
904 |
next |
44677 | 905 |
case False |
906 |
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
|
907 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
908 |
have a: "I \<subseteq> {\<zero>}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
909 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
910 |
fix x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
911 |
assume "x \<in> I" |
44677 | 912 |
then have "x = \<zero>" by (rule IZ) |
913 |
then show "x \<in> {\<zero>}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
914 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
915 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
916 |
have "\<zero> \<in> I" by simp |
44677 | 917 |
then have "{\<zero>} \<subseteq> I" by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
918 |
|
44677 | 919 |
with a have "I = {\<zero>}" by fast |
920 |
then show "I \<in> {{\<zero>}, carrier R}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
921 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
922 |
qed (simp add: zeroideal oneideal) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
923 |
|
63167 | 924 |
\<comment>"Jacobson Theorem 2.2" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
925 |
lemma (in cring) trivialideals_eq_field: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
926 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
927 |
shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R" |
44677 | 928 |
by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
929 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
930 |
|
61382 | 931 |
text \<open>Like zeroprimeideal for domains\<close> |
44677 | 932 |
lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R" |
933 |
apply (rule maximalidealI) |
|
934 |
apply (rule zeroideal) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
935 |
proof- |
44677 | 936 |
from one_not_zero have "\<one> \<notin> {\<zero>}" by simp |
937 |
with one_closed show "carrier R \<noteq> {\<zero>}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
938 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
939 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
940 |
assume Jideal: "ideal J R" |
44677 | 941 |
then have "J \<in> {I. ideal I R}" by fast |
942 |
with all_ideals show "J = {\<zero>} \<or> J = carrier R" |
|
943 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
944 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
945 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
946 |
lemma (in cring) zeromaximalideal_fieldI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
947 |
assumes zeromax: "maximalideal {\<zero>} R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
948 |
shows "field R" |
44677 | 949 |
apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax]) |
950 |
apply rule apply clarsimp defer 1 |
|
951 |
apply (simp add: zeroideal oneideal) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
952 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
953 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
954 |
assume Jn0: "J \<noteq> {\<zero>}" |
44677 | 955 |
and idealJ: "ideal J R" |
29237 | 956 |
interpret ideal J R by (rule idealJ) |
44677 | 957 |
have "{\<zero>} \<subseteq> J" by (rule ccontr) simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
958 |
from zeromax and idealJ and this and a_subset |
44677 | 959 |
have "J = {\<zero>} \<or> J = carrier R" |
960 |
by (rule maximalideal.I_maximal) |
|
961 |
with Jn0 show "J = carrier R" |
|
962 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
963 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
964 |
|
44677 | 965 |
lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R" |
966 |
apply rule |
|
967 |
apply (erule zeromaximalideal_fieldI) |
|
968 |
apply (erule field.zeromaximalideal) |
|
969 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
970 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
971 |
end |