Theory Ring_ZF_2
section ‹Rings - Ideals›
theory Ring_ZF_2 imports Ring_ZF Group_ZF_2 Finite_ZF Finite1 Cardinal_ZF Semigroup_ZF
begin
text ‹This section defines the concept of a ring ideal, and
defines some basic concepts and types, finishing with the theorem
that shows that the quotient of the additive group by the ideal
is actually a full ring.›
text‹An ideal is a subgroup of the additive group of the ring, which
is closed by left and right multiplication by any ring element.›
definition (in ring0) Ideal ("_◃R") where
"I ◃R ≡ (∀x∈I. ∀y∈R. y⋅x∈I ∧ x⋅y∈I) ∧ IsAsubgroup(I,A)"
text‹To write less during proofs, we add this small definition›
abbreviation (in ring0) ideals ("ℐ") where
"ℐ ≡ {J∈Pow(R). J◃R}"
text‹The first examples of ideals are the whole ring and the zero ring:›
lemma (in ring0) R_ideal:
shows "R ◃R" unfolding Ideal_def apply simp
using add_group.group0_3_T3[of R]
Ring_ZF_1_L3(1) Ring_ZF_1_L2(1) unfolding IsOpClosed_def
using Ring_ZF_1_L4(1,3) by auto
lemma (in ring0) zero_ideal:
shows "{𝟬} ◃R" unfolding Ideal_def
using
Ring_ZF_1_L6 add_group.unit_singl_subgr by auto
text‹Some small lemmas dividing the definition of ideal into small parts›
lemma (in ring0) ideal_dest_subset:
assumes "I ◃R"
shows "I ⊆ R" using assms unfolding Ideal_def using add_group.group0_3_L2 by auto
lemma (in ring0) ideal_dest_sum:
assumes "I ◃R" "x∈I" "y∈I"
shows "x\<ra>y ∈I" using assms add_group.group0_3_L6
unfolding Ideal_def by auto
lemma (in ring0) ideal_dest_mult:
assumes "I ◃R" "x∈I" "y∈R"
shows "x⋅y ∈I" "y⋅x ∈I" using assms unfolding Ideal_def by auto
lemma (in ring0) ideal_dest_minus:
assumes "I ◃R" "x∈I"
shows "(\<rm>x) ∈ I" using assms unfolding Ideal_def using
add_group.group0_3_T3A by auto
lemma (in ring0) ideal_dest_zero:
assumes "I ◃R"
shows "𝟬 ∈ I" using assms unfolding Ideal_def using
add_group.group0_3_L5 by auto
text‹The most simple way to obtain an ideal from others is the intersection,
since the intersection of arbitrary ideals is an ideal.›
theorem (in ring0) intersection_ideals:
assumes "∀J∈𝒥. (J ◃R)" "𝒥 ≠ 0"
shows "(⋂𝒥) ◃R"
proof-
{
fix x assume x:"x:⋂𝒥"
{
fix y assume y:"y:R"
{
fix J assume J:"J∈𝒥"
with x have "x∈J" by auto
with y J have "y⋅x∈J ∧ x⋅y∈J" using assms(1)
ideal_dest_mult by auto
}
then have "y⋅x∈⋂𝒥 ∧ x⋅y∈⋂𝒥" using assms(2) by auto
}
then have "∀y∈R. y⋅x∈⋂𝒥 ∧ x⋅y∈⋂𝒥" by auto
}
then have e2:"∀x∈⋂𝒥. ∀y∈R. y⋅x∈⋂𝒥 ∧ x⋅y∈⋂𝒥" by auto
have "IsAsubgroup(⋂𝒥,A)" using add_group.subgroup_inter[OF assms(2)] assms(1)
unfolding Ideal_def by auto
with e2 show ?thesis unfolding Ideal_def by auto
qed
text‹From any set, we may construct the minimal ideal containing that set›
definition (in ring0) generatedIdeal ("⟨_⟩⇩I")
where "X⊆R ⟹ ⟨X⟩⇩I ≡ ⋂{I∈ℐ. X ⊆ I}"
text‹The ideal generated by a set is an ideal›
corollary (in ring0) generated_ideal_is_ideal:
assumes "X⊆R"
shows " ⟨X⟩⇩I ◃R" unfolding generatedIdeal_def[OF assms]
apply (rule intersection_ideals) apply simp
using R_ideal assms by auto
text‹The ideal generated by a set is contained in any ideal containing the set›
corollary (in ring0) generated_ideal_small:
assumes "X ⊆ I" "I ◃R"
shows " ⟨X⟩⇩I ⊆ I"
proof-
have "I∈{J∈Pow(R). J ◃R ∧ X⊆J}" using assms(2,1)
ideal_dest_subset by auto
then have "⋂{J∈Pow(R). J ◃R ∧ X⊆J} ⊆ I" by auto moreover
from assms have "X⊆ R" using ideal_dest_subset by auto
ultimately show "⟨X⟩⇩I ⊆ I" using generatedIdeal_def[of X]
by auto
qed
text‹The ideal generated by a set contains the set›
corollary (in ring0) generated_ideal_contains_set:
assumes "X⊆R"
shows "X⊆⟨X⟩⇩I"
proof-
{
fix J assume J:"J:{J∈ℐ. X⊆J}"
{
fix t assume "t:X"
with J have "t:J" by auto
}
then have "X⊆J" by auto
}
then have "X⊆⋂{J∈ℐ. X⊆J} ∨ {J∈ℐ. X⊆J}=0" by auto
then show "X⊆⟨X⟩⇩I" unfolding generatedIdeal_def[OF assms]
using assms R_ideal by auto
qed
text‹To be able to show properties of an ideal generated by a set, we
have the following induction result›
lemma (in ring0) induction_generated_ideal:
assumes "∀y∈R. ∀z∈R. ∀q∈⟨X⟩⇩I. P(q) ⟶ P(y⋅q⋅z)"
"∀y∈R. ∀z∈R. P(y) ∧ P(z) ⟶ P(y\<ra>z)"
"X ⊆ R"
"∀x∈X. P(x)"
"X≠0"
shows "∀y∈⟨X⟩⇩I. P(y)"
proof-
let ?J="{m∈⟨X⟩⇩I. P(m)}"
have XJ:"X ⊆ ?J" using assms(3,4) generated_ideal_contains_set by auto
have sub:"?J ⊆ R" using generated_ideal_is_ideal ideal_dest_subset assms(3) by auto moreover
{
fix y z assume "y∈R" "z∈?J"
then have yz:"z∈⟨X⟩⇩I" "y∈R" "P(z)" "z:R" using sub by auto
from assms(1) yz have "P(y⋅z)" using
Ring_ZF_1_L2(2) Ring_ZF_1_L3(5)[of "y⋅z"] Ring_ZF_1_L4(3)[of y]
by force moreover
from assms(1) yz have "P(z⋅y)" using
Ring_ZF_1_L2(2) Ring_ZF_1_L3(6) Ring_ZF_1_L4(3)[of _ y]
by force moreover
from yz(1,2) have "y⋅z∈⟨X⟩⇩I" "z⋅y∈⟨X⟩⇩I" using
generated_ideal_is_ideal[OF assms(3)] ideal_dest_mult by auto
ultimately have "y⋅z∈?J" "z⋅y∈?J" by auto
}
then have "∀x∈?J. ∀y∈R. y ⋅ x ∈ ?J ∧ x ⋅ y ∈ ?J" by auto
moreover
have "IsAsubgroup(?J,A)"
proof(rule add_group.group0_3_T3)
show "?J≠0" using assms(3-5) generated_ideal_contains_set[OF assms(3)] by force
show "?J⊆R" using sub .
{
fix x assume "x:?J"
then have x:"x:⟨X⟩⇩I" "x∈R" "P(x)" using sub by auto moreover
have "𝟭:R" using Ring_ZF_1_L2(2).
then have "𝟭:R" "(\<rm>𝟭):R" using Ring_ZF_1_L3(1) by auto
ultimately have "P((\<rm>𝟭)⋅x⋅𝟭)" using assms(1) by auto
then have "P((\<rm>x)⋅𝟭)" using Ring_ZF_1_L3(6)[of x]
Ring_ZF_1_L7(1)[of 𝟭 x] `𝟭:R` `x:R` by auto
then have "P(\<rm>x)" using Ring_ZF_1_L3(5)[OF Ring_ZF_1_L3(1)]
`x:R` by auto moreover
from x(1) have "(\<rm>x)∈⟨X⟩⇩I" using generated_ideal_is_ideal[OF assms(3)]
ideal_dest_minus by auto
ultimately have "(\<rm>x)∈?J" by auto
}
then show "∀x∈?J. (\<rm> x) ∈ ?J" by auto
{
fix x y assume as:"x∈?J" "y∈?J"
from as have "P(x\<ra>y)" using assms(2)
ideal_dest_subset[OF generated_ideal_is_ideal[OF assms(3)]] by auto
moreover
have "x\<ra>y∈⟨X⟩⇩I" using as generated_ideal_is_ideal[OF assms(3)]
ideal_dest_sum by auto
ultimately have "x\<ra>y ∈ ?J" by auto
}
then show "?J {is closed under} A" unfolding IsOpClosed_def by auto
qed
ultimately have "?J◃R" unfolding Ideal_def by auto
with XJ have "⟨X⟩⇩I ⊆ ?J" using generated_ideal_small by auto
then show ?thesis by auto
qed
text‹An ideal is very particular with the elements it may contain. If it contains
any invertible element, it is in fact the whole ring and not a proper subset›
theorem (in ring0) ideal_with_one:
assumes "I◃R" "𝟭∈I"
shows "I = R"
proof-
from assms(1) have "I ⊆ R" using ideal_dest_subset by auto
moreover
{
fix t assume t:"t:R"
with assms have "t⋅𝟭 ∈I" using ideal_dest_mult(2) by auto
with t have "t:I" using Ring_ZF_1_L3(5) by auto
}
then have "R⊆ I" by auto
ultimately show "I=R" by auto
qed
theorem (in ring0) ideal_with_unit:
assumes "I◃R" "x∈I" "∃y∈R. y⋅x = 𝟭 ∨ x⋅y =𝟭"
shows "I = R"
proof-
from assms(3) obtain y where y:"y:R" "y⋅x = 𝟭 ∨ x⋅y =𝟭" by auto
from this(1) assms(1,2) have "y⋅x ∈I" "x⋅y∈I" unfolding Ideal_def by auto
with y(2) have "𝟭∈I" by auto
with ideal_with_one assms(1) show ?thesis by auto
qed
text‹The previous result drives us to define what a maximal ideal would be:
an ideal such that any bigger ideal is the whole ring›
definition (in ring0) maximalIdeal ("_◃⇩mR") where
"I◃⇩mR ≡ I◃R ∧ I ≠R ∧ (∀J∈ℐ. I⊆J ∧ J≠R ⟶ I=J)"
text‹Before delving into maximal ideals, lets define some operation on ideals
that are useful when formulating some proofs.›
definition (in ring0) productIdeal (infix "⋅⇩I" 90) where
"I◃R ⟹ J◃R ⟹ I⋅⇩IJ ≡ ⟨M``(I×J)⟩⇩I"
definition (in ring0) sumIdeal (infix "+⇩I" 90) where
"I◃R ⟹ J◃R ⟹ I+⇩IJ ≡ ⟨I∪J⟩⇩I"
text‹Some times, we may need to sum an arbitrary number
of ideals, and not just two›
definition(in ring0) sumArbitraryIdeals ("⊕⇩I_" 90) where
"𝒥 ⊆ ℐ ⟹ ⊕⇩I𝒥 ≡ ⟨⋃𝒥⟩⇩I"
text‹Every element in the arbitrary sum of ideals
is generated by only a finite subset of those ideals›
lemma (in ring0) sum_ideals_finite_sum:
assumes "𝒥 ⊆ ℐ" "s∈(⊕⇩I𝒥)"
shows "∃𝒯∈FinPow(𝒥). s∈(⊕⇩I𝒯)"
proof-
{
assume "⋃𝒥=0"
then have "𝒥⊆{0}" by auto
then have "Finite(𝒥)" using subset_Finite[OF _ nat_into_Finite[of 1]]
by auto
then have "𝒥∈FinPow(𝒥)" unfolding FinPow_def by auto
then have ?thesis using assms(2) by auto
}
moreover
{
assume notE:"⋃𝒥≠0"
let ?P= "λt. ∃𝒯∈FinPow(𝒥). t∈(⊕⇩I𝒯)"
{
fix t assume "t∈⋃𝒥"
then obtain J where J:"t∈J" "J∈𝒥" by auto
then have "{J}∈FinPow(𝒥)" unfolding FinPow_def
using eqpoll_imp_Finite_iff[of "{J}" "1"] nat_into_Finite
by auto moreover
have "(⊕⇩I{J}) = ⟨J⟩⇩I" using J(2) assms(1)
sumArbitraryIdeals_def by auto
with J(1) have "t∈(⊕⇩I{J})"
using generated_ideal_contains_set[of J]
J(2) assms(1) by auto
ultimately have "?P(t)" by auto
}
then have "∀t∈⋃𝒥. ?P(t)" by auto moreover
{
fix y z q assume q:"?P(q)" "y:R" "z:R" "q:⟨⋃𝒥⟩⇩I"
then obtain 𝒯 where T:"𝒯∈FinPow(𝒥)" "q:⊕⇩I𝒯" by auto
from T(1) have "⋃𝒯 ⊆ R" "𝒯⊆ℐ" using assms(1) unfolding FinPow_def by auto
then have "(⊕⇩I𝒯)◃R" using generated_ideal_is_ideal[of "⋃𝒯"]
sumArbitraryIdeals_def[of 𝒯] by auto
with T(2) q(2,3) have "y ⋅ q ⋅ z ∈ ⊕⇩I𝒯"
unfolding Ideal_def by auto
with T(1) have "?P(y ⋅ q ⋅ z)" by auto
}
then have "∀y∈R. ∀z∈R. ∀q∈⟨⋃𝒥⟩⇩I. ?P(q) ⟶ ?P(y ⋅ q ⋅ z)" by auto moreover
{
fix y z assume "?P(y)" "?P(z)"
then obtain Ty Tz where T:"Ty∈FinPow(𝒥)" "y ∈ ⊕⇩ITy"
"Tz∈FinPow(𝒥)" "z ∈ ⊕⇩ITz" by auto
from T(1,3) have A:"Ty∪Tz:FinPow(𝒥)" unfolding FinPow_def
using Finite_Un by auto
then have "⋃Ty ⊆ ⋃(Ty∪Tz)" "⋃Tz ⊆ ⋃(Ty∪Tz)" and sub:"⋃(Ty∪Tz) ⊆R"
unfolding FinPow_def using assms(1) by auto
with A have "⋃Ty ⊆ ⟨⋃(Ty∪Tz)⟩⇩I" "⋃Tz ⊆ ⟨⋃(Ty∪Tz)⟩⇩I" using
generated_ideal_contains_set[of "⋃(Ty∪Tz)"] by auto
then have "⟨⋃Ty⟩⇩I⊆ ⟨⋃(Ty∪Tz)⟩⇩I" "⟨⋃Tz⟩⇩I ⊆ ⟨⋃(Ty∪Tz)⟩⇩I"
using generated_ideal_small[OF _ generated_ideal_is_ideal]
sub by auto
moreover from T(1,3) have Q:"Ty ⊆ℐ" "Tz⊆ ℐ" using assms(1)
unfolding FinPow_def by auto
moreover note T(2,4)
ultimately have "y∈⟨⋃(Ty∪Tz)⟩⇩I" "z∈⟨⋃(Ty∪Tz)⟩⇩I"
using sumArbitraryIdeals_def[of "Ty"]
sumArbitraryIdeals_def[of "Tz"] by auto
then have "y\<ra>z∈⟨⋃(Ty∪Tz)⟩⇩I" using
generated_ideal_is_ideal[OF sub] ideal_dest_sum
by auto
then have "y\<ra>z∈(⊕⇩I(Ty∪Tz))" using sumArbitraryIdeals_def[of "Ty∪Tz"]
Q by force
with A have "?P(y\<ra>z)" by auto
}
then have "∀y∈R. ∀z∈R. ?P(y) ∧ ?P(z) ⟶ ?P(y \<ra> z)" by auto
moreover
have sub:"⋃𝒥 ⊆ R" using assms(1) by auto
ultimately have "∀t∈⟨⋃𝒥⟩⇩I. ?P(t)"
using induction_generated_ideal[of "⋃𝒥" ?P] notE by blast
with assms(2) have ?thesis unfolding
sumArbitraryIdeals_def[OF assms(1)] by auto
}
ultimately show ?thesis by auto
qed
text‹By definition of product of ideals and of an ideal itself, it follows
that the product of ideals is an ideal contained in the intersection›
theorem (in ring0) product_in_intersection:
assumes "I◃R" "J◃R"
shows "I⋅⇩IJ ⊆ I∩J" and "(I⋅⇩IJ)◃R" and "M``(I×J) ⊆ I⋅⇩IJ"
proof-
have s:"M``(I×J) ⊆ I∩J"
proof
fix x assume x:"x∈M``(I×J)"
then obtain y where "y:I×J" "⟨y,x⟩∈M" unfolding image_def
by auto
then obtain yi yj where y:"yi:I" "yj:J" "⟨⟨yi,yj⟩,x⟩∈M" by auto
then have "yi⋅yj:I" "yi⋅yj:J" using assms ideal_dest_subset[of I] ideal_dest_subset[of J] unfolding Ideal_def
by auto
with y(3) show "x∈I∩J" using apply_equality[of _ x M]
using ringAssum unfolding IsAring_def IsAmonoid_def IsAssociative_def
by auto
qed
moreover
have "(I∩J) ◃R" using intersection_ideals[of "{I,J}"] assms by auto
ultimately show "I⋅⇩IJ ⊆ I∩J" unfolding productIdeal_def[OF assms]
using generated_ideal_small by auto
from s have q:"M``(I×J) ⊆ R" using assms ideal_dest_subset by auto
with generated_ideal_is_ideal show "(I⋅⇩IJ) ◃R" unfolding
productIdeal_def[OF assms] by auto
from q show "M``(I×J) ⊆ I⋅⇩IJ" using generated_ideal_contains_set
unfolding productIdeal_def[OF assms] by auto
qed
text‹We will show now that the sum of ideals is no more that the sum of the ideal elements›
lemma (in ring0) sum_elements:
assumes "I ◃R" "J ◃R" "x ∈ I" "y ∈ J"
shows "x\<ra>y ∈ I+⇩IJ"
proof-
from assms(1,2) have "I∪J ⊆ R" using ideal_dest_subset by auto moreover
have "x∈ I∪J" "y∈ I∪J" using assms(3,4) by auto
ultimately have "x ∈ ⟨I∪J⟩⇩I" "y ∈ ⟨I∪J⟩⇩I" using generated_ideal_contains_set
by auto
moreover have "⟨I∪J⟩⇩I ◃R" using generated_ideal_is_ideal[of "I∪J"] assms(1,2)
using ideal_dest_subset[of I] ideal_dest_subset[of J]
by auto
ultimately have "x\<ra>y∈⟨I∪J⟩⇩I" using ideal_dest_sum by auto
then show ?thesis using sumIdeal_def assms(1,2) by auto
qed
lemma (in ring0) sum_elements_is_ideal:
assumes "I ◃R" "J ◃R"
shows "(A``(I×J)) ◃R"
proof-
have a:"A:R×R → R" using add_group.groupAssum IsAgroup_def
IsAmonoid_def IsAssociative_def by simp
from assms have ij:"I×J ⊆ R×R" using ideal_dest_subset by auto
from a have Aimage:"A``(I×J) ⊆ R" using func1_1_L6(2) by auto
moreover
{
fix x y assume xy:"x∈R" "y∈A``(I×J)"
from ij xy(2) obtain z where "y=A`z" "z∈I×J" using func_imagedef[OF a, of "I×J"]
by auto
then obtain yi yj where y:"y=yi\<ra>yj" "yi∈I" "yj∈J"
by auto
from y(1) have "x⋅y = x⋅(yi\<ra>yj)" "y⋅x = (yi\<ra>yj)⋅x" by auto
then have "x⋅y = (x⋅yi)\<ra>(x⋅yj)" "y⋅x = (yi⋅x)\<ra>(yj⋅x)"
using ring_oper_distr xy(1) y ij add_group.group_op_closed by auto
moreover
have "x⋅yi ∈ I" "yi⋅x ∈ I" "x⋅yj ∈ J" "yj⋅x ∈ J"
using assms xy(1) y(2,3) ideal_dest_mult by auto
ultimately have "x⋅y∈A``(I×J)" "y⋅x∈A``(I×J)"
using func_imagedef[OF a, of "I×J"] ij by auto
}
then have "∀x∈A``(I×J). ∀y∈R. y ⋅ x ∈ A``(I×J) ∧ x ⋅ y ∈ A``(I×J)" by auto
moreover
have "IsAsubgroup(A``(I×J),A)"
proof(rule add_group.group0_3_T3)
show AsubR:"A `` (I × J) ⊆ R" using Aimage.
{
fix x assume "x∈A `` (I × J)"
then obtain z where "x=A`z" "z∈I×J" using func_imagedef[OF a, of "I×J"]
ij by auto
then obtain xi xj where x:"xi∈I" "xj∈J" "x=xi\<ra>xj" by auto
from x(3) have "(\<rm>x) = \<rm>(xi\<ra>xj)" by auto
then have "(\<rm>x) = (\<rm>xi)\<rs>xj" using Ring_ZF_1_L9(2)
assms x(1,2) ideal_dest_subset by auto
moreover
have "(\<rm>xi)∈I" using assms(1) ideal_dest_minus x(1) by auto
moreover
have "(\<rm>xj)∈J" using assms(2) ideal_dest_minus x(2) by auto
ultimately have "(\<rm>x) ∈ A``(I×J)" using func_imagedef[OF a, of "I×J"]
ij by auto
}
then show "∀x∈A `` (I × J). (\<rm> x) ∈ A `` (I × J)" by auto
have "𝟬∈I" "𝟬∈J" using ideal_dest_zero assms by auto
then have "𝟬\<ra>𝟬 ∈ A `` (I × J)" using func_imagedef[OF a, of "I×J"] ij by auto
then show "A `` (I × J) ≠ 0" by auto
{
fix x y assume xy:"x∈ A `` (I × J)" "y∈ A `` (I × J)"
then obtain z g where "x=A`z" "z∈I×J" "y=A`g" "g∈I×J" using func_imagedef[OF a, of "I×J"]
ij by auto
then obtain xi xj yi yj where x:"xi∈I" "xj∈J" "x=xi\<ra>xj"
"yi∈I" "yj∈J" "y=yi\<ra>yj" by auto
have "x\<ra>y = (x\<ra>yi)\<ra>yj" using xy(1) AsubR
x(4-6) ij Ring_ZF_1_L10(1)[of x yi yj] by force
then have "x\<ra>y = (xi\<ra>yi)\<ra>(xj\<ra>yj)"
using x(1-5) ij Ring_ZF_2_L5(4)[of xi xj yi yj] by auto
moreover have "xi\<ra>yi ∈ I" using x(1,4) assms(1)
ideal_dest_sum by auto
moreover have "xj\<ra>yj ∈ J" using x(2,5) assms(2)
ideal_dest_sum by auto
ultimately have "x\<ra>y ∈ A``(I×J)" using func_imagedef[OF a, of "I×J"]
ij by auto
}
then show "A `` (I × J) {is closed under} A" unfolding IsOpClosed_def
by auto
qed
ultimately show "(A `` (I × J))◃R" unfolding Ideal_def by auto
qed
corollary (in ring0) sum_ideals_is_sum_elements:
assumes "I ◃R" "J ◃R"
shows "(A `` (I × J)) = I+⇩IJ"
proof
have a:"A:R×R → R" using add_group.groupAssum IsAgroup_def
IsAmonoid_def IsAssociative_def by simp
from assms have ij:"I⊆R" "J ⊆ R" using ideal_dest_subset by auto
then have ij_prd:"I×J ⊆ R×R" by auto
then show "A `` (I × J) ⊆ I +⇩I J" using sum_elements[OF assms]
func_imagedef[OF a, of "I×J"] by auto
{
fix x assume x:"x∈I"
with ij(1) have "x=x\<ra>𝟬" using Ring_ZF_1_L3(3)[of x] by auto
then have "x∈A `` (I × J)" using x assms(2) add_group.group0_3_L5[of J]
unfolding Ideal_def using func_imagedef[OF a, of "I×J"]
ij_prd by auto
}
then have "I ⊆ A `` (I × J)" by auto moreover
{
fix x assume x:"x∈J"
with ij(2) have "x=𝟬\<ra>x" using Ring_ZF_1_L3(4)[of x] by auto
then have "x∈A `` (I × J)" using x assms(1) add_group.group0_3_L5[of I]
unfolding Ideal_def using func_imagedef[OF a, of "I×J"]
ij_prd by auto
}
then have "J ⊆ A `` (I × J)" by auto
ultimately have "I∪J ⊆ A `` (I × J)" by auto
then show "I+⇩IJ ⊆ A `` (I × J)" using generated_ideal_small
sum_elements_is_ideal[OF assms] assms sumIdeal_def
by auto
qed
corollary (in ring0) sum_ideals_is_ideal:
assumes "I ◃R" "J ◃R"
shows "(I +⇩I J) ◃R" using assms sum_ideals_is_sum_elements
sum_elements_is_ideal ideal_dest_subset by auto
corollary (in ring0) sum_ideals_commute:
assumes "I◃R" "J◃R"
shows "(I +⇩I J) = (J +⇩I I)"
proof-
have "I ∪ J = J ∪ I" by auto
then show ?thesis unfolding
sumIdeal_def[OF assms] sumIdeal_def[OF assms(2,1)]
by auto
qed
text‹Now that we know what the product of ideals is, we are able to define
what a prime ideal is:›
definition (in ring0) primeIdeal ("_◃⇩pR") where
"P◃⇩pR ≡ P◃R ∧ P≠R ∧ (∀I∈ℐ. ∀J∈ℐ. I ⋅⇩I J ⊆ P ⟶ (I ⊆ P ∨ J ⊆ P))"
text‹Any maximal ideal is prime›
theorem (in ring0) maximal_is_prime:
assumes "Q◃⇩mR"
shows "Q◃⇩pR"
proof-
have a:"A:R×R → R" using add_group.groupAssum IsAgroup_def
IsAmonoid_def IsAssociative_def by simp
have MI:"Q ∈ ℐ" using assms unfolding maximalIdeal_def
using ideal_dest_subset by auto
{
fix I J assume ij:"I∈ℐ" "J∈ℐ" "I ⋅⇩I J ⊆ Q"
{
assume K:"¬(I⊆Q)" "¬(J⊆Q)"
from this(1) obtain x where x:"x∈I-Q" by auto
then have xR:"x∈R" using ij(1) ideal_dest_subset by auto
let ?K = "⟨Q∪{x}⟩⇩I"
have MK:"Q ⊆ ?K" "x∈?K" using generated_ideal_contains_set[of "Q∪{x}"]
assms unfolding maximalIdeal_def using ideal_dest_subset[of Q]
xR by auto
with x have "Q ⊆ ?K" "?K≠Q" by auto
with assms have "?K∈ℐ ⟹ ?K=R" unfolding maximalIdeal_def by auto
then have KR:"?K=R" using generated_ideal_is_ideal[of "Q∪{x}"] xR
assms unfolding maximalIdeal_def using ideal_dest_subset[of Q]
ideal_dest_subset[of "⟨Q∪{x}⟩⇩I"] by auto
let ?P="Q+⇩II"
have "Q∪I ⊆ Q+⇩II" using generated_ideal_contains_set[of "Q∪I"]
sumIdeal_def[of Q I] assms ij(1)
maximalIdeal_def using ideal_dest_subset by auto
then have "Q∪{x} ⊆ Q+⇩II" using x by auto
then have "?K ⊆ Q+⇩II" "Q+⇩II ⊆R" using generated_ideal_small[of "Q∪{x}" "Q+⇩II"]
generated_ideal_is_ideal[of "Q∪I"] sumIdeal_def[of Q I]
ij(1) assms unfolding maximalIdeal_def using
ideal_dest_subset by auto
with KR have "Q+⇩II = R" by auto
then have "𝟭∈Q+⇩II " using Ring_ZF_1_L2(2) by auto
then have "𝟭∈A``(Q×I)"
using sum_ideals_is_sum_elements MI ij(1) by auto
moreover have "Q×I ⊆ R×R" using MI ij(1) by auto
ultimately obtain xm xi where mi1:"xm∈Q" "xi∈I" "𝟭=xm\<ra>xi"
using func_imagedef[OF a, of "Q×I"] by auto
{
fix y assume y:"y∈J"
then have "𝟭⋅y = y" using Ring_ZF_1_L3(6) ij(2) by auto
with mi1(3) have "(xm\<ra>xi)⋅y = y" by auto
moreover have elems:"y:R" "xm:R" "xi:R" using y mi1(1,2)
MI ij(1,2) by auto
ultimately have "(xm⋅y)\<ra>(xi⋅y) = y" using
ring_oper_distr(2)[of y xm xi] by auto
moreover have "xm⋅y:Q" using mi1(1) elems(1)
MI ideal_dest_mult(1) by auto
moreover
have sub:"I×J ⊆ R×R" using ij(1,2) by auto
have MR:"M:R×R→R" using ringAssum unfolding IsAring_def
IsAmonoid_def IsAssociative_def by auto
from sub MR have "xi⋅y:M``(I×J)"
using func_imagedef[of M "R×R" R "I×J"] y mi1(2) by auto
then have "xi⋅y:I⋅⇩IJ" using generated_ideal_contains_set[of "M``(I×J)"]
func1_1_L6(2)[OF MR] productIdeal_def ij(1,2) by auto
with ij(3) have "xi⋅y:Q" by auto
ultimately have "y∈Q" using MI ideal_dest_sum by force
}
then have "J ⊆ Q" by auto
with K have False by auto
}
then have "(I⊆Q)∨(J⊆Q)" by auto
}
then have "∀I∈ℐ. ∀J∈ℐ. I ⋅⇩I J ⊆ Q ⟶ (I ⊆ Q ∨ J ⊆ Q)" by auto
then show ?thesis using assms unfolding maximalIdeal_def primeIdeal_def
by auto
qed
text‹In case of non-commutative rings, the zero divisor concept is too constrictive.
For that we define the following concept of a prime ring. Note that in case that
our ring is commutative, this is equivalent to having no zero divisors (there is no proof yet)›
definition primeRing ("[_,_,_]{is a prime ring}") where
"IsAring(R,A,M) ⟹ [R,A,M]{is a prime ring} ≡
(∀x∈R. ∀y∈R. (∀z∈R. M`⟨M`⟨x,z⟩,y⟩ = TheNeutralElement(R,A)) ⟶ x =TheNeutralElement(R,A) ∨ y=TheNeutralElement(R,A))"
text‹Prime rings appear when the zero ideal is prime›
lemma (in ring0) prime_ring_zero_prime_ideal:
assumes "[R,A,M]{is a prime ring}" "R≠{𝟬}"
shows "{𝟬}◃⇩pR"
proof-
have MR:"M:R×R→R" using ringAssum unfolding IsAring_def
IsAmonoid_def IsAssociative_def by auto
{
fix I J assume ij:"I∈ℐ" "J∈ℐ" "I ⋅⇩I J ⊆ {𝟬}"
from ij(1,2) have ij_rr:"I×J ⊆ R×R" by auto
{
assume "¬(I⊆{𝟬})" "¬(J⊆{𝟬})"
then obtain xi xj where x:"xi≠𝟬" "xj≠𝟬" "xi∈I" "xj:J" by auto
{
fix u assume "u∈R"
with x(3) have "xi⋅u∈I" using ij(1) ideal_dest_mult(1)
by auto
with x(4) have "xi⋅u⋅xj:M``(I×J)" using func_imagedef[OF MR]
ij_rr by auto
then have "xi⋅u⋅xj:I ⋅⇩I J" using generated_ideal_contains_set[of "M `` (I × J)"]
func1_1_L6(2)[OF MR, of "I×J"] productIdeal_def ij(1,2)
by auto
with ij(3) have "xi⋅u⋅xj = 𝟬" by auto
}
then have "∀u∈R. xi⋅u⋅xj = 𝟬" by auto moreover
have "xi∈R" "xj∈R" using ij(1,2) x(3,4) by auto
moreover note assms(1) ultimately have False
using x(1,2) unfolding primeRing_def[OF ringAssum] by auto
}
then have "I⊆{𝟬} ∨ J⊆{𝟬}" by auto
}
then have "∀I∈ℐ. ∀J∈ℐ. I ⋅⇩I J ⊆ {𝟬} ⟶ (I ⊆ {𝟬} ∨ J ⊆ {𝟬})" by auto
moreover
note zero_ideal assms(2) ultimately
show ?thesis unfolding primeIdeal_def by auto
qed
lemma (in ring0) zero_prime_ideal_prime_ring:
assumes "{𝟬}◃⇩pR"
shows "[R,A,M]{is a prime ring}"
proof-
have MR:"M:R×R→R" using ringAssum unfolding IsAring_def
IsAmonoid_def IsAssociative_def by auto
{
fix x y z assume as:"x∈R" "y∈R" "∀z∈R. x⋅z⋅y = 𝟬"
let ?X="⟨{x}⟩⇩I"
let ?Y="⟨{y}⟩⇩I"
have "?X⊆R" "?Y⊆R" using generated_ideal_is_ideal
ideal_dest_subset as(1,2) by auto
then have XY:"?X×?Y ⊆ R×R" by auto
let ?P="λq. (∀z∈?Y. q⋅z = 𝟬)"
let ?Q="λq. (∀z∈R. x⋅z⋅q =𝟬)"
have Y:"∀y∈?Y. ?Q(y)"
proof(rule induction_generated_ideal)
show "{y}⊆R" "{y}≠0" using as(2) by auto
show "∀xa∈{y}. ∀z∈R. x ⋅ z ⋅ xa = 𝟬" using as(3) by auto
{
fix s t q assume yzq:"s:R" "t:R" "q:⟨{y}⟩⇩I" "∀k∈R. x ⋅ k ⋅ q = 𝟬"
from yzq(3) have q:"q∈R" using generated_ideal_is_ideal
ideal_dest_subset as(2) by auto
{
fix u assume "u:R"
have "x ⋅ u ⋅ (s ⋅ q ⋅ t) = (x ⋅ (u⋅s)⋅q)⋅t"
using Ring_ZF_1_L11(2) yzq(1-2) q `u:R` as(1) Ring_ZF_1_L4(3)
by auto
moreover have "u⋅s:R" using `u:R` yzq(1) Ring_ZF_1_L4(3) by auto
moreover note yzq(4) ultimately
have "x ⋅ u ⋅ (s ⋅ q ⋅ t) = 𝟬⋅t" by auto
then have "x ⋅ u ⋅ (s ⋅ q ⋅ t) = 𝟬" using yzq(2) Ring_ZF_1_L6(1) by auto
}
then have "∀za∈R. x ⋅ za ⋅ (s ⋅ q ⋅ t) = 𝟬" by auto
}
then show "∀t∈R. ∀z∈R. ∀q∈⟨{y}⟩⇩I. (∀z∈R. x ⋅ z ⋅ q = 𝟬) ⟶ (∀za∈R. x ⋅ za ⋅ (t ⋅ q ⋅ z) = 𝟬)" by auto
{
fix s t assume st:"s:R" "t:R" "∀k∈R. x ⋅ k ⋅ s = 𝟬" "∀k∈R. x ⋅ k ⋅ t = 𝟬"
{
fix u assume "u:R"
have "x ⋅ u ⋅ (s \<ra> t) = (x ⋅ u ⋅ s) \<ra>(x ⋅ u ⋅ t)"
using ring_oper_distr(1) `u:R` as(1) st(1,2) Ring_ZF_1_L4(3) by auto
with st(3,4) `u:R` have "x ⋅ u ⋅ (s \<ra> t) = 𝟬 \<ra> 𝟬" by auto
then have "x ⋅ u ⋅ (s \<ra> t) = 𝟬" using Ring_ZF_1_L3(3) Ring_ZF_1_L2(1) by auto
}
then have "∀za∈R. x ⋅ za ⋅ (s \<ra> t) = 𝟬" by auto
}
then show "∀y∈R. ∀z∈R. (∀z∈R. x ⋅ z ⋅ y = 𝟬) ∧ (∀za∈R. x ⋅ za ⋅ z = 𝟬) ⟶
(∀za∈R. x ⋅ za ⋅ (y \<ra> z) = 𝟬)" by auto
qed
{
fix yy assume "yy:?Y"
with Y have "∀z∈R. x ⋅ z ⋅ yy = 𝟬" by auto
then have "x⋅yy = 𝟬" using Ring_ZF_1_L2(2) Ring_ZF_1_L3(5)
as(1) by auto
}
then have z:"∀y∈?Y. x⋅y = 𝟬" by auto
have yy:"?Y◃R" "?Y ⊆ R" using generated_ideal_is_ideal as(2)
ideal_dest_subset by auto
have xy:"∀y∈?X. ?P(y)"
proof(rule induction_generated_ideal)
show "{x}⊆R" "{x}≠0" using as(1) by auto
from z show "∀x∈{x}. ∀z∈⟨{y}⟩⇩I. x ⋅ z = 𝟬" by auto
{
fix q1 q2 q3 assume q:"q1:R" "q2:R" "q3:⟨{x}⟩⇩I"
"∀k∈?Y. q3 ⋅ k = 𝟬"
have q3:"q3∈R" using q(3) generated_ideal_is_ideal as(1)
ideal_dest_subset by auto
{
fix q4 assume q4:"q4∈?Y"
from yy q4 q(2) have "q2 ⋅ q4 :?Y" using ideal_dest_mult(2) by auto
moreover have "q1 ⋅ q3 ⋅ q2 ⋅ q4 = q1 ⋅ (q3 ⋅ (q2 ⋅ q4))"
using q(1-2) q3 q4 yy(2) Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) by auto
moreover note q(4) ultimately
have "q1 ⋅ q3 ⋅ q2 ⋅ q4 = q1 ⋅ 𝟬" by auto
then have "q1 ⋅ q3 ⋅ q2 ⋅ q4 = 𝟬" using Ring_ZF_1_L6(2) q(1) by auto
}
then have "∀za∈⟨{y}⟩⇩I. q1 ⋅ q3 ⋅ q2 ⋅ za = 𝟬" by auto
}
then show "∀ya∈R. ∀z∈R. ∀q∈⟨{x}⟩⇩I. (∀z∈⟨{y}⟩⇩I. q ⋅ z = 𝟬) ⟶
(∀za∈⟨{y}⟩⇩I. ya ⋅ q ⋅ z ⋅ za = 𝟬)" by auto
{
fix q1 q2 assume q:"q1:R" "q2:R" "∀z∈⟨{y}⟩⇩I. q1 ⋅ z = 𝟬" "∀za∈⟨{y}⟩⇩I. q2 ⋅ za = 𝟬"
{
fix q3 assume "q3∈?Y"
have "(q1 \<ra> q2) ⋅ q3 = (q1⋅q3) \<ra> (q2⋅q3)" using ring_oper_distr(2)
q(1,2) `q3:?Y` yy(2) by auto
with q(3,4) have "(q1 \<ra> q2) ⋅ q3 = 𝟬 \<ra> 𝟬" using `q3:?Y` by auto
then have "(q1 \<ra> q2) ⋅ q3 = 𝟬" using Ring_ZF_1_L3(3) Ring_ZF_1_L2(1) by auto
}
then have "∀q∈?Y. (q1 \<ra> q2) ⋅ q = 𝟬" by auto
}
then show "∀ya∈R.
∀z∈R. (∀z∈⟨{y}⟩⇩I. ya ⋅ z = 𝟬) ∧ (∀za∈⟨{y}⟩⇩I. z ⋅ za = 𝟬) ⟶
(∀za∈⟨{y}⟩⇩I. (ya \<ra> z) ⋅ za = 𝟬)" by auto
qed
{
fix q assume "q∈M``(?X×?Y)"
then obtain qx qy where q:"qx:?X" "qy:?Y" "q=qx⋅qy"
using func_imagedef[OF MR XY] by auto
with xy have "q=𝟬" by auto
}
then have "M``(?X×?Y) ⊆ {𝟬}" by auto
then have "?X⋅⇩I?Y ⊆ {𝟬}" using generated_ideal_small
zero_ideal productIdeal_def generated_ideal_is_ideal
as(1,2) by auto
then have "?X ⊆ {𝟬} ∨ ?Y ⊆ {𝟬}" using assms unfolding primeIdeal_def
using generated_ideal_is_ideal as(1,2) ideal_dest_subset by auto
then have "x=𝟬 ∨ y =𝟬" using generated_ideal_contains_set
as(1,2) by auto
}
then have " ∀x∈R. ∀y∈R. (∀z∈R. x ⋅ z ⋅ y = 𝟬) ⟶ x = 𝟬 ∨ y = 𝟬" by auto
then show ?thesis unfolding primeRing_def[OF ringAssum] by auto
qed
text‹We can actually use this definition of a prime ring,
as a condition to check for prime ideals.›
theorem (in ring0) equivalent_prime_ideal:
assumes "P◃⇩pR"
shows "∀x∈R. ∀y∈R. (∀z∈R. x⋅z⋅y∈P) ⟶ x∈P ∨ y∈P"
proof(safe)
fix x y assume as:"x∈R" "y∈R" "∀z∈R. x⋅z⋅y∈P" "y∉P"
let ?X="⟨{x}⟩⇩I"
let ?Y="⟨{y}⟩⇩I"
from as(3) have "∀x∈{x}. ∀u∈R. x ⋅ u ⋅ y ∈ P" by auto moreover
have "∀ya∈R.
∀z∈R. ∀q∈?X. (∀u∈R. q ⋅ u ⋅ y ∈ P) ⟶ (∀u∈R. ya ⋅ q ⋅ z ⋅ u ⋅ y ∈ P)"
proof(safe)
fix ya z q u assume ass:"ya∈R" "z∈R" "q∈?X" "∀u∈R. q ⋅ u ⋅ y ∈ P" "u ∈ R"
from ass(3) have q:"q∈R" using generated_ideal_is_ideal[THEN ideal_dest_subset]
as(1) by auto
from ass(2,5) have "z⋅u∈R" using Ring_ZF_1_L4(3) by auto
with ass(4) have "q⋅(z⋅u)⋅y:P" by auto
with ass(1) have "ya⋅(q⋅(z⋅u)⋅y)∈P" using assms
unfolding primeIdeal_def using ideal_dest_mult(2) by auto
then show "ya⋅q⋅z⋅u⋅y∈P" using Ring_ZF_1_L4(3)
Ring_ZF_1_L11(2) ass(1,2,5) as(2) q by auto
qed
moreover
have "∀ya∈R.
∀z∈R. (∀u∈R. ya ⋅ u ⋅ y ∈ P) ∧ (∀u∈R. z ⋅ u ⋅ y ∈ P) ⟶
(∀u∈R. (ya \<ra> z) ⋅ u ⋅ y ∈ P)"
proof(safe)
fix ya z u assume ass:"ya∈R" "z∈R" "u∈R"
"∀u∈R. ya ⋅ u ⋅ y ∈ P" "∀u∈R. z ⋅ u ⋅ y ∈ P"
from ass(3-5) have "ya ⋅ u ⋅ y ∈ P" "z ⋅ u ⋅ y ∈ P" by auto
then have "(ya ⋅ u ⋅ y)\<ra>(z ⋅ u ⋅ y) ∈ P" using
ideal_dest_sum assms unfolding primeIdeal_def by auto
then have "((ya⋅u)\<ra>(z⋅u))⋅y∈P" using ring_oper_distr(2)
as(2) Ring_ZF_1_L4(3) ass(1-3) by auto
then show "((ya\<ra>z)⋅u)⋅y∈P" using ring_oper_distr(2)
ass(1-3) by auto
qed
ultimately have R:"∀ya∈⟨{x}⟩⇩I. ∀u∈R. ya ⋅ u ⋅ y ∈ P"
using induction_generated_ideal[of "{x}" "λt. ∀u∈R. t⋅u⋅y ∈ P"]
as(1) by auto
then have "∀xa∈{y}. ∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ xa ∈ P" by auto moreover
have "∀ya∈R.
∀z∈R. ∀q∈⟨{y}⟩⇩I.
(∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ q ∈ P) ⟶
(∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ (ya ⋅ q ⋅ z) ∈ P)"
proof(safe)
fix ya z q t u assume ass:"ya∈R" "z∈R" "q∈?Y" "∀t∈?X. ∀u∈R. t ⋅ u ⋅ q ∈ P"
"t∈?X" "u∈R"
from ass(3,5) have qt:"q:R" "t∈R" using generated_ideal_is_ideal
ideal_dest_subset as(1,2) by auto
from ass(1,6) have "u⋅ya:R" using Ring_ZF_1_L4(3) by auto
with ass(4,5) have "t⋅(u⋅ya)⋅q ∈P" by auto
then have "(t⋅(u⋅ya)⋅q)⋅z∈P" using ass(2) assms
ideal_dest_mult(1) unfolding primeIdeal_def by auto
then show "t ⋅ u ⋅ (ya ⋅ q ⋅ z) ∈P" using
Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) ass(1,2,6) qt by auto
qed moreover
have "∀y∈R. ∀z∈R. (∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ y ∈ P) ∧
(∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ z ∈ P) ⟶
(∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ (y \<ra> z) ∈ P)"
proof(safe)
fix ya z t u assume ass:"ya∈R" "z∈R" "t∈?X" "u∈R"
"∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ ya ∈ P" "∀t∈⟨{x}⟩⇩I. ∀u∈R. t ⋅ u ⋅ z ∈ P"
from ass(3) have "t∈R" using ideal_dest_subset generated_ideal_is_ideal
as(1) by auto
from ass(3-6) have "t ⋅ u ⋅ ya ∈ P" "t ⋅ u ⋅ z ∈ P" by auto
then have "(t ⋅ u ⋅ ya)\<ra>(t ⋅ u ⋅ z) ∈P" using assms
unfolding primeIdeal_def using ideal_dest_sum by auto
then have "t⋅((u⋅ya)\<ra>(u⋅z)) ∈P" using ring_oper_distr(1)
`t∈R` Ring_ZF_1_L4(3) ass(4,2,1) Ring_ZF_1_L11 by auto
then have "t⋅(u⋅(ya\<ra>z)) ∈P" using ring_oper_distr(1)
ass(1,2,4) by auto
then show "t⋅u⋅(ya\<ra>z) ∈P" using Ring_ZF_1_L11(2)
Ring_ZF_1_L4(1) ass(1,2,4) `t∈R` by auto
qed
ultimately have R:"∀q∈?Y. ∀t∈?X. ∀u∈R. t⋅u⋅q ∈ P"
using induction_generated_ideal[of "{y}" "λq. ∀t∈?X. ∀u∈R. t⋅u⋅q ∈ P"]
as(2) by auto
have "?X⊆R" "?Y⊆R" using ideal_dest_subset
generated_ideal_is_ideal as(1,2) by auto
then have subprd:"?X×?Y ⊆ R×R" by auto
{
fix t assume "t∈M``(?X×?Y)"
then obtain tx ty where t:"tx∈?X" "ty∈?Y" "t= tx⋅ty"
using func_imagedef[of M "R×R" R "?X×?Y"]
subprd ringAssum unfolding IsAring_def
IsAmonoid_def IsAssociative_def by auto
from this(1,2) have "tx⋅𝟭⋅ty ∈P" using R Ring_ZF_1_L2(2)
by auto moreover
from t(1) have "tx∈R" using generated_ideal_is_ideal[THEN
ideal_dest_subset] as(1) by auto
ultimately have "t∈P" using Ring_ZF_1_L3(5) t(3) by auto
}
then have "M``(?X×?Y) ⊆ P" by auto
then have "?X⋅⇩I?Y ⊆ P" using generated_ideal_small
assms unfolding primeIdeal_def using productIdeal_def[
OF generated_ideal_is_ideal generated_ideal_is_ideal]
as(1,2) by auto moreover
have "?X:ℐ" "?Y:ℐ"
using generated_ideal_is_ideal generated_ideal_is_ideal[THEN ideal_dest_subset]
as(1,2) by auto
ultimately have "?X ⊆ P ∨ ?Y ⊆ P" using assms
unfolding primeIdeal_def by auto
with as(4) generated_ideal_contains_set as(2)
have "?X ⊆ P" by auto
then show "x∈P" using generated_ideal_contains_set as(1) by auto
qed
theorem (in ring0) equivalent_prime_ideal_2:
assumes "∀x∈R. ∀y∈R. (∀z∈R. x⋅z⋅y∈P) ⟶ x∈P ∨ y∈P" "P◃R" "P≠R"
shows "P◃⇩pR" unfolding primeIdeal_def apply(safe)
using assms(2) apply simp
using assms(3) apply simp
proof-
fix I J x xa assume as:"I◃R" "I⊆R" "J◃R" "J⊆R" "I ⋅⇩I J ⊆ P" "x ∈ J" "x ∉ P" "xa ∈ I"
from as(4,2) have prdsub:"I×J ⊆ R×R" by auto
{
fix z assume z:"z∈R"
then have "xa⋅z∈I" using as(1,8) ideal_dest_mult(1) by auto
then have "⟨xa⋅z,x⟩∈I×J" using as(6) by auto
then have "(xa⋅z⋅x)∈M``(I×J)" using func_imagedef[of M "R×R" R
"I×J"] prdsub ringAssum unfolding IsAring_def IsAmonoid_def
IsAssociative_def by auto
then have "(xa⋅z⋅x)∈⟨M``(I×J)⟩⇩I" using generated_ideal_contains_set
[OF func1_1_L6(2)[of M "R×R" R]] ringAssum
unfolding IsAring_def IsAmonoid_def
IsAssociative_def by force
then have "(xa⋅z⋅x)∈ I⋅⇩IJ" using productIdeal_def
as(1,3) by auto
with as(5) have "xa⋅z⋅x∈P" by auto
}
then have "∀z∈R. xa⋅z⋅x ∈ P" by auto
moreover have "xa∈R" "x∈R" using as(2,4,6,8) by auto
with assms(1) have "(∀z∈R. xa ⋅ z ⋅ x ∈ P) ⟶ x ∈ P ∨ xa ∈ P" by auto
ultimately have "x∈P ∨ xa∈P" by auto
with as(7) show "xa∈P" by auto
qed
subsection‹Ring quotient›
text‹Similar to groups, rings can be quotiented by normal additive subgroups;
but to keep the structure of the multiplicative monoid we need extra structure
in the normal subgroup. This extra structure is given by the ideal.›
text‹Any ideal is a normal subgroup›
lemma (in ring0) ideal_normal_add_subgroup:
assumes "I◃R"
shows "IsAnormalSubgroup(R,A,I)"
using Group_ZF_2_4_L6(1) using ringAssum
unfolding IsAring_def using assms unfolding Ideal_def by auto
definition (in ring0) QuotientBy where
"I◃R ⟹ QuotientBy(I) ≡ R//QuotientGroupRel(R,A,I)"
text‹Any ideal gives rise to an equivalent relation›
corollary (in ring0) equiv_rel:
assumes "I◃R"
shows "equiv(R,QuotientGroupRel(R,A,I))"
using assms add_group.Group_ZF_2_4_L3 unfolding Ideal_def
by auto
text‹Any quotient by an ideal is an abelian group›
lemma (in ring0) quotientBy_add_group:
assumes "I◃R"
shows "IsAgroup(QuotientBy(I), QuotientGroupOp(R, A, I))" and
"QuotientGroupOp(R, A, I) {is commutative on} QuotientBy(I)"
proof-
from Group_ZF_2_4_T1[of R A I] show "IsAgroup(QuotientBy(I), QuotientGroupOp(R, A, I))"
using ideal_normal_add_subgroup[OF assms]
ringAssum unfolding QuotientBy_def[OF assms] IsAring_def by auto
from Group_ZF_2_4_L6(2) show "QuotientGroupOp(R, A, I) {is commutative on} QuotientBy(I)"
using ringAssum unfolding IsAring_def QuotientBy_def[OF assms]
using assms unfolding Ideal_def by auto
qed
text‹The multiplicative monoid is congruent with the quotient relation
and gives rise to a monoid in the quotient›
lemma (in ring0) quotientBy_mul_monoid:
assumes "I◃R"
shows "Congruent2(QuotientGroupRel(R, A, I),M)" and
"IsAmonoid(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R,A,I), M))"
proof-
{
fix x y s t assume "⟨x,y⟩∈QuotientGroupRel(R,A,I)" "⟨s,t⟩∈QuotientGroupRel(R,A,I)"
then have xyst:"x∈R" "y∈R" "s∈R" "t∈R" "x\<rs>y ∈I" "s\<rs>t ∈I"
unfolding QuotientGroupRel_def by auto
have "(x⋅s)\<rs>(y⋅t) = (x⋅s)\<ra>𝟬\<rs>(y⋅t)"
using Ring_ZF_1_L3(3) Ring_ZF_1_L4(3)[OF xyst(1,3)] by auto
then have "(x⋅s)\<rs>(y⋅t) = ((x⋅s)\<ra>((\<rm>(y⋅s))\<ra>(y⋅s)))\<rs>(y⋅t)"
using Ring_ZF_1_L3(7)[of "y⋅s"] Ring_ZF_1_L4(3)[OF xyst(2,3)]
Ring_ZF_1_L4(4)[of "\<rm>(y⋅s)" "y⋅s"] Ring_ZF_1_L3(1)[of "y⋅s"]
by auto
then have "(x⋅s)\<rs>(y⋅t) = ((x⋅s)\<rs>(y⋅s))\<ra>((y⋅s)\<rs>(y⋅t))"
using Ring_ZF_1_L3(1) Ring_ZF_1_L4(1,2)
Ring_ZF_1_L10(1)[of "x⋅s" "\<rm>(y⋅s)" "y⋅s"]
Ring_ZF_1_L10(1)[of "(x⋅s)\<rs>(y⋅s)" "y⋅s" "\<rm>(y⋅t)"]
Ring_ZF_1_L4(3)[OF xyst(1,3)] Ring_ZF_1_L4(3)[OF xyst(2,3)]
Ring_ZF_1_L4(3)[OF xyst(2,4)] by auto
then have "(x⋅s)\<rs>(y⋅t) = ((x\<rs>y)⋅s)\<ra>(y⋅(s\<rs>t))"
using Ring_ZF_1_L8 xyst(1-4) by auto
moreover
have "(x\<rs>y)⋅s ∈I" using xyst(3,5) assms
ideal_dest_mult(1) by auto
moreover
have "y⋅(s\<rs>t) ∈I" using xyst(2,6) assms
ideal_dest_mult(2) by auto
ultimately have "(x⋅s)\<rs>(y⋅t) ∈I" using assms
ideal_dest_sum by auto
then have "⟨M ` ⟨x, s⟩, M ` ⟨y, t⟩⟩ ∈ QuotientGroupRel(R, A, I)"
unfolding QuotientGroupRel_def using Ring_ZF_1_L4(3)
xyst(1-4) by auto
}
then show "Congruent2(QuotientGroupRel(R, A, I),M)"
unfolding Congruent2_def by auto moreover
have "equiv(R,QuotientGroupRel(R,A,I))" using add_group.Group_ZF_2_4_L3
assms unfolding Ideal_def by auto
moreover note mult_monoid.Group_ZF_2_2_T1
ultimately show "IsAmonoid(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R,A,I), M))" unfolding QuotientBy_def[OF assms] by auto
qed
definition (in ring0) ideal_radd ("_{\<ra>_}_") where
"x{\<ra>I}y ≡ QuotientGroupOp(R, A, I)`⟨x,y⟩"
definition (in ring0) ideal_rmult ("_{⋅_}_") where
"x{⋅I}y ≡ ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩"
definition (in ring0) ideal_rmin ("{\<rm>_}_") where
"{\<rm>I}y ≡ GroupInv(QuotientBy(I),QuotientGroupOp(R, A, I))`y"
definition (in ring0) ideal_rsub ("_{\<rs>_}_") where
"x{\<rs>I}y ≡ x{\<ra>I}({\<rm>I}y)"
definition (in ring0) ideal_rzero ("𝟬⇩_") where
"𝟬⇩I ≡ QuotientGroupRel(R,A,I)``{𝟬}"
definition (in ring0) ideal_rone ("𝟭⇩_") where
"𝟭⇩I ≡ QuotientGroupRel(R,A,I)``{𝟭}"
definition (in ring0) ideal_rtwo ("𝟮⇩_") where
"𝟮⇩I ≡ QuotientGroupRel(R,A,I)``{𝟮}"
definition (in ring0) ideal_rsqr ("_⇧2⇧_") where
"x⇧2⇧I ≡ ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,x⟩"
lemma (in ring0) neutral_quotient:
assumes "I◃R"
shows "QuotientGroupRel(R,A,I)``{𝟬} = TheNeutralElement(QuotientBy(I),QuotientGroupOp(R, A, I))"
using Group_ZF_2_4_L5B[of R A I "QuotientGroupRel(R, A, I)" 𝟬] ideal_normal_add_subgroup[OF assms]
ringAssum unfolding IsAring_def QuotientBy_def[OF assms] by auto
lemma (in ring0) one_quotient:
assumes "I◃R"
shows "QuotientGroupRel(R,A,I)``{𝟭} = TheNeutralElement(QuotientBy(I),ProjFun2(R, QuotientGroupRel(R, A, I), M))"
using Group_ZF_2_2_L1[of R M "QuotientGroupRel(R, A, I)"
"ProjFun2(R, QuotientGroupRel(R, A, I), M)" 𝟭]
equiv_rel[OF assms] quotientBy_mul_monoid[OF assms]
ringAssum unfolding IsAring_def QuotientBy_def[OF assms] by auto
lemma (in ring0) two_quotient:
assumes "I◃R"
shows "QuotientGroupRel(R,A,I)``{𝟮} = QuotientGroupOp(R, A, I)`⟨QuotientGroupRel(R,A,I)``{𝟭},QuotientGroupRel(R,A,I)``{𝟭}⟩"
proof-
have "QuotientGroupRel(R,A,I)``{𝟮} = QuotientGroupRel(R,A,I)``{𝟭\<ra>𝟭}"
unfolding ringtwo_def by auto
then show "QuotientGroupRel(R,A,I)``{𝟮} = QuotientGroupOp(R, A, I)`⟨QuotientGroupRel(R,A,I)``{𝟭}, QuotientGroupRel(R,A,I)``{𝟭}⟩"
using EquivClass_1_L10[OF equiv_rel[OF assms] _
Ring_ZF_1_L2(2) Ring_ZF_1_L2(2), of A]
Group_ZF_2_4_L5A[of R A I] ringAssum
ideal_normal_add_subgroup[OF assms]
unfolding IsAring_def QuotientGroupOp_def by auto
qed
lemma (in ring0) sqrt_quotient:
assumes "I◃R" "x∈R"
shows "QuotientGroupRel(R,A,I)``{x⇧2} = ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupRel(R,A,I)``{x},QuotientGroupRel(R,A,I)``{x}⟩"
proof-
have "QuotientGroupRel(R,A,I)``{x⇧2} = QuotientGroupRel(R,A,I)``{x⋅x}"
unfolding ringsq_def by auto
then show ?thesis using EquivClass_1_L10[OF equiv_rel[OF assms(1)]
quotientBy_mul_monoid(1)[OF assms(1)] assms(2,2)] by auto
qed
text‹Both quotient operations are distributive›
lemma (in ring0) quotientBy_distributive:
assumes "I◃R"
shows "IsDistributive(QuotientBy(I),QuotientGroupOp(R, A, I),ProjFun2(R, QuotientGroupRel(R,A,I), M))"
proof-
{
fix x y z assume xyz:"x∈QuotientBy(I)" "y∈QuotientBy(I)" "z∈QuotientBy(I)"
then obtain x1 y1 z1 where xyz1:"x1∈R" "y1∈R" "z1∈R"
"QuotientGroupRel(R,A,I)``{x1} =x"
"QuotientGroupRel(R,A,I)``{y1} =y"
"QuotientGroupRel(R,A,I)``{z1} =z"
unfolding QuotientBy_def[OF assms] quotient_def by auto
have aux:"QuotientGroupOp(R, A, I)`⟨y,z⟩ = QuotientGroupRel(R,A,I)``{y1\<ra>z1}"
using EquivClass_1_L10[OF equiv_rel Group_ZF_2_4_L5A] unfolding
QuotientGroupOp_def using assms ringAssum ideal_normal_add_subgroup
unfolding IsAring_def using xyz1(2,3,5,6) by auto
then have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,QuotientGroupOp(R, A, I)`⟨y,z⟩⟩ = QuotientGroupRel(R,A,I)``{x1⋅(y1\<ra>z1)}"
using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)]
assms xyz1(1-4) Ring_ZF_1_L4(1) by auto
moreover have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩ = QuotientGroupRel(R,A,I)``{x1⋅y1}"
"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩ = QuotientGroupRel(R,A,I)``{x1⋅z1}"
using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)]
assms xyz1 by auto
then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩ = QuotientGroupRel(R,A,I)``{(x1⋅y1)\<ra>(x1⋅z1)}"
using EquivClass_1_L10[OF equiv_rel Group_ZF_2_4_L5A] unfolding
QuotientGroupOp_def using assms ringAssum ideal_normal_add_subgroup
unfolding IsAring_def using Ring_ZF_1_L4(3) xyz1(1-3) by auto
then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩ = QuotientGroupRel(R,A,I)``{x1⋅(y1\<ra>z1)}"
using ring_oper_distr(1) xyz1 by auto
ultimately have A:"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,QuotientGroupOp(R, A, I)`⟨y,z⟩⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩"
by auto
from aux have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupOp(R, A, I)`⟨y,z⟩,x⟩ = QuotientGroupRel(R,A,I)``{(y1\<ra>z1)⋅x1}"
using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)]
assms xyz1(1-4) Ring_ZF_1_L4(1) by auto
moreover have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩ = QuotientGroupRel(R,A,I)``{y1⋅x1}"
"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩ = QuotientGroupRel(R,A,I)``{z1⋅x1}"
using EquivClass_1_L10[OF equiv_rel quotientBy_mul_monoid(1)]
assms xyz1 by auto
then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩ = QuotientGroupRel(R,A,I)``{(y1⋅x1)\<ra>(z1⋅x1)}"
using EquivClass_1_L10[OF equiv_rel Group_ZF_2_4_L5A] unfolding
QuotientGroupOp_def using assms ringAssum ideal_normal_add_subgroup
unfolding IsAring_def using Ring_ZF_1_L4(3) xyz1(1-3) by auto
then have "QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩ = QuotientGroupRel(R,A,I)``{(y1\<ra>z1)⋅x1}"
using ring_oper_distr(2) xyz1 by auto
ultimately have B:"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupOp(R, A, I)`⟨y,z⟩,x⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩"
by auto
with A have "ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,QuotientGroupOp(R, A, I)`⟨y,z⟩⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,z⟩⟩"
"ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨QuotientGroupOp(R, A, I)`⟨y,z⟩,x⟩ = QuotientGroupOp(R, A, I)`⟨ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨y,x⟩,ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨z,x⟩⟩" by auto
}
with IsDistributive_def show "IsDistributive
(QuotientBy(I), QuotientGroupOp(R, A, I),
ProjFun2(R, QuotientGroupRel(R, A, I), M))" by auto
qed
text‹The quotient group is a ring with the quotient multiplication›
theorem (in ring0) quotientBy_is_ring:
assumes "I◃R"
shows "IsAring(QuotientBy(I), QuotientGroupOp(R, A, I), ProjFun2(R, QuotientGroupRel(R, A, I), M))"
unfolding IsAring_def using quotientBy_distributive[OF assms]
quotientBy_mul_monoid(2)[OF assms] quotientBy_add_group[OF assms]
by auto
text‹An import property satisfied by many important rings is
being Noetherian: every ideal is finitely generated.›
definition (in ring0) isFinGen ("_{is finitely generated}") where
"I◃R ⟹ I{is finitely generated} ≡ ∃S∈FinPow(R). I = ⟨S⟩⇩I"
text‹For noetherian rings the arbitrary sum can be reduced
to the sum of a finite subset of the initial set of ideals›
theorem (in ring0) sum_ideals_noetherian:
assumes "∀I∈ℐ. (I{is finitely generated})" "𝒥 ⊆ ℐ"
shows "∃𝒯∈FinPow(𝒥). (⊕⇩I𝒥) = (⊕⇩I𝒯)"
proof-
have JR:"(⊕⇩I𝒥)◃R" using generated_ideal_is_ideal[of "⋃𝒥"]
assms(2) unfolding sumArbitraryIdeals_def[OF assms(2)]
by auto
with assms(1) have "(⊕⇩I𝒥) {is finitely generated}"
using ideal_dest_subset by auto
then obtain S where S:"S∈FinPow(R)" "(⊕⇩I𝒥) = ⟨S⟩⇩I"
unfolding isFinGen_def[OF JR] by auto
from this(1) have fins:"Finite(S)" unfolding FinPow_def
by auto
then obtain n where n:"n∈nat" "S≈n" unfolding Finite_def by auto
then have "S≲n" using eqpoll_iff by auto moreover
let ?N = "λs∈S. {J∈FinPow(𝒥). s∈(⊕⇩IJ)}"
from n(1) have "{the axiom of} n {choice holds}" using finite_choice
by auto
ultimately have "(∀t∈S. ?N ` t ≠ 0) ⟶
(∃f. f ∈ (∏t∈S. ?N ` t) ∧ (∀t∈S. f ` t ∈ ?N ` t))"
unfolding AxiomCardinalChoiceGen_def by blast moreover
{
fix t assume t:"t∈S"
then have "?N`t = {J∈FinPow(𝒥). t∈(⊕⇩IJ)}" using lamE by auto
moreover from t have "t∈⟨S⟩⇩I" using generated_ideal_contains_set
S(1) unfolding FinPow_def by auto
with S(2) have "t∈(⊕⇩I𝒥)" by auto
ultimately have "?N`t≠0" using sum_ideals_finite_sum[OF assms(2)]
by auto
}
ultimately obtain f where f:"f:(∏t∈S. ?N ` t)" "∀t∈S. f ` t ∈ ?N ` t"
by auto
{
fix y assume "y∈f``S"
with image_iff obtain x where x:"x∈S" "⟨x,y⟩∈f" by auto
with f(1) have "y∈?N`x" unfolding Pi_def by auto
then have "y:{J∈FinPow(𝒥). x∈(⊕⇩IJ)}" using x(1) lamE by auto
then have "Finite(y)" using lamE unfolding FinPow_def by auto
}
moreover
from f(1) have f_Fun:"f:S→ (⋃{?N`t. t:S})" unfolding Pi_def
Sigma_def by blast
then have "Finite(f``S)" using Finite1_L6A[of f S _ S]
Finite_Fin_iff fins Fin_into_Finite by auto
ultimately have A:"Finite(⋃(f``S))" using Finite_Union by auto
{
fix t assume "t∈⋃(f``S)"
then obtain q where q:"t∈q" "q∈f``S" by auto
then obtain s where s:"t∈f`s" "s∈S" using
func_imagedef[OF f_Fun] by auto
from s(2) have J:"f`s∈FinPow(𝒥)" "s∈(⊕⇩I(f`s))"
using f(2) lamE by auto
with s(1) have "t:𝒥" unfolding FinPow_def by auto
}
with A have B:"(⋃(f``S)):FinPow(𝒥)" unfolding FinPow_def by auto
then have P:"(⋃(f``S)) ⊆ 𝒥" unfolding FinPow_def by auto
then have C:"(⋃(f``S)) ⊆ ℐ" using assms(2) by auto
then have "(⋃(f``S)) ⊆ Pow(R)" by auto
then have sub:"⋃(⋃(f``S)) ⊆ R" by auto
{
fix t assume t:"t∈S"
then have J:"f`t∈FinPow(𝒥)" "t∈(⊕⇩I(f`t))"
using f(2) lamE by auto
from t have "⋃(f`t) ⊆ ⋃(⋃(f``S))" using func_imagedef[OF f_Fun]
by auto
then have "⋃(f`t) ⊆ ⟨⋃(⋃(f``S))⟩⇩I" using generated_ideal_contains_set
sub by blast
then have "⟨⋃(f`t)⟩⇩I ⊆ ⟨⋃(⋃(f``S))⟩⇩I" using
generated_ideal_is_ideal[OF sub] generated_ideal_small
by auto
moreover have "f`t ⊆ ℐ" using J(1) assms(2) unfolding FinPow_def by auto
moreover note J(2)
ultimately have "t∈⟨⋃(⋃(f``S))⟩⇩I" using sumArbitraryIdeals_def
by auto
then have "t∈(⊕⇩I(⋃(f``S)))" using sumArbitraryIdeals_def
C by auto
}
then have "S ⊆ ⊕⇩I(⋃(f``S))" by auto
then have "⟨S⟩⇩I ⊆ ⊕⇩I(⋃(f``S))" using generated_ideal_small[
OF _ generated_ideal_is_ideal[OF sub]]
sumArbitraryIdeals_def[OF C] by auto
with S(2) have "(⊕⇩I𝒥)⊆ ⊕⇩I(⋃(f `` S))" by auto
moreover
from P have "⋃(⋃(f``S)) ⊆ ⋃𝒥" by auto
then have "⋃(⋃(f``S)) ⊆⟨⋃𝒥⟩⇩I" using
generated_ideal_contains_set[of "⋃𝒥"]
assms(2) by blast
then have "⟨⋃(⋃(f``S))⟩⇩I ⊆ ⟨⋃𝒥⟩⇩I" using generated_ideal_small[OF _
generated_ideal_is_ideal] assms(2) by blast
then have "(⊕⇩I(⋃(f `` S))) ⊆(⊕⇩I𝒥)" unfolding
sumArbitraryIdeals_def[OF assms(2)]
sumArbitraryIdeals_def[OF C].
ultimately have "(⊕⇩I𝒥) = ⊕⇩I(⋃(f `` S))" by auto
with B show ?thesis by auto
qed
end