author | paulson <lp15@cam.ac.uk> |
Wed, 17 Jul 2019 16:32:06 +0100 (2019-07-17) | |
changeset 70367 | 81b65ddac59f |
parent 70215 | 8371a25ca177 |
child 80914 | d97fdabd9e2b |
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 |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
42 |
by (auto simp: ideal.intro ideal_axioms.intro additive_subgroupI a_subgroup ring_axioms 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 |
|
69597 | 46 |
subsubsection (in ring) \<open>Ideals Generated by a Subset of \<^term>\<open>carrier R\<close>\<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 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
71 |
(* NEW ====== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
72 |
lemma (in ideal) rcos_const_imp_mem: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
73 |
assumes "i \<in> carrier R" and "I +> i = I" shows "i \<in> I" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
74 |
using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF ideal_axioms]] assms |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
75 |
by (force simp add: a_r_coset_def') |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
76 |
(* ========== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
77 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
78 |
(* NEW ====== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
79 |
lemma (in ring) a_rcos_zero: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
80 |
assumes "ideal I R" "i \<in> I" shows "I +> i = I" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
81 |
using abelian_subgroupI3[OF ideal.axioms(1) is_abelian_group] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
82 |
by (simp add: abelian_subgroup.a_rcos_const assms) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
83 |
(* ========== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
84 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
85 |
(* NEW ====== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
86 |
lemma (in ring) ideal_is_normal: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
87 |
assumes "ideal I R" shows "I \<lhd> (add_monoid R)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
88 |
using abelian_subgroup.a_normal[OF abelian_subgroupI3[OF ideal.axioms(1)]] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
89 |
abelian_group_axioms assms |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
90 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
91 |
(* ========== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
92 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
93 |
(* NEW ====== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
94 |
lemma (in ideal) a_rcos_sum: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
95 |
assumes "a \<in> carrier R" and "b \<in> carrier R" shows "(I +> a) <+> (I +> b) = I +> (a \<oplus> b)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
96 |
using normal.rcos_sum[OF ideal_is_normal[OF ideal_axioms]] assms |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
97 |
unfolding set_add_def a_r_coset_def by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
98 |
(* ========== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
99 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
100 |
(* NEW ====== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
101 |
lemma (in ring) set_add_comm: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
102 |
assumes "I \<subseteq> carrier R" "J \<subseteq> carrier R" shows "I <+> J = J <+> I" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
103 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
104 |
{ fix I J assume "I \<subseteq> carrier R" "J \<subseteq> carrier R" hence "I <+> J \<subseteq> J <+> I" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
105 |
using a_comm unfolding set_add_def' by (auto, blast) } |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
106 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
107 |
using assms by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
108 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
109 |
(* ========== *) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
110 |
|
35849 | 111 |
|
61382 | 112 |
subsubsection \<open>Maximal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
113 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
114 |
locale maximalideal = ideal + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
115 |
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
|
116 |
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
|
117 |
|
44677 | 118 |
lemma (in maximalideal) is_maximalideal: "maximalideal I R" |
119 |
by (rule maximalideal_axioms) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
120 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
121 |
lemma maximalidealI: |
27611 | 122 |
fixes R |
123 |
assumes "ideal I R" |
|
47409 | 124 |
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
|
125 |
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
|
126 |
shows "maximalideal I R" |
27611 | 127 |
proof - |
29237 | 128 |
interpret ideal I R by fact |
44677 | 129 |
show ?thesis |
130 |
by (intro maximalideal.intro maximalideal_axioms.intro) |
|
131 |
(rule is_ideal, rule I_notcarr, rule I_maximal) |
|
27611 | 132 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
133 |
|
35849 | 134 |
|
61382 | 135 |
subsubsection \<open>Prime Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
136 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
137 |
locale primeideal = ideal + cring + |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
138 |
assumes I_notcarr: "carrier R \<noteq> I" |
44677 | 139 |
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
|
140 |
|
63633 | 141 |
lemma (in primeideal) primeideal: "primeideal I R" |
44677 | 142 |
by (rule primeideal_axioms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
143 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
144 |
lemma primeidealI: |
27611 | 145 |
fixes R (structure) |
146 |
assumes "ideal I R" |
|
47409 | 147 |
and "cring R" |
148 |
and I_notcarr: "carrier R \<noteq> I" |
|
44677 | 149 |
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
|
150 |
shows "primeideal I R" |
27611 | 151 |
proof - |
29237 | 152 |
interpret ideal I R by fact |
153 |
interpret cring R by fact |
|
44677 | 154 |
show ?thesis |
155 |
by (intro primeideal.intro primeideal_axioms.intro) |
|
156 |
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime) |
|
27611 | 157 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
158 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
159 |
lemma primeidealI2: |
27611 | 160 |
fixes R (structure) |
161 |
assumes "additive_subgroup I R" |
|
47409 | 162 |
and "cring R" |
163 |
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I" |
|
44677 | 164 |
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I" |
165 |
and I_notcarr: "carrier R \<noteq> I" |
|
166 |
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
|
167 |
shows "primeideal I R" |
27611 | 168 |
proof - |
29240 | 169 |
interpret additive_subgroup I R by fact |
29237 | 170 |
interpret cring R by fact |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
171 |
show ?thesis apply intro_locales |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
172 |
apply (intro ideal_axioms.intro) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
173 |
apply (erule (1) I_l_closed) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
174 |
apply (erule (1) I_r_closed) |
68464 | 175 |
by (simp add: I_notcarr I_prime primeideal_axioms.intro) |
27611 | 176 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
177 |
|
35849 | 178 |
|
61382 | 179 |
subsection \<open>Special Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
180 |
|
44677 | 181 |
lemma (in ring) zeroideal: "ideal {\<zero>} R" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
182 |
by (intro idealI subgroup.intro) (simp_all add: ring_axioms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
183 |
|
44677 | 184 |
lemma (in ring) oneideal: "ideal (carrier R) R" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
185 |
by (rule idealI) (auto intro: ring_axioms add.subgroupI) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
186 |
|
44677 | 187 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
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
|
193 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
194 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
195 |
|
70215
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
196 |
subsection \<open>General Ideal Properties\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
197 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
198 |
lemma (in ideal) one_imp_carrier: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
199 |
assumes I_one_closed: "\<one> \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
200 |
shows "I = carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
201 |
proof |
68464 | 202 |
show "carrier R \<subseteq> I" |
203 |
using I_r_closed assms by fastforce |
|
204 |
show "I \<subseteq> carrier R" |
|
205 |
by (rule a_subset) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
206 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
207 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
208 |
lemma (in ideal) Icarr: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
209 |
assumes iI: "i \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
210 |
shows "i \<in> carrier R" |
44677 | 211 |
using iI by (rule a_Hcarr) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
212 |
|
70215
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
213 |
lemma (in ring) quotient_eq_iff_same_a_r_cos: |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
214 |
assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
215 |
shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
216 |
proof |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
217 |
assume "I +> a = I +> b" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
218 |
then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
219 |
using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2) |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
220 |
unfolding a_r_coset_def' by blast |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
221 |
hence "a \<ominus> b = i" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
222 |
using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero) |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
223 |
with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
224 |
by simp |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
225 |
next |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
226 |
assume "a \<ominus> b \<in> I" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
227 |
then obtain i where "i \<in> I" and "a = i \<oplus> b" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
228 |
using ideal.Icarr[OF assms(1)] assms(2-3) |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
229 |
by (metis a_minus_def add.inv_solve_right) |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
230 |
hence "I +> a = (I +> i) +> b" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
231 |
using ideal.Icarr[OF assms(1)] assms(3) |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
232 |
by (simp add: a_coset_add_assoc subsetI) |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
233 |
with \<open>i \<in> I\<close> show "I +> a = I +> b" |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
234 |
using a_rcos_zero[OF assms(1)] by simp |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
235 |
qed |
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
69895
diff
changeset
|
236 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
237 |
|
61382 | 238 |
subsection \<open>Intersection of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
239 |
|
61506 | 240 |
paragraph \<open>Intersection of two ideals\<close> |
69597 | 241 |
text \<open>The intersection of any two ideals is again an ideal in \<^term>\<open>R\<close>\<close> |
61506 | 242 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
243 |
lemma (in ring) i_intersect: |
27611 | 244 |
assumes "ideal I R" |
245 |
assumes "ideal J R" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
246 |
shows "ideal (I \<inter> J) R" |
27611 | 247 |
proof - |
29237 | 248 |
interpret ideal I R by fact |
29240 | 249 |
interpret ideal J R by fact |
68464 | 250 |
have IJ: "I \<inter> J \<subseteq> carrier R" |
251 |
by (force simp: a_subset) |
|
27611 | 252 |
show ?thesis |
44677 | 253 |
apply (intro idealI subgroup.intro) |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
254 |
apply (simp_all add: IJ ring_axioms I_l_closed assms ideal.I_l_closed ideal.I_r_closed flip: a_inv_def) |
44677 | 255 |
done |
27611 | 256 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
|
69597 | 258 |
text \<open>The intersection of any Number of Ideals is again an Ideal in \<^term>\<open>R\<close>\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
259 |
|
68464 | 260 |
lemma (in ring) i_Intersect: |
261 |
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}" |
|
262 |
shows "ideal (\<Inter>S) R" |
|
263 |
proof - |
|
264 |
{ fix x y J |
|
265 |
assume "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S" |
|
266 |
interpret ideal J R by (rule Sideals[OF JS]) |
|
267 |
have "x \<oplus> y \<in> J" |
|
268 |
by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>) } |
|
269 |
moreover |
|
270 |
have "\<zero> \<in> J" if "J \<in> S" for J |
|
271 |
by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) |
|
272 |
moreover |
|
273 |
{ fix x J |
|
274 |
assume "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S" |
|
275 |
interpret ideal J R by (rule Sideals[OF JS]) |
|
276 |
have "\<ominus> x \<in> J" |
|
277 |
by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>) } |
|
278 |
moreover |
|
279 |
{ fix x y J |
|
280 |
assume "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S" |
|
281 |
interpret ideal J R by (rule Sideals[OF JS]) |
|
282 |
have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" |
|
283 |
using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+ } |
|
284 |
moreover |
|
285 |
{ fix x |
|
286 |
assume "\<forall>I\<in>S. x \<in> I" |
|
287 |
obtain I0 where I0S: "I0 \<in> S" |
|
288 |
using notempty by blast |
|
289 |
interpret ideal I0 R by (rule Sideals[OF I0S]) |
|
290 |
have "x \<in> I0" |
|
291 |
by (simp add: I0S \<open>\<forall>I\<in>S. x \<in> I\<close>) |
|
292 |
with a_subset have "x \<in> carrier R" by fast } |
|
293 |
ultimately show ?thesis |
|
294 |
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
|
295 |
qed |
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 |
|
61382 | 298 |
subsection \<open>Addition of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
lemma (in ring) add_ideals: |
68464 | 301 |
assumes idealI: "ideal I R" and idealJ: "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
302 |
shows "ideal (I <+> J) R" |
68464 | 303 |
proof (rule ideal.intro) |
304 |
show "additive_subgroup (I <+> J) R" |
|
305 |
by (intro ideal.axioms[OF idealI] ideal.axioms[OF idealJ] add_additive_subgroups) |
|
306 |
show "ring R" |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
307 |
by (rule ring_axioms) |
68464 | 308 |
show "ideal_axioms (I <+> J) R" |
309 |
proof - |
|
310 |
{ fix x i j |
|
311 |
assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" |
|
312 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] |
|
313 |
have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k" |
|
314 |
by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) } |
|
315 |
moreover |
|
316 |
{ fix x i j |
|
317 |
assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" |
|
318 |
from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] |
|
319 |
have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k" |
|
320 |
by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) } |
|
321 |
ultimately show "ideal_axioms (I <+> J) R" |
|
322 |
by (intro ideal_axioms.intro) (auto simp: set_add_defs) |
|
323 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
324 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
|
69597 | 326 |
subsection (in ring) \<open>Ideals generated by a subset of \<^term>\<open>carrier R\<close>\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
327 |
|
69597 | 328 |
text \<open>\<^term>\<open>genideal\<close> generates an ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
329 |
lemma (in ring) genideal_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
330 |
assumes Scarr: "S \<subseteq> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
331 |
shows "ideal (Idl S) R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
332 |
unfolding genideal_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
333 |
proof (rule i_Intersect, fast, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
from oneideal and Scarr |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
335 |
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
|
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 |
lemma (in ring) genideal_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
assumes "S \<subseteq> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
340 |
shows "S \<subseteq> Idl S" |
44677 | 341 |
unfolding genideal_def by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
342 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
343 |
lemma (in ring) genideal_self': |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
344 |
assumes carr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
shows "i \<in> Idl {i}" |
68464 | 346 |
by (simp add: genideal_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
347 |
|
69597 | 348 |
text \<open>\<^term>\<open>genideal\<close> generates the minimal ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
349 |
lemma (in ring) genideal_minimal: |
68464 | 350 |
assumes "ideal I R" "S \<subseteq> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
351 |
shows "Idl S \<subseteq> I" |
68464 | 352 |
unfolding genideal_def by rule (elim InterD, simp add: assms) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
353 |
|
61382 | 354 |
text \<open>Generated ideals and subsets\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
355 |
lemma (in ring) Idl_subset_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
assumes Iideal: "ideal I R" |
44677 | 357 |
and Hcarr: "H \<subseteq> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
358 |
shows "(Idl H \<subseteq> I) = (H \<subseteq> I)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
359 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
360 |
assume a: "Idl H \<subseteq> I" |
23350 | 361 |
from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self) |
44677 | 362 |
with a show "H \<subseteq> I" by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
363 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
364 |
fix x |
47409 | 365 |
assume "H \<subseteq> I" |
366 |
with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast |
|
44677 | 367 |
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
|
368 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
369 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
370 |
lemma (in ring) subset_Idl_subset: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
371 |
assumes Icarr: "I \<subseteq> carrier R" |
44677 | 372 |
and HI: "H \<subseteq> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
373 |
shows "Idl H \<subseteq> Idl I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
374 |
proof - |
44677 | 375 |
from Icarr have Iideal: "ideal (Idl I) R" |
376 |
by (rule genideal_ideal) |
|
377 |
from HI and Icarr have "H \<subseteq> carrier R" |
|
378 |
by fast |
|
379 |
with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)" |
|
380 |
by (rule Idl_subset_ideal[symmetric]) |
|
68464 | 381 |
then show "Idl H \<subseteq> Idl I" |
382 |
by (meson HI Icarr genideal_self order_trans) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
383 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
384 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
385 |
lemma (in ring) Idl_subset_ideal': |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
386 |
assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" |
68464 | 387 |
shows "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> a \<in> Idl {b}" |
388 |
proof - |
|
389 |
have "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> {a} \<subseteq> Idl {b}" |
|
390 |
by (simp add: Idl_subset_ideal acarr bcarr genideal_ideal) |
|
391 |
also have "\<dots> \<longleftrightarrow> a \<in> Idl {b}" |
|
392 |
by blast |
|
393 |
finally show ?thesis . |
|
394 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
395 |
|
44677 | 396 |
lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}" |
68464 | 397 |
proof |
398 |
show "Idl {\<zero>} \<subseteq> {\<zero>}" |
|
399 |
by (simp add: genideal_minimal zeroideal) |
|
400 |
show "{\<zero>} \<subseteq> Idl {\<zero>}" |
|
401 |
by (simp add: genideal_self') |
|
402 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
403 |
|
44677 | 404 |
lemma (in ring) genideal_one: "Idl {\<one>} = carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
405 |
proof - |
44677 | 406 |
interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
407 |
show "Idl {\<one>} = carrier R" |
68464 | 408 |
using genideal_self' one_imp_carrier by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
409 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
410 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
411 |
|
61382 | 412 |
text \<open>Generation of Principal Ideals in Commutative Rings\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
413 |
|
44677 | 414 |
definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79) |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
415 |
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
|
416 |
|
61382 | 417 |
text \<open>genhideal (?) really generates an ideal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
418 |
lemma (in cring) cgenideal_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
419 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
420 |
shows "ideal (PIdl a) R" |
68464 | 421 |
unfolding cgenideal_def |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
422 |
proof (intro subgroup.intro idealI[OF ring_axioms], simp_all) |
68464 | 423 |
show "{x \<otimes> a |x. x \<in> carrier R} \<subseteq> carrier R" |
424 |
by (blast intro: acarr) |
|
425 |
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> |
|
426 |
\<Longrightarrow> \<exists>v. x \<oplus> y = v \<otimes> a \<and> v \<in> carrier R" |
|
427 |
by (metis assms cring.cring_simprules(1) is_cring l_distr) |
|
428 |
show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" |
|
429 |
by (metis assms l_null zero_closed) |
|
430 |
show "\<And>x. \<exists>u. x = u \<otimes> a \<and> u \<in> carrier R |
|
431 |
\<Longrightarrow> \<exists>v. inv\<^bsub>add_monoid R\<^esub> x = v \<otimes> a \<and> v \<in> carrier R" |
|
432 |
by (metis a_inv_def add.inv_closed assms l_minus) |
|
433 |
show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk> |
|
434 |
\<Longrightarrow> \<exists>z. x \<otimes> b = z \<otimes> a \<and> z \<in> carrier R" |
|
435 |
by (metis assms m_assoc m_closed) |
|
436 |
show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk> |
|
437 |
\<Longrightarrow> \<exists>z. b \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" |
|
438 |
by (metis assms m_assoc m_comm m_closed) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
439 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
440 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
441 |
lemma (in ring) cgenideal_self: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
442 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
443 |
shows "i \<in> PIdl i" |
44677 | 444 |
unfolding cgenideal_def |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
445 |
proof simp |
44677 | 446 |
from icarr have "i = \<one> \<otimes> i" |
447 |
by simp |
|
448 |
with icarr show "\<exists>x. i = x \<otimes> i \<and> x \<in> carrier R" |
|
449 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
450 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
451 |
|
69597 | 452 |
text \<open>\<^const>\<open>cgenideal\<close> is minimal\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
453 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
454 |
lemma (in ring) cgenideal_minimal: |
27611 | 455 |
assumes "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
456 |
assumes aJ: "a \<in> J" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
457 |
shows "PIdl a \<subseteq> J" |
27611 | 458 |
proof - |
29240 | 459 |
interpret ideal J R by fact |
44677 | 460 |
show ?thesis |
461 |
unfolding cgenideal_def |
|
68464 | 462 |
using I_l_closed aJ by blast |
27611 | 463 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
464 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
465 |
lemma (in cring) cgenideal_eq_genideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
466 |
assumes icarr: "i \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
467 |
shows "PIdl i = Idl {i}" |
68464 | 468 |
proof |
469 |
show "PIdl i \<subseteq> Idl {i}" |
|
470 |
by (simp add: cgenideal_minimal genideal_ideal genideal_self' icarr) |
|
471 |
show "Idl {i} \<subseteq> PIdl i" |
|
472 |
by (simp add: cgenideal_ideal cgenideal_self genideal_minimal icarr) |
|
473 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
474 |
|
44677 | 475 |
lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i" |
476 |
unfolding cgenideal_def r_coset_def by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
477 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
478 |
lemma (in cring) cgenideal_is_principalideal: |
68464 | 479 |
assumes "i \<in> carrier R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
480 |
shows "principalideal (PIdl i) R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
481 |
proof - |
68464 | 482 |
have "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" |
483 |
using cgenideal_eq_genideal assms by auto |
|
484 |
then show ?thesis |
|
485 |
by (simp add: cgenideal_ideal assms principalidealI) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
486 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
487 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
488 |
|
61382 | 489 |
subsection \<open>Union of Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
490 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
491 |
lemma (in ring) union_genideal: |
68464 | 492 |
assumes idealI: "ideal I R" and idealJ: "ideal J R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
493 |
shows "Idl (I \<union> J) = I <+> J" |
68464 | 494 |
proof |
495 |
show "Idl (I \<union> J) \<subseteq> I <+> J" |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
496 |
proof (rule ring.genideal_minimal [OF ring_axioms]) |
68464 | 497 |
show "ideal (I <+> J) R" |
498 |
by (rule add_ideals[OF idealI idealJ]) |
|
499 |
have "\<And>x. x \<in> I \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb" |
|
500 |
by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def local.idealI r_zero) |
|
501 |
moreover have "\<And>x. x \<in> J \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb" |
|
502 |
by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def l_zero local.idealI) |
|
503 |
ultimately show "I \<union> J \<subseteq> I <+> J" |
|
504 |
by (auto simp: set_add_defs) |
|
505 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
506 |
next |
68464 | 507 |
show "I <+> J \<subseteq> Idl (I \<union> J)" |
69712 | 508 |
by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def subsetD) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
509 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
510 |
|
61382 | 511 |
subsection \<open>Properties of Principal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
512 |
|
61382 | 513 |
text \<open>The zero ideal is a principal ideal\<close> |
44677 | 514 |
corollary (in ring) zeropideal: "principalideal {\<zero>} R" |
68464 | 515 |
using genideal_zero principalidealI zeroideal by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
516 |
|
61382 | 517 |
text \<open>The unit ideal is a principal ideal\<close> |
44677 | 518 |
corollary (in ring) onepideal: "principalideal (carrier R) R" |
68464 | 519 |
using genideal_one oneideal principalidealI by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
520 |
|
61382 | 521 |
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
|
522 |
lemma (in principalideal) rcos_generate: |
27611 | 523 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
524 |
shows "\<exists>x\<in>I. I = carrier R #> x" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
525 |
proof - |
29237 | 526 |
interpret cring R by fact |
44677 | 527 |
from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}" |
528 |
by fast+ |
|
68464 | 529 |
then have "I = PIdl i" |
44677 | 530 |
by (simp add: cgenideal_eq_genideal) |
68464 | 531 |
moreover have "i \<in> I" |
532 |
by (simp add: I1 genideal_self' icarr) |
|
533 |
moreover have "PIdl i = carrier R #> i" |
|
44677 | 534 |
unfolding cgenideal_def r_coset_def by fast |
68464 | 535 |
ultimately show "\<exists>x\<in>I. I = carrier R #> x" |
44677 | 536 |
by fast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
537 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
538 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
539 |
|
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
|
540 |
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
|
541 |
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
|
542 |
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
|
543 |
|
69895
6b03a8cf092d
more formal contributors (with the help of the history);
wenzelm
parents:
69712
diff
changeset
|
544 |
lemma (in cring) cgenideal_prod: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
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
|
545 |
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
|
546 |
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
|
547 |
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
|
548 |
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
|
549 |
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
|
550 |
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
|
551 |
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
|
552 |
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
|
553 |
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
|
554 |
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
|
555 |
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
|
556 |
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
|
557 |
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
|
558 |
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
|
559 |
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
|
560 |
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
|
561 |
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
|
562 |
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
|
563 |
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
|
564 |
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
|
565 |
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
|
566 |
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
|
567 |
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
|
568 |
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
|
569 |
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
|
570 |
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
|
571 |
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
|
572 |
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
|
573 |
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
|
574 |
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
|
575 |
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
|
576 |
|
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
|
577 |
|
61382 | 578 |
subsection \<open>Prime Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
579 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
580 |
lemma (in ideal) primeidealCD: |
27611 | 581 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
582 |
assumes notprime: "\<not> primeideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
583 |
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
|
584 |
proof (rule ccontr, clarsimp) |
29237 | 585 |
interpret cring R by fact |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
586 |
assume InR: "carrier R \<noteq> I" |
44677 | 587 |
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)" |
588 |
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" |
|
589 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
590 |
have "primeideal I R" |
68464 | 591 |
by (simp add: I_prime InR is_cring is_ideal primeidealI) |
44677 | 592 |
with notprime show False by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
593 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
594 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
595 |
lemma (in ideal) primeidealCE: |
27611 | 596 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
597 |
assumes notprime: "\<not> primeideal I R" |
23383 | 598 |
obtains "carrier R = I" |
599 |
| "\<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 | 600 |
proof - |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30363
diff
changeset
|
601 |
interpret R: cring R by fact |
27611 | 602 |
assume "carrier R = I ==> thesis" |
603 |
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" |
|
604 |
then show thesis using primeidealCD [OF R.is_cring notprime] by blast |
|
605 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
606 |
|
63167 | 607 |
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
|
608 |
lemma (in cring) zeroprimeideal_domainI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
609 |
assumes pi: "primeideal {\<zero>} R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
610 |
shows "domain R" |
68464 | 611 |
proof (intro domain.intro is_cring domain_axioms.intro) |
612 |
show "\<one> \<noteq> \<zero>" |
|
613 |
using genideal_one genideal_zero pi primeideal.I_notcarr by force |
|
614 |
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 |
|
615 |
proof - |
|
616 |
interpret primeideal "{\<zero>}" "R" by (rule pi) |
|
617 |
show "a = \<zero> \<or> b = \<zero>" |
|
618 |
using I_prime ab carr by blast |
|
619 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
620 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
621 |
|
44677 | 622 |
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
|
623 |
using domain.zeroprimeideal zeroprimeideal_domainI by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
624 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
625 |
|
61382 | 626 |
subsection \<open>Maximal Ideals\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
627 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
628 |
lemma (in ideal) helper_I_closed: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
629 |
assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R" |
44677 | 630 |
and axI: "a \<otimes> x \<in> I" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
631 |
shows "a \<otimes> (x \<otimes> y) \<in> I" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
632 |
proof - |
44677 | 633 |
from axI and carr have "(a \<otimes> x) \<otimes> y \<in> I" |
634 |
by (simp add: I_r_closed) |
|
635 |
also from carr have "(a \<otimes> x) \<otimes> y = a \<otimes> (x \<otimes> y)" |
|
636 |
by (simp add: m_assoc) |
|
637 |
finally show "a \<otimes> (x \<otimes> y) \<in> I" . |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
638 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
639 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
640 |
lemma (in ideal) helper_max_prime: |
27611 | 641 |
assumes "cring R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
642 |
assumes acarr: "a \<in> carrier R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
643 |
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R" |
27611 | 644 |
proof - |
29237 | 645 |
interpret cring R by fact |
68464 | 646 |
show ?thesis |
647 |
proof (rule idealI, simp_all) |
|
648 |
show "ring R" |
|
649 |
by (simp add: local.ring_axioms) |
|
650 |
show "subgroup {x \<in> carrier R. a \<otimes> x \<in> I} (add_monoid R)" |
|
651 |
by (rule subgroup.intro) (auto simp: r_distr acarr r_minus simp flip: a_inv_def) |
|
652 |
show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk> |
|
653 |
\<Longrightarrow> a \<otimes> (x \<otimes> b) \<in> I" |
|
654 |
using acarr helper_I_closed m_comm by auto |
|
655 |
show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk> |
|
656 |
\<Longrightarrow> a \<otimes> (b \<otimes> x) \<in> I" |
|
657 |
by (simp add: acarr helper_I_closed) |
|
27611 | 658 |
qed |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
659 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
660 |
|
61382 | 661 |
text \<open>In a cring every maximal ideal is prime\<close> |
63633 | 662 |
lemma (in cring) maximalideal_prime: |
27611 | 663 |
assumes "maximalideal I R" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
664 |
shows "primeideal I R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
665 |
proof - |
29237 | 666 |
interpret maximalideal I R by fact |
68464 | 667 |
show ?thesis |
668 |
proof (rule ccontr) |
|
669 |
assume neg: "\<not> primeideal I R" |
|
670 |
then obtain a b where acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" |
|
671 |
and abI: "a \<otimes> b \<in> I" and anI: "a \<notin> I" and bnI: "b \<notin> I" |
|
672 |
using primeidealCE [OF is_cring] |
|
673 |
by (metis I_notcarr) |
|
63040 | 674 |
define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}" |
44677 | 675 |
from is_cring and acarr have idealJ: "ideal J R" |
676 |
unfolding J_def by (rule helper_max_prime) |
|
27611 | 677 |
have IsubJ: "I \<subseteq> J" |
68464 | 678 |
using I_l_closed J_def a_Hcarr acarr by blast |
44677 | 679 |
from abI and acarr bcarr have "b \<in> J" |
680 |
unfolding J_def by fast |
|
681 |
with bnI have JnI: "J \<noteq> I" by fast |
|
68464 | 682 |
have "\<one> \<notin> J" |
683 |
unfolding J_def by (simp add: acarr anI) |
|
44677 | 684 |
then have Jncarr: "J \<noteq> carrier R" by fast |
68464 | 685 |
interpret ideal J R by (rule idealJ) |
27611 | 686 |
have "J = I \<or> J = carrier R" |
68464 | 687 |
by (simp add: I_maximal IsubJ a_subset is_ideal) |
44677 | 688 |
with JnI and Jncarr show False by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
689 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
690 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
691 |
|
35849 | 692 |
|
61382 | 693 |
subsection \<open>Derived Theorems\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
694 |
|
68464 | 695 |
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
|
696 |
lemma (in cring) trivialideals_fieldI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
697 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}" |
44677 | 698 |
and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
699 |
shows "field R" |
68464 | 700 |
proof (intro cring_fieldI equalityI) |
701 |
show "Units R \<subseteq> carrier R - {\<zero>}" |
|
702 |
by (metis Diff_empty Units_closed Units_r_inv_ex carrnzero l_null one_zeroD subsetI subset_Diff_insert) |
|
703 |
show "carrier R - {\<zero>} \<subseteq> Units R" |
|
704 |
proof |
|
705 |
fix x |
|
706 |
assume xcarr': "x \<in> carrier R - {\<zero>}" |
|
707 |
then have xcarr: "x \<in> carrier R" and xnZ: "x \<noteq> \<zero>" by auto |
|
708 |
from xcarr have xIdl: "ideal (PIdl x) R" |
|
709 |
by (intro cgenideal_ideal) fast |
|
710 |
have "PIdl x \<noteq> {\<zero>}" |
|
711 |
using xcarr xnZ cgenideal_self by blast |
|
712 |
with haveideals have "PIdl x = carrier R" |
|
713 |
by (blast intro!: xIdl) |
|
714 |
then have "\<one> \<in> PIdl x" by simp |
|
715 |
then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" |
|
716 |
unfolding cgenideal_def by blast |
|
717 |
then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x" |
|
718 |
by fast |
|
719 |
have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" |
|
720 |
using m_comm xcarr ycarr ylinv by auto |
|
721 |
with xcarr show "x \<in> Units R" |
|
722 |
unfolding Units_def by fast |
|
723 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
724 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
725 |
|
44677 | 726 |
lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}" |
68464 | 727 |
proof (intro equalityI subsetI) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
728 |
fix I |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
729 |
assume a: "I \<in> {I. ideal I R}" |
44677 | 730 |
then interpret ideal I R by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
731 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
732 |
show "I \<in> {{\<zero>}, carrier R}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
733 |
proof (cases "\<exists>a. a \<in> I - {\<zero>}") |
44677 | 734 |
case True |
735 |
then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>" |
|
736 |
by fast+ |
|
68464 | 737 |
have aUnit: "a \<in> Units R" |
738 |
by (simp add: aI anZ field_Units) |
|
44677 | 739 |
then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv) |
740 |
from aI and aUnit have "a \<otimes> inv a \<in> I" |
|
741 |
by (simp add: I_r_closed del: Units_r_inv) |
|
742 |
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
|
743 |
have "carrier R \<subseteq> I" |
68464 | 744 |
using oneI one_imp_carrier by auto |
44677 | 745 |
with a_subset have "I = carrier R" by fast |
746 |
then show "I \<in> {{\<zero>}, carrier R}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
747 |
next |
44677 | 748 |
case False |
749 |
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
|
750 |
have a: "I \<subseteq> {\<zero>}" |
68464 | 751 |
using False by auto |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
752 |
have "\<zero> \<in> I" by simp |
44677 | 753 |
with a have "I = {\<zero>}" by fast |
754 |
then show "I \<in> {{\<zero>}, carrier R}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
755 |
qed |
68464 | 756 |
qed (auto simp: zeroideal oneideal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
757 |
|
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
|
758 |
\<comment>\<open>"Jacobson Theorem 2.2"\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
759 |
lemma (in cring) trivialideals_eq_field: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
760 |
assumes carrnzero: "carrier R \<noteq> {\<zero>}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
761 |
shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R" |
44677 | 762 |
by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
763 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
764 |
|
61382 | 765 |
text \<open>Like zeroprimeideal for domains\<close> |
44677 | 766 |
lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R" |
68464 | 767 |
proof (intro maximalidealI zeroideal) |
44677 | 768 |
from one_not_zero have "\<one> \<notin> {\<zero>}" by simp |
769 |
with one_closed show "carrier R \<noteq> {\<zero>}" by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
770 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
771 |
fix J |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
772 |
assume Jideal: "ideal J R" |
44677 | 773 |
then have "J \<in> {I. ideal I R}" by fast |
774 |
with all_ideals show "J = {\<zero>} \<or> J = carrier R" |
|
775 |
by simp |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
776 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
777 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
778 |
lemma (in cring) zeromaximalideal_fieldI: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
779 |
assumes zeromax: "maximalideal {\<zero>} R" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
780 |
shows "field R" |
68464 | 781 |
proof (intro trivialideals_fieldI maximalideal.I_notcarr[OF zeromax]) |
782 |
have "J = carrier R" if Jn0: "J \<noteq> {\<zero>}" and idealJ: "ideal J R" for J |
|
783 |
proof - |
|
784 |
interpret ideal J R by (rule idealJ) |
|
785 |
have "{\<zero>} \<subseteq> J" |
|
786 |
by force |
|
787 |
from zeromax idealJ this a_subset |
|
788 |
have "J = {\<zero>} \<or> J = carrier R" |
|
789 |
by (rule maximalideal.I_maximal) |
|
790 |
with Jn0 show "J = carrier R" |
|
791 |
by simp |
|
792 |
qed |
|
793 |
then show "{I. ideal I R} = {{\<zero>}, carrier R}" |
|
794 |
by (auto simp: zeroideal oneideal) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
795 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
796 |
|
44677 | 797 |
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
|
798 |
using field.zeromaximalideal zeromaximalideal_fieldI by blast |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
799 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
800 |
end |