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.›
subsection‹Ideals›
text‹In ring theory ideals are special subsets of a ring that play a similar role
as normal subgroups in the group theory. ›
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 will write ‹ℐ› to denote
the set of ideals of the ring $R$. ›
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) ring_self_ideal:
shows "R ◃R"
using add_group.group_self_subgroup Ring_ZF_1_L4(3)
unfolding Ideal_def by simp
text‹The singleton containing zero is and ideal.›
lemma (in ring0) zero_ideal:
shows "{𝟬} ◃R" unfolding Ideal_def
using Ring_ZF_1_L6 add_group.unit_singl_subgr by auto
text‹An ideal is s subset of the the ring.›
lemma (in ring0) ideal_dest_subset:
assumes "I ◃R"
shows "I ⊆ R" using assms add_group.group0_3_L2
unfolding Ideal_def by auto
text‹Ideals are closed with respect to the ring addition.›
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
text‹Ideals are closed with respect to the ring multiplication.›
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
text‹Ideals are closed with respect to taking the opposite in the ring.›
lemma (in ring0) ideal_dest_minus:
assumes "I ◃R" "x∈I"
shows "(\<rm>x) ∈ I"
using assms add_group.group0_3_T3A unfolding Ideal_def by auto
text‹Every ideals contains zero.›
lemma (in ring0) ideal_dest_zero:
assumes "I ◃R"
shows "𝟬 ∈ I"
using assms add_group.group0_3_L5 unfolding Ideal_def by auto
text‹If the rules are satisfied, then we have an ideal›
theorem (in ring0) ideal_intro:
assumes "∀x∈I. ∀y∈I. x\<ra>y∈I"
"∀x∈I. ∀y∈R. x⋅y ∈I"
"∀x∈I. ∀y∈R. y⋅x ∈I"
"I ⊆ R" "I≠0"
shows "I◃R"
proof -
{ fix x assume "x∈I"
with assms(4) have "(\<rm>x)∈R" using Ring_ZF_1_L3(1) by auto
then have "(\<rm>x) = 𝟭⋅(\<rm>x)" using Ring_ZF_1_L3(6) by auto
with assms(4) ‹x∈I› have "(\<rm>x) = \<rm>(𝟭⋅x)"
using Ring_ZF_1_L7(2) Ring_ZF_1_L2(2) by auto
with assms(4) ‹x∈I› have "(\<rm>x) = (\<rm>𝟭)⋅x"
using Ring_ZF_1_L7(1) Ring_ZF_1_L2(2) by auto
with assms(3) ‹x∈I› have "(\<rm>x) ∈I"
using Ring_ZF_1_L2(2) Ring_ZF_1_L3(1) by auto
} hence "∀x∈I. GroupInv(R, A)`(x) ∈ I" by auto
with assms(1,4,5) have "IsAsubgroup(I,A)"
using add_group.group0_3_T3 unfolding IsOpClosed_def by auto
moreover from assms(2,3) have "∀x∈I. ∀y∈R. y⋅x ∈ I ∧ x⋅y ∈ I" by auto
ultimately show ?thesis unfolding Ideal_def by auto
qed
text‹The simplest way to obtain an ideal from others is the intersection,
since the intersection of arbitrary collection of ideals is an ideal.›
theorem (in ring0) intersection_ideals:
assumes "∀J∈𝒥. (J ◃R)" "𝒥 ≠ 0"
shows "(⋂𝒥) ◃R"
using assms ideal_dest_mult add_group.subgroup_inter
unfolding Ideal_def by auto
text‹In particular, intersection of two ideals is an ideal.›
corollary (in ring0) inter_two_ideals: assumes "I◃R" "J◃R"
shows "(I∩J) ◃R"
proof -
let ?𝒥 = "{I,J}"
from assms have "∀J∈?𝒥. (J ◃R)" and "?𝒥 ≠ 0" by simp_all
then have "(⋂?𝒥) ◃R" using intersection_ideals by blast
thus ?thesis by simp
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"
proof -
let ?𝒥 = "{I∈ℐ. X ⊆ I}"
have "∀J ∈ ?𝒥. (J ◃R)" by auto
with assms have "(⋂?𝒥) ◃R" using ring_self_ideal intersection_ideals by blast
with assms show ?thesis using generatedIdeal_def by simp
qed
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 -
from assms have "I∈{J∈Pow(R). J ◃R ∧ X⊆J}"
using 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 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"
using assms ring_self_ideal generatedIdeal_def by auto
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
"X≠0"
"X⊆R"
"∀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∈X. P(x)"
shows "∀y∈⟨X⟩⇩I. P(y)"
proof -
let ?J = "{m∈⟨X⟩⇩I. P(m)}"
from assms(2,5) have "X⊆?J"
using generated_ideal_contains_set by auto
from assms(2) have "?J⊆R"
using generated_ideal_is_ideal ideal_dest_subset by auto
moreover
{ fix y z assume "y∈R" "z∈?J"
then have "y∈R" "𝟭∈R" "z∈⟨X⟩⇩I" "P(z)"
using Ring_ZF_1_L2(2) by simp_all
with assms(3) have "P(y⋅z⋅𝟭)" and "P(𝟭⋅z⋅y)" by simp_all
with ‹?J⊆R› ‹y∈R› ‹z∈?J› have "P(y⋅z)" and "P(z⋅y)"
using Ring_ZF_1_L4(3) Ring_ZF_1_L3(5,6) by auto
with assms(2) ‹z∈⟨X⟩⇩I› ‹y∈R› have "y⋅z∈?J" "z⋅y∈?J"
using ideal_dest_mult generated_ideal_is_ideal
by auto
} hence "∀x∈?J. ∀y∈R. y ⋅ x ∈ ?J ∧ x ⋅ y ∈ ?J" by auto
moreover have "IsAsubgroup(?J,A)"
proof -
from assms(1) ‹X⊆?J› ‹?J⊆R› have "?J≠0" and "?J⊆R"
by auto
moreover
{ fix x y assume as: "x∈?J" "y∈?J"
with assms(2,4) have "P(x\<ra>y)"
using ideal_dest_subset generated_ideal_is_ideal
by blast
with assms(2) ‹x∈?J› ‹y∈?J› have "x\<ra>y ∈ ?J"
using generated_ideal_is_ideal ideal_dest_sum
by auto
} then have "?J {is closed under} A"
unfolding IsOpClosed_def by auto
moreover
{ fix x assume "x∈?J"
with ‹?J⊆R› have "x∈⟨X⟩⇩I" "x∈R" "P(x)" by auto
with assms(3) have "P((\<rm>𝟭)⋅x⋅𝟭)"
using Ring_ZF_1_L2(2) Ring_ZF_1_L3(1) by simp
with assms(2) ‹x∈⟨X⟩⇩I› ‹x∈R› have "(\<rm>x)∈?J"
using Ring_ZF_1_L3(1,5,6) Ring_ZF_1_L7(1) Ring_ZF_1_L2(2)
generated_ideal_is_ideal ideal_dest_minus by auto
} hence "∀x∈?J. (\<rm>x)∈?J" by simp
ultimately show "IsAsubgroup(?J,A)"
by (rule add_group.group0_3_T3)
qed
ultimately have "?J◃R" unfolding Ideal_def by auto
with ‹X⊆?J› show ?thesis using generated_ideal_small by auto
qed
text‹An ideal is very particular with the elements it may contain.
If it contains the neutral element of multiplication then
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"
using assms ideal_dest_subset ideal_dest_mult(2) Ring_ZF_1_L3(5)
by force
text‹The only ideal containing an invertible element is the whole ring. ›
theorem (in ring0) ideal_with_unit:
assumes "I◃R" "x∈I" "∃y∈R. y⋅x = 𝟭 ∨ x⋅y =𝟭"
shows "I = R"
using assms ideal_with_one unfolding Ideal_def by blast
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.
The product ideal of ideals $I,J$ is the smallest ideal containing all
products of elements from $I$ and $J$: ›
definition (in ring0) productIdeal (infix "⋅⇩I" 90) where
"I◃R ⟹ J◃R ⟹ I⋅⇩IJ ≡ ⟨M``(I×J)⟩⇩I"
text‹The sum ideal of ideals is the smallest ideal containg both $I$ and $J$: ›
definition (in ring0) sumIdeal (infix "+⇩I" 90) where
"I◃R ⟹ J◃R ⟹ I+⇩IJ ≡ ⟨I∪J⟩⇩I"
text‹Sometimes we may need to sum an arbitrary number
of ideals, and not just two.›
definition(in ring0) sumArbitraryIdeals ("⊕⇩I_" 90) where
"𝒥 ⊆ ℐ ⟹ ⊕⇩I𝒥 ≡ ⟨⋃𝒥⟩⇩I"
text‹Each component of the sum of ideals is contained in the sum.›
lemma (in ring0) comp_in_sum_ideals:
assumes "I◃R" and "J◃R"
shows "I ⊆ I+⇩IJ" and "J ⊆ I+⇩IJ" and "I∪J ⊆ I+⇩IJ"
proof -
from assms have "I∪J ⊆ R" using ideal_dest_subset
by auto
with assms show "I ⊆ I+⇩IJ" "J ⊆ I+⇩IJ" "I∪J ⊆ I+⇩IJ"
using generated_ideal_contains_set sumIdeal_def
by auto
qed
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
with assms(2) have ?thesis
using subset_Finite nat_into_Finite
unfolding FinPow_def by blast
}
moreover
{ let ?P = "λt. ∃𝒯∈FinPow(𝒥). t∈(⊕⇩I𝒯)"
assume "⋃𝒥≠0"
moreover from assms(1) have "⋃𝒥⊆R" by auto
moreover
{ fix y z q assume "?P(q)" "y∈R" "z∈R" "q∈⟨⋃𝒥⟩⇩I"
then obtain 𝒯 where "𝒯∈FinPow(𝒥)" and "q ∈ ⊕⇩I𝒯"
by auto
from assms(1) ‹𝒯∈FinPow(𝒥)› have "⋃𝒯 ⊆ R" "𝒯⊆ℐ"
unfolding FinPow_def by auto
with ‹q∈⊕⇩I𝒯› ‹y∈R› ‹z∈R› have "y⋅q⋅z ∈ ⊕⇩I𝒯"
using generated_ideal_is_ideal sumArbitraryIdeals_def
unfolding Ideal_def by auto
with ‹𝒯∈FinPow(𝒥)› have "?P(y⋅q ⋅z)" by auto
} hence "∀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 T⇩y T⇩z where T: "T⇩y∈FinPow(𝒥)" "y ∈ ⊕⇩IT⇩y"
"T⇩z∈FinPow(𝒥)" "z ∈ ⊕⇩IT⇩z" by auto
from T(1,3) have A: "T⇩y∪T⇩z ∈ FinPow(𝒥)"
unfolding FinPow_def using Finite_Un by auto
with assms(1) have "⋃T⇩y ⊆ ⋃(T⇩y∪T⇩z)" "⋃T⇩z ⊆ ⋃(T⇩y∪T⇩z)" and
sub: "⋃(T⇩y∪T⇩z) ⊆ R"
unfolding FinPow_def by auto
then have "⋃(T⇩y∪T⇩z) ⊆ ⟨⋃(T⇩y∪T⇩z)⟩⇩I"
using generated_ideal_contains_set by simp
hence "⋃T⇩y ⊆ ⟨⋃(T⇩y∪T⇩z)⟩⇩I" "⋃T⇩z ⊆ ⟨⋃(T⇩y∪T⇩z)⟩⇩I" by auto
with sub have "⟨⋃T⇩y⟩⇩I⊆ ⟨⋃(T⇩y∪T⇩z)⟩⇩I" "⟨⋃T⇩z⟩⇩I ⊆ ⟨⋃(T⇩y∪T⇩z)⟩⇩I"
using generated_ideal_small generated_ideal_is_ideal
by auto
moreover from assms(1) T(1,3) have "T⇩y⊆ℐ" "T⇩z⊆ℐ"
unfolding FinPow_def by auto
moreover note T(2,4)
ultimately have "y ∈ ⟨⋃(T⇩y∪T⇩z)⟩⇩I" "z ∈ ⟨⋃(T⇩y∪T⇩z)⟩⇩I"
using sumArbitraryIdeals_def sumArbitraryIdeals_def
by auto
with ‹⋃(T⇩y∪T⇩z) ⊆ R› have "y\<ra>z ∈ ⟨⋃(T⇩y∪T⇩z)⟩⇩I"
using generated_ideal_is_ideal ideal_dest_sum by auto
moreover
from ‹T⇩y⊆ℐ› ‹T⇩z⊆ℐ› have "T⇩y∪T⇩z ⊆ ℐ" by auto
then have "(⊕⇩I(T⇩y∪T⇩z)) = ⟨⋃(T⇩y∪T⇩z)⟩⇩I"
using sumArbitraryIdeals_def by auto
ultimately have "y\<ra>z ∈ (⊕⇩I(T⇩y∪T⇩z))" by simp
with A have "?P(y\<ra>z)" by auto
} hence "∀y∈R. ∀z∈R. ?P(y) ∧ ?P(z) ⟶ ?P(y \<ra> z)"
by auto
moreover
{ fix t assume "t∈⋃𝒥"
then obtain J where "t∈J" "J∈𝒥" by auto
then have "{J}∈FinPow(𝒥)" unfolding FinPow_def
using eqpoll_imp_Finite_iff nat_into_Finite
by auto
moreover
from assms(1) ‹J∈𝒥› have "(⊕⇩I{J}) = ⟨J⟩⇩I"
using sumArbitraryIdeals_def by auto
with assms(1) ‹t∈J› ‹J∈𝒥› have "t∈(⊕⇩I{J})"
using generated_ideal_contains_set by force
ultimately have "?P(t)" by auto
} hence "∀t∈⋃𝒥. ?P(t)" by auto
ultimately have "∀t∈⟨⋃𝒥⟩⇩I. ?P(t)"
by (rule induction_generated_ideal)
with assms have ?thesis using sumArbitraryIdeals_def
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 "M``(I×J) ⊆ I∩J"
proof
fix x assume "x∈M``(I×J)"
then obtain y where "y∈I×J" "⟨y,x⟩∈M" unfolding image_def
by auto
then obtain y⇩i y⇩j where y: "y⇩i∈I" "y⇩j∈J" "⟨⟨y⇩i,y⇩j⟩,x⟩ ∈ M"
by auto
from assms have "I⊆R" "J⊆R" using ideal_dest_subset by simp_all
with ringAssum assms y show "x∈I∩J"
unfolding Ideal_def IsAring_def IsAmonoid_def IsAssociative_def
using apply_equality by force
qed
with assms show "I⋅⇩IJ ⊆ I∩J"
using productIdeal_def generated_ideal_small inter_two_ideals
by auto
from assms ‹M``(I×J) ⊆ I∩J› have "M``(I×J) ⊆ R"
using ideal_dest_subset by auto
with assms show "(I⋅⇩IJ) ◃R" and "M``(I×J) ⊆ I⋅⇩IJ"
using productIdeal_def generated_ideal_is_ideal
generated_ideal_contains_set 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
with assms(3,4) have "x ∈ ⟨I∪J⟩⇩I" "y ∈ ⟨I∪J⟩⇩I"
using generated_ideal_contains_set by auto
with assms(1,2) ‹I∪J ⊆ R› show ?thesis
using generated_ideal_is_ideal ideal_dest_subset ideal_dest_sum
sumIdeal_def by auto
qed
text‹For two ideals the set containing all sums of their elements is also an ideal.›
lemma (in ring0) sum_elements_is_ideal:
assumes "I ◃R" "J ◃R"
shows "(A``(I×J)) ◃R"
proof -
from assms have ij: "I×J ⊆ R×R" using ideal_dest_subset by auto
have Aim: "A``(I×J) ⊆ R" using add_group.group_oper_fun func1_1_L6(2)
by auto
moreover
{ fix x y assume "x∈R" "y ∈ A``(I×J)"
from ij ‹y∈A``(I×J)› obtain y⇩i y⇩j where
y: "y=y⇩i\<ra>y⇩j" "y⇩i∈I" "y⇩j∈J"
using add_group.group_oper_fun func_imagedef by auto
from ‹x∈R› y ij have
"x⋅y = (x⋅y⇩i)\<ra>(x⋅y⇩j)" and "y⋅x = (y⇩i⋅x)\<ra>(y⇩j⋅x)"
using ring_oper_distr add_group.group_op_closed by auto
moreover from assms ‹x∈R› y(2,3) have
"x⋅y⇩i ∈ I" "y⇩i⋅x ∈ I" "x⋅y⇩j ∈ J" "y⇩j⋅x ∈ J"
using ideal_dest_mult by auto
ultimately have "x⋅y∈A``(I×J)" "y⋅x∈A``(I×J)"
using ij add_group.group_oper_fun func_imagedef by auto
} hence "∀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 -
from assms ij have "𝟬\<ra>𝟬 ∈ A `` (I × J)"
using add_group.group_oper_fun ideal_dest_zero func_imagedef
by auto
with Aim have "A``(I × J) ≠ 0" and "A``(I × J) ⊆ R"
by auto
moreover
{ fix x y assume xy: "x ∈ A``(I × J)" "y ∈ A``(I × J)"
with ij obtain x⇩i x⇩j y⇩i y⇩j where
"x⇩i∈I" "x⇩j∈J" "x=x⇩i\<ra>x⇩j" "y⇩i∈I" "y⇩j∈J" "y=y⇩i\<ra>y⇩j"
using add_group.group_oper_fun func_imagedef by auto
from ‹x∈A``(I × J)› ‹A``(I × J)⊆R› have "x∈R" by auto
from assms ‹x⇩i∈I› ‹x⇩j∈J› ‹y⇩i∈I› ‹y⇩j∈J›
have "x⇩i∈R" "x⇩j∈R" "y⇩i∈R" "y⇩j∈R"
using ideal_dest_subset by auto
from ij ‹x∈R› ‹y⇩i∈R› ‹y⇩j∈R› ‹y=y⇩i\<ra>y⇩j›
have "x\<ra>y = (x\<ra>y⇩i)\<ra>y⇩j"
using Ring_ZF_1_L10(1) by simp
with ‹x=x⇩i\<ra>x⇩j› ‹x⇩i∈R› ‹x⇩j∈R› ‹y⇩i∈R› ‹y⇩j∈R›
have "x\<ra>y = (x⇩i\<ra>y⇩i)\<ra>(x⇩j\<ra>y⇩j)"
using Ring_ZF_2_L5(4) by simp
moreover from assms ‹x⇩i∈I› ‹x⇩j∈J› ‹y⇩i∈I› ‹y⇩j∈J›
have "x⇩i\<ra>y⇩i ∈ I" and "x⇩j\<ra>y⇩j ∈ J"
using ideal_dest_sum by auto
ultimately have "x\<ra>y ∈ A``(I×J)"
using ij add_group.group_oper_fun func_imagedef
by auto
} then have "A``(I × J) {is closed under} A"
unfolding IsOpClosed_def by auto
moreover
{ fix x assume "x ∈ A``(I × J)"
with ij obtain x⇩i x⇩j where "x⇩i∈I" "x⇩j∈J" "x=x⇩i\<ra>x⇩j"
using add_group.group_oper_fun func_imagedef by auto
with assms have "(\<rm>x) = (\<rm>x⇩i)\<rs>x⇩j"
using Ring_ZF_1_L9(2) ideal_dest_subset by auto
moreover from assms ‹x⇩i∈I› ‹x⇩j∈J›
have "(\<rm>x⇩i)∈I" and "(\<rm>x⇩j)∈J"
using ideal_dest_minus by simp_all
ultimately have "(\<rm>x) ∈ A``(I×J)"
using add_group.group_oper_fun ij func_imagedef by auto
} hence "∀x∈A``(I × J). (\<rm> x) ∈ A``(I × J)" by auto
ultimately show ?thesis using add_group.group0_3_T3
by simp
qed
ultimately show "(A``(I × J)) ◃R" unfolding Ideal_def by auto
qed
text‹The set of all sums of elements of two ideals is their sum ideal i.e.
the ideal generated by their union. ›
corollary (in ring0) sum_ideals_is_sum_elements:
assumes "I ◃R" "J ◃R"
shows "(A``(I × J)) = I+⇩IJ"
proof
from assms have ij: "I⊆R" "J⊆R" using ideal_dest_subset
by auto
then have ij_prd: "I×J ⊆ R×R" by auto
with assms show "A``(I × J) ⊆ I +⇩I J"
using add_group.group_oper_fun sum_elements func_imagedef
by auto
{ fix x assume "x∈I"
with ij(1) have "x=x\<ra>𝟬" using Ring_ZF_1_L3(3) by auto
with assms(2) ij_prd ‹x∈I› have "x∈A `` (I × J)"
using add_group.group0_3_L5 add_group.group_oper_fun func_imagedef
unfolding Ideal_def by auto
} hence "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) by auto
with assms(1) ij_prd ‹x∈J› have "x ∈ A``(I × J)"
using add_group.group0_3_L5 add_group.group_oper_fun func_imagedef
unfolding Ideal_def by auto
} hence "J ⊆ A``(I × J)" by auto
ultimately have "I∪J ⊆ A``(I × J)" by auto
with assms show "I+⇩IJ ⊆ A``(I × J)"
using generated_ideal_small sum_elements_is_ideal sumIdeal_def
by auto
qed
text‹The sum ideal of two ideals is indeed an ideal.›
corollary (in ring0) sum_ideals_is_ideal:
assumes "I ◃R" "J ◃R"
shows "(I+⇩IJ) ◃R" using assms sum_ideals_is_sum_elements
sum_elements_is_ideal ideal_dest_subset by auto
text‹The operation of taking the sum of ideals is commutative.›
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
with assms show ?thesis using sumIdeal_def 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⋅⇩IJ ⊆ P ⟶ (I⊆P ∨ J⊆P))"
text‹Any maximal ideal is a prime ideal.›
theorem (in ring0) maximal_is_prime:
assumes "Q◃⇩mR" shows "Q◃⇩pR"
proof -
have "Q∈ℐ" using assms ideal_dest_subset
unfolding maximalIdeal_def by auto
{ fix I J assume "I∈ℐ" "J∈ℐ" "I⋅⇩IJ ⊆ Q"
{ assume K: "¬(I⊆Q)" "¬(J⊆Q)"
from ‹¬(I⊆Q)› obtain x where "x∈I-Q" by auto
with ‹I∈ℐ› have "x∈R" using ideal_dest_subset by auto
from ‹I∈ℐ› ‹J∈ℐ› have sub: "I×J ⊆ R×R" by auto
let ?K = "⟨Q∪{x}⟩⇩I"
from ‹Q∈ℐ› ‹x∈R› have "Q∪{x} ⊆ R" by auto
then have "Q⊆?K" and "x∈?K" using generated_ideal_contains_set
by auto
with ‹x∈I-Q› have "Q⊆?K" "?K≠Q" by auto
from ‹Q∪{x} ⊆ R› have "?K∈ℐ"
using ideal_dest_subset generated_ideal_is_ideal by blast
with assms ‹Q⊆?K› ‹?K≠Q› have "?K=R" unfolding maximalIdeal_def
by auto
let ?P = "Q+⇩II"
from ‹Q∈ℐ› ‹I∈ℐ› ‹x∈I-Q› have "Q∪{x} ⊆ Q+⇩II"
using comp_in_sum_ideals(3) by auto
with ‹Q∈ℐ› ‹I∈ℐ› have "?K ⊆ Q+⇩II" "Q+⇩II ⊆ R"
using sum_ideals_is_ideal generated_ideal_small ideal_dest_subset
by simp_all
with ‹?K=R› have "𝟭∈Q+⇩II " using Ring_ZF_1_L2(2) by auto
with ‹I∈ℐ› ‹Q∈ℐ› have "𝟭∈A``(Q×I)"
using sum_ideals_is_sum_elements by auto
moreover from ‹I∈ℐ› ‹Q∈ℐ› have "Q×I ⊆ R×R" by auto
ultimately obtain x⇩m x⇩i where "x⇩m∈Q" "x⇩i∈I" "𝟭=x⇩m\<ra>x⇩i"
using func_imagedef add_group.group_oper_fun by auto
{ fix y assume "y∈J"
with ‹x⇩m∈Q› ‹x⇩i∈I› ‹Q∈ℐ› ‹I∈ℐ› ‹J∈ℐ›
have "y∈R" "x⇩m∈R" "x⇩i∈R" by auto
with ‹y∈J› ‹J∈ℐ› ‹𝟭=x⇩m\<ra>x⇩i› have "(x⇩m⋅y)\<ra>(x⇩i⋅y) = y"
using Ring_ZF_1_L3(6) ring_oper_distr(2) by simp
from ‹Q∈ℐ› ‹x⇩m∈Q› ‹y∈R› have "x⇩m⋅y∈Q"
using ideal_dest_mult(1) by auto
from sub ‹y∈J› ‹x⇩i∈I› ‹I∈ℐ› ‹J∈ℐ› ‹I⋅⇩IJ⊆Q› have "x⇩i⋅y∈Q"
using func_imagedef mult_monoid.monoid_oper_fun
product_in_intersection(3) by force
with ‹Q∈ℐ› ‹(x⇩m⋅y)\<ra>(x⇩i⋅y) = y› ‹x⇩m⋅y∈Q› have "y∈Q"
using ideal_dest_sum by force
} hence "J ⊆ Q" by auto
with K have False by auto
} hence "(I⊆Q)∨(J⊆Q)" by auto
} hence "∀I∈ℐ. ∀J∈ℐ. I ⋅⇩I J ⊆ Q ⟶ (I ⊆ Q ∨ J ⊆ Q)" by auto
with assms show ?thesis 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 of that 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 -
{
fix I J assume ij: "I∈ℐ" "J∈ℐ" "I⋅⇩IJ ⊆ {𝟬}"
from ij(1,2) have "I×J ⊆ R×R" by auto
{ assume "¬(I⊆{𝟬})" "¬(J⊆{𝟬})"
then obtain x⇩i x⇩j where "x⇩i≠𝟬" "x⇩j≠𝟬" "x⇩i∈I" "x⇩j∈J"
by auto
from ij(1,2) ‹x⇩i∈I› ‹x⇩j∈J› have "x⇩i∈R" "x⇩j∈R" by auto
{ fix u assume "u∈R"
with ‹I∈ℐ› ‹x⇩i∈I› ‹x⇩j∈J› ‹I×J ⊆ R×R›
have "x⇩i⋅u⋅x⇩j ∈ M``(I×J)"
using ideal_dest_mult(1) func_imagedef
mult_monoid.monoid_oper_fun by auto
with ij have "x⇩i⋅u⋅x⇩j = 𝟬"
using product_in_intersection(3) by blast
} hence "∀u∈R. x⇩i⋅u⋅x⇩j = 𝟬" by simp
with ringAssum assms(1) ‹x⇩i∈R› ‹x⇩j∈R› ‹x⇩i≠𝟬› ‹x⇩j≠𝟬›
have False using primeRing_def by auto
} hence "I⊆{𝟬} ∨ J⊆{𝟬}" by auto
} hence "∀I∈ℐ. ∀J∈ℐ. I ⋅⇩I J ⊆ {𝟬} ⟶ (I ⊆ {𝟬} ∨ J ⊆ {𝟬})"
by auto
with assms(2) show ?thesis
using zero_ideal unfolding primeIdeal_def by blast
qed
text‹If the trivial ideal $\{ 0\}$ is a prime ideal then the ring is a prime ring.›
lemma (in ring0) zero_prime_ideal_prime_ring:
assumes "{𝟬}◃⇩pR"
shows "[R,A,M]{is a prime ring}"
proof -
{ fix x y z assume "x∈R" "y∈R" "∀z∈R. x⋅z⋅y = 𝟬"
let ?X = "⟨{x}⟩⇩I"
let ?Y = "⟨{y}⟩⇩I"
from ‹x∈R› ‹y∈R› have "?X×?Y ⊆ R×R"
using generated_ideal_is_ideal ideal_dest_subset
by auto
let ?P = "λq. (∀z∈?Y. q⋅z = 𝟬)"
let ?Q = "λq. (∀z∈R. x⋅z⋅q =𝟬)"
have "∀y∈?Y. ?Q(y)"
proof -
from ‹y∈R› have "{y}≠0" and "{y}⊆R" by auto
moreover
{ fix s t q assume yzq: "s∈R" "t∈R" "q ∈ ⟨{y}⟩⇩I" "∀k∈R. x⋅k⋅q = 𝟬"
from ‹y∈R› yzq(3) have "q∈R"
using generated_ideal_is_ideal ideal_dest_subset by auto
{ fix u assume "u∈R"
from yzq(1,2) ‹x∈R› ‹q∈R› ‹u∈R›
have "x⋅u⋅(s⋅q⋅t) = (x⋅(u⋅s)⋅q)⋅t"
using Ring_ZF_1_L11(2) Ring_ZF_1_L4(3) by auto
with ‹u∈R› yzq(1,2,4) have "x⋅u⋅(s⋅q⋅t) = 𝟬"
using Ring_ZF_1_L4(3) Ring_ZF_1_L6(1) by simp
} hence "∀z⇩a∈R. x⋅z⇩a⋅(s⋅q⋅t) = 𝟬" by simp
} hence "∀t∈R. ∀z∈R. ∀q∈⟨{y}⟩⇩I.
(∀z∈R. x⋅z⋅q = 𝟬) ⟶ (∀z⇩a∈R. x⋅z⇩a⋅(t⋅q⋅z) = 𝟬)" by simp
moreover from ‹x∈R› have "∀y∈R. ∀z∈R.
(∀z∈R. x⋅z⋅y = 𝟬) ∧ (∀z⇩a∈R. x⋅z⇩a⋅z = 𝟬) ⟶
(∀z⇩a∈R. x⋅z⇩a⋅(y\<ra>z) = 𝟬)"
using ring_oper_distr(1) Ring_ZF_1_L4(3) Ring_ZF_1_L3(3)
Ring_ZF_1_L2(1) by simp
moreover from ‹∀z∈R. x⋅z⋅y = 𝟬› have "∀x⇩a∈{y}. ∀z∈R. x⋅z⋅x⇩a = 𝟬" by simp
ultimately show ?thesis by (rule induction_generated_ideal)
qed
from ‹x∈R› ‹∀y∈?Y. ?Q(y)› have "∀y∈?Y. x⋅y = 𝟬"
using Ring_ZF_1_L2(2) Ring_ZF_1_L3(5) by force
from ‹y∈R› have "?Y◃R" "?Y⊆R"
using generated_ideal_is_ideal ideal_dest_subset by auto
have "∀y∈?X. ?P(y)"
proof -
from ‹x∈R› have "{x}≠0" "{x}⊆R" by auto
moreover
{ fix q⇩1 q⇩2 q⇩3
assume q: "q⇩1∈R" "q⇩2∈R" "q⇩3 ∈ ⟨{x}⟩⇩I" "∀k∈?Y. q⇩3⋅k = 𝟬"
from ‹x∈R› ‹q⇩3 ∈ ⟨{x}⟩⇩I› have "q⇩3∈R"
using generated_ideal_is_ideal ideal_dest_subset by auto
with ‹?Y◃R› ‹?Y⊆R› q(1,2,4) have "∀z⇩a∈⟨{y}⟩⇩I. q⇩1⋅q⇩3⋅q⇩2 ⋅ z⇩a = 𝟬"
using ideal_dest_mult(2) Ring_ZF_1_L4(3) Ring_ZF_1_L11(2)
Ring_ZF_1_L6(2) by auto
} hence "∀y⇩a∈R. ∀z∈R. ∀q∈⟨{x}⟩⇩I.
(∀z∈⟨{y}⟩⇩I. q⋅z = 𝟬) ⟶ (∀z⇩a∈⟨{y}⟩⇩I. y⇩a⋅q⋅z⋅z⇩a = 𝟬)"
by auto
moreover from ‹?Y⊆R› have "∀y⇩a∈R. ∀z∈R.
(∀z∈⟨{y}⟩⇩I. y⇩a⋅z = 𝟬) ∧ (∀z⇩a∈⟨{y}⟩⇩I. z⋅z⇩a = 𝟬) ⟶
(∀z⇩a∈⟨{y}⟩⇩I. (y⇩a\<ra>z)⋅z⇩a = 𝟬)"
using ring_oper_distr(2) Ring_ZF_1_L3(3) Ring_ZF_1_L2(1)
by auto
moreover from ‹∀y∈?Y. x⋅y = 𝟬› have "∀x∈{x}. ∀z∈⟨{y}⟩⇩I. x⋅z = 𝟬" by auto
ultimately show ?thesis by (rule induction_generated_ideal)
qed
from ‹?X×?Y ⊆ R×R› ‹∀y∈?X. ?P(y)› have "M``(?X×?Y) ⊆ {𝟬}"
using mult_monoid.monoid_oper_fun func_imagedef by auto
with ‹x∈R› ‹y∈R› have "?X⋅⇩I?Y ⊆ {𝟬}"
using generated_ideal_small zero_ideal productIdeal_def
generated_ideal_is_ideal by auto
with assms ‹x∈R› ‹y∈R› have "?X ⊆ {𝟬} ∨ ?Y ⊆ {𝟬}"
using generated_ideal_is_ideal ideal_dest_subset
unfolding primeIdeal_def by auto
with ‹x∈R› ‹y∈R› have "x=𝟬 ∨ y=𝟬"
using generated_ideal_contains_set by auto
} hence "∀x∈R. ∀y∈R. (∀z∈R. x⋅z⋅y = 𝟬) ⟶ x=𝟬 ∨ y=𝟬"
by auto
with ringAssum show ?thesis using primeRing_def 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 -
{ fix x y assume "x∈R" "y∈R" "∀z∈R. x⋅z⋅y∈P" "y∉P"
let ?X = "⟨{x}⟩⇩I"
let ?Y = "⟨{y}⟩⇩I"
from ‹y∈R› have "{y}≠0" and "{y}⊆R" by auto
moreover have "∀y⇩a∈R.
∀z∈R. ∀q∈⟨{y}⟩⇩I. (∀t∈⟨{x}⟩⇩I. ∀u∈R. t⋅u⋅q ∈ P) ⟶
(∀t∈⟨{x}⟩⇩I. ∀u∈R. t⋅u⋅(y⇩a⋅q⋅z) ∈ P)"
proof -
{ fix y⇩a z q t u
assume "y⇩a∈R" "z∈R" "q∈?Y" "∀t∈?X. ∀u∈R. t⋅u⋅q∈P" "t∈?X" "u∈R"
from ‹x∈R› ‹y∈R› ‹q∈?Y› ‹t∈?X› have "q∈R" "t∈R"
using generated_ideal_is_ideal ideal_dest_subset by auto
from ‹y⇩a∈R› ‹u∈R› have "u⋅y⇩a∈R" using Ring_ZF_1_L4(3) by auto
with assms ‹z∈R› ‹∀t∈?X. ∀u∈R. t⋅u⋅q∈P› ‹t∈?X›
have "(t⋅(u⋅y⇩a)⋅q)⋅z ∈ P"
using ideal_dest_mult(1) unfolding primeIdeal_def by auto
with ‹y⇩a∈R› ‹z∈R› ‹u∈R› ‹q∈R› ‹t∈R› have "t⋅u⋅(y⇩a⋅q⋅z) ∈ P"
using Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) by auto
} thus ?thesis by simp
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 -
{ fix y⇩a z t u assume ass: "y⇩a∈R" "z∈R" "t∈?X" "u∈R"
"∀t∈⟨{x}⟩⇩I. ∀u∈R. t⋅u⋅y⇩a∈P" "∀t∈⟨{x}⟩⇩I. ∀u∈R. t⋅u⋅z∈P"
from ‹x∈R› ‹t∈?X› have "t∈R"
using ideal_dest_subset generated_ideal_is_ideal by auto
from assms ass(3,4,5,6) have "(t⋅u⋅y⇩a)\<ra>(t⋅u⋅z) ∈ P"
using ideal_dest_sum unfolding primeIdeal_def by simp
with ‹t∈R› ‹y⇩a∈R› ‹z∈R› ‹u∈R› have "t⋅u⋅(y⇩a\<ra>z) ∈ P"
using Ring_ZF_1_L4(3) ring_oper_distr(1) by simp
} thus ?thesis by simp
qed
moreover have "∀y⇩a∈⟨{x}⟩⇩I. ∀u∈R. y⇩a⋅u⋅y ∈ P"
proof -
from ‹x∈R› have "{x}≠0" and "{x}⊆R" by auto
moreover have "∀y⇩a∈R. ∀z∈R. ∀q∈?X.
(∀u∈R. q⋅u⋅y ∈ P) ⟶ (∀u∈R. y⇩a⋅q⋅z⋅u⋅y ∈ P)"
proof -
{ fix y⇩a z q u assume
ass: "y⇩a∈R" "z∈R" "q∈?X" "∀u∈R. q⋅u⋅y ∈ P" "u ∈ R"
from ‹x∈R› ‹q∈?X› have q: "q∈R"
using generated_ideal_is_ideal ideal_dest_subset
by auto
from assms ass(1,2,4,5) have "y⇩a⋅(q⋅(z⋅u)⋅y) ∈ P"
using Ring_ZF_1_L4(3) ideal_dest_mult(2)
unfolding primeIdeal_def by simp
with ‹y∈R› ‹y⇩a∈R› ‹z∈R› ‹u ∈ R› ‹q∈R›
have "y⇩a⋅q⋅z⋅u⋅y ∈ P"
using Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) by auto
} thus ?thesis by auto
qed
moreover have "∀y⇩a∈R. ∀z∈R.
(∀u∈R. y⇩a⋅u⋅y ∈ P) ∧ (∀u∈R. z⋅u⋅y ∈ P) ⟶ (∀u∈R. (y⇩a\<ra>z)⋅u⋅y ∈ P)"
proof -
{ fix y⇩a z u assume "y⇩a∈R" "z∈R" "u∈R"
"∀u∈R. y⇩a⋅u⋅y ∈ P" "∀u∈R. z⋅u⋅y ∈ P"
with assms ‹y∈R› have "((y⇩a\<ra>z)⋅u)⋅y∈P"
using ideal_dest_sum ring_oper_distr(2) Ring_ZF_1_L4(3)
unfolding primeIdeal_def by simp
} thus ?thesis by simp
qed
moreover from ‹∀z∈R. x⋅z⋅y∈P› have "∀x∈{x}. ∀u∈R. x⋅u⋅y ∈ P"
by simp
ultimately show ?thesis by (rule induction_generated_ideal)
qed
hence "∀x⇩a∈{y}. ∀t∈⟨{x}⟩⇩I. ∀u∈R. t⋅u⋅x⇩a ∈ P" by auto
ultimately have R: "∀q∈?Y. ∀t∈?X. ∀u∈R. t⋅u⋅q ∈ P"
by (rule induction_generated_ideal)
from ‹x∈R› ‹y∈R› have subprd: "?X×?Y ⊆ R×R"
using ideal_dest_subset generated_ideal_is_ideal by auto
{ fix t assume "t ∈ M``(?X×?Y)"
with subprd obtain t⇩x t⇩y where
"t⇩x∈?X" "t⇩y∈?Y" and t: "t= t⇩x⋅t⇩y"
using func_imagedef mult_monoid.monoid_oper_fun
by auto
with R ‹t⇩x∈?X› ‹t⇩y∈?Y› have "t⇩x⋅𝟭⋅t⇩y ∈P"
using Ring_ZF_1_L2(2) by auto
moreover from ‹x∈R› ‹t⇩x∈?X› have "t⇩x∈R"
using generated_ideal_is_ideal ideal_dest_subset by auto
ultimately have "t∈P" using Ring_ZF_1_L3(5) t by auto
} hence "M``(?X×?Y) ⊆ P" by auto
with assms ‹x∈R› ‹y∈R› have "?X ⊆ P ∨ ?Y ⊆ P"
unfolding primeIdeal_def
using generated_ideal_small productIdeal_def
generated_ideal_is_ideal ideal_dest_subset by auto
with ‹x∈R› ‹y∈R› ‹y∉P› have "x∈P" using generated_ideal_contains_set
by auto
} thus ?thesis by auto
qed
text‹The next theorem provides a sufficient condition for a proper ideal $P$ to be a prime ideal:
if for all $x,y\in R$ it holds that for all $z\in R$ $x z y \in P$ only when $x\in P$ or $y\in P$
then $P$ is a prime ideal. ›
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"
proof -
{ fix I J x x⇩a
assume "I◃R" "I⊆R" "J◃R" "J⊆R" "I⋅⇩IJ ⊆ P" "x∈J" "x∉P" "x⇩a∈I"
from ‹I⊆R› ‹J⊆R› have "I×J ⊆ R×R" by auto
{ fix z assume "z∈R"
with ‹I◃R› ‹x∈J› ‹x⇩a∈I› ‹I×J ⊆ R×R› have "(x⇩a⋅z⋅x)∈M``(I×J)"
using ideal_dest_mult(1) func_imagedef mult_monoid.monoid_oper_fun
by auto
with ‹I◃R› ‹J◃R› ‹I⋅⇩IJ ⊆ P› have "x⇩a⋅z⋅x ∈ P"
using generated_ideal_contains_set func1_1_L6(2)
mult_monoid.monoid_oper_fun productIdeal_def by force
} with assms(1) ‹I⊆R› ‹J⊆R› ‹x∈J› ‹x∉P› ‹x⇩a∈I› have "x⇩a∈P"
by blast
} with assms(2,3) show ?thesis unfolding primeIdeal_def
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 ringAssum assms Group_ZF_2_4_L6(1)
unfolding IsAring_def Ideal_def by auto
text‹ Each ring $R$ is a group with respect to its addition operation.
By the lemma ‹ideal_normal_add_subgroup› above an ideal $I\subseteq R$ is a normal subgroup of that group.
Therefore we can define the quotient of the ring $R$ by the ideal $I$ using
the notion of quotient of a group by its normal subgroup, see section
‹Normal subgroups and quotient groups› in ‹Group_ZF_2› theory. ›
definition (in ring0) QuotientBy where
"I◃R ⟹ QuotientBy(I) ≡ R//QuotientGroupRel(R,A,I)"
text‹Any ideal gives rise to an equivalence relation›
corollary (in ring0) ideal_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)"
using assms ringAssum ideal_normal_add_subgroup Group_ZF_2_4_T1
Group_ZF_2_4_L6(2) QuotientBy_def QuotientBy_def Ideal_def
unfolding IsAring_def by auto
text‹ Since every ideal is a normal subgroup of the additive group
of the ring it is quite obvious that that addition is congruent with respect
to the quotient group relation. The next lemma shows something a little bit less obvious:
that the multiplicative ring operation is also 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 -
let ?r = "QuotientGroupRel(R,A,I)"
{ fix x y s t assume "⟨x,y⟩ ∈ ?r" and "⟨s,t⟩ ∈ ?r"
then have xyst: "x∈R" "y∈R" "s∈R" "t∈R" "x\<rs>y ∈I" "s\<rs>t ∈I"
unfolding QuotientGroupRel_def by auto
from ‹x∈R› ‹y∈R› ‹s∈R› have
"(x⋅s)\<rs>(y⋅t) = ((x⋅s)\<ra>((\<rm>(y⋅s))\<ra>(y⋅s)))\<rs>(y⋅t)"
using Ring_ZF_1_L3(1,3,7) Ring_ZF_1_L4(3,4) by simp
with ‹x∈R› ‹y∈R› ‹s∈R› ‹t∈R› 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,3) Ring_ZF_1_L10(1)
by simp
with ‹x∈R› ‹y∈R› ‹s∈R› ‹t∈R› have
"(x⋅s)\<rs>(y⋅t) = ((x\<rs>y)⋅s)\<ra>(y⋅(s\<rs>t))"
using Ring_ZF_1_L8 by simp
with assms xyst have "⟨M`⟨x,s⟩,M`⟨y,t⟩⟩ ∈ ?r"
using ideal_dest_sum ideal_dest_mult(1,2) Ring_ZF_1_L4(3)
unfolding QuotientGroupRel_def by auto
} then show "Congruent2(?r,M)" unfolding Congruent2_def by simp
with assms show "IsAmonoid(QuotientBy(I),ProjFun2(R,?r, M))"
using add_group.Group_ZF_2_4_L3 mult_monoid.Group_ZF_2_2_T1 QuotientBy_def
unfolding Ideal_def by auto
qed
text‹Each ideal defines an equivalence relation on the ring with which both addition and
multiplication are congruent. The next couple of definitions set up notation
for the operations that result from projecting the ring addition and multiplication
on the quotient space.
We will write $x+_I y $ to denote the result of the quotient
operation (with respect to an ideal I) on classes $x$ and $y$ ›
definition (in ring0) ideal_radd ("_{\<ra>_}_") where
"x{\<ra>I}y ≡ QuotientGroupOp(R, A, I)`⟨x,y⟩"
text‹Similarly $x \cdot_I y$ is the value of the projection of the ring's multiplication
on the quotient space defined by the an ideal $I$, which as we know
is a normal subgroup of the ring with addition. ›
definition (in ring0) ideal_rmult ("_{⋅_}_") where
"x{⋅I}y ≡ ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,y⟩"
text‹The value of the projection of taking the negative in the ring on the quotient space
defined by an ideal $I$ will be denoted ‹{\<rm>I}›. ›
definition (in ring0) ideal_rmin ("{\<rm>_}_") where
"{\<rm>I}y ≡ GroupInv(QuotientBy(I),QuotientGroupOp(R, A, I))`(y)"
text‹Subtraction in the quotient space is defined by the ‹\<ra>I› and ‹\<rm>I› operations in
the obvious way. ›
definition (in ring0) ideal_rsub ("_{\<rs>_}_") where
"x{\<rs>I}y ≡ x{\<ra>I}({\<rm>I}y)"
text‹The class of the zero of the ring with respect to the equivalence relation
defined by an ideal $I$ will be denoted $0_I$.›
definition (in ring0) ideal_rzero ("𝟬⇩_") where
"𝟬⇩I ≡ QuotientGroupRel(R,A,I)``{𝟬}"
text‹Similarly the class of the neutral element of multiplication in the ring
with respect to the equivalence relation defined by an ideal $I$ will be denoted $1_I$.›
definition (in ring0) ideal_rone ("𝟭⇩_") where
"𝟭⇩I ≡ QuotientGroupRel(R,A,I)``{𝟭}"
text‹The class of the sum of two units of the ring will be denoted $2_I$.›
definition (in ring0) ideal_rtwo ("𝟮⇩_") where
"𝟮⇩I ≡ QuotientGroupRel(R,A,I)``{𝟮}"
text‹The value of the projection of the ring multiplication onto the the quotient space
defined by an ideal $I$ on a pair of the same classes $\langle x,x\rangle$ is denoted $x^{2I}$. ›
definition (in ring0) ideal_rsqr ("_⇧2⇧_") where
"x⇧2⇧I ≡ ProjFun2(R, QuotientGroupRel(R,A,I), M)`⟨x,x⟩"
text‹The class of the additive neutral element of the ring (i.e. $0$) with respect to the
equivalence relation defined by an ideal is the neutral of the projected addition. ›
lemma (in ring0) neutral_quotient:
assumes "I◃R"
shows
"QuotientGroupRel(R,A,I)``{𝟬} = TheNeutralElement(QuotientBy(I),QuotientGroupOp(R,A,I))"
using ringAssum assms Group_ZF_2_4_L5B ideal_normal_add_subgroup QuotientBy_def
unfolding IsAring_def by auto
text‹Similarly, the class of the multiplicative neutral element of the ring (i.e. $1$)
with respect to the equivalence relation defined by an ideal is the neutral of the projected
multiplication. ›
lemma (in ring0) one_quotient:
assumes "I◃R"
defines "r ≡ QuotientGroupRel(R,A,I)"
shows "r``{𝟭} = TheNeutralElement(QuotientBy(I),ProjFun2(R,r,M))"
using ringAssum assms Group_ZF_2_2_L1 ideal_equiv_rel quotientBy_mul_monoid QuotientBy_def
unfolding IsAring_def by auto
text‹The class of $2$ (i.e. $1+1$) is the same as the value of the addition projected on the
quotient space on the pair of classes of $1$. ›
lemma (in ring0) two_quotient:
assumes "I◃R"
defines "r ≡ QuotientGroupRel(R,A,I)"
shows "r``{𝟮} = QuotientGroupOp(R,A,I)`⟨r``{𝟭},r``{𝟭}⟩"
using ringAssum assms EquivClass_1_L10 ideal_equiv_rel Ring_ZF_1_L2(2) Ring_ZF_1_L2(2)
Group_ZF_2_4_L5A ideal_normal_add_subgroup
unfolding IsAring_def QuotientGroupOp_def by simp
text‹The class of a square of an element of the ring is the same as the result of the
projected multiplication on the pair of classes of the element. ›
lemma (in ring0) sqrt_quotient:
assumes "I◃R" "x∈R"
defines "r ≡ QuotientGroupRel(R,A,I)"
shows "r``{x⇧2} = ProjFun2(R,r, M)`⟨r``{x},r``{x}⟩"
using assms EquivClass_1_L10 ideal_equiv_rel quotientBy_mul_monoid(1)
by auto
text‹The projection of the ring addition is distributive with respect
to the projection of the ring multiplication. ›
lemma (in ring0) quotientBy_distributive:
assumes "I◃R"
defines "r ≡ QuotientGroupRel(R,A,I)"
shows
"IsDistributive(QuotientBy(I),QuotientGroupOp(R,A,I),ProjFun2(R,r,M))"
using ringAssum assms QuotientBy_def ring_oper_distr(1) Ring_ZF_1_L4(1,3)
quotientBy_mul_monoid(1) EquivClass_1_L10 ideal_equiv_rel Group_ZF_2_4_L5A
ideal_normal_add_subgroup ring_oper_distr(2)
unfolding quotient_def QuotientGroupOp_def IsAring_def IsDistributive_def
by auto
text‹The quotient group is a ring with the quotient multiplication.›
theorem (in ring0) quotientBy_is_ring:
assumes "I◃R"
defines "r ≡ QuotientGroupRel(R,A,I)"
shows "IsAring(QuotientBy(I), QuotientGroupOp(R, A, I), ProjFun2(R,r, M))"
using assms quotientBy_distributive quotientBy_mul_monoid(2) quotientBy_add_group
unfolding IsAring_def by auto
text‹An important 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 -
from assms(2) have "⋃𝒥 ⊆ R" using ideal_dest_subset by auto
then have "⟨⋃𝒥⟩⇩I ◃R" using generated_ideal_is_ideal by simp
with assms(2) have "(⊕⇩I𝒥) ◃R" using sumArbitraryIdeals_def
by simp
with assms(1) have "(⊕⇩I𝒥) {is finitely generated}"
using ideal_dest_subset by auto
with ‹(⊕⇩I𝒥)◃R› obtain S where "S∈FinPow(R)" "(⊕⇩I𝒥) = ⟨S⟩⇩I"
using isFinGen_def by auto
let ?N = "λs∈S. {J∈FinPow(𝒥). s∈(⊕⇩IJ)}"
from ‹S∈FinPow(R)› have "Finite(S)" unfolding FinPow_def
by auto
then have "(∀t∈S. ?N`(t) ≠ 0) ⟶
(∃f. f ∈ (∏t∈S. ?N`(t)) ∧ (∀t∈S. f`(t) ∈ ?N`(t)))"
using eqpoll_iff finite_choice AxiomCardinalChoiceGen_def
unfolding Finite_def by blast
moreover
{ fix t assume "t∈S"
then have "?N`(t) = {J∈FinPow(𝒥). t∈(⊕⇩IJ)}" using lamE by auto
moreover
from ‹S∈FinPow(R)› ‹(⊕⇩I𝒥) = ⟨S⟩⇩I› ‹t∈S› have "t∈(⊕⇩I𝒥)"
using generated_ideal_contains_set unfolding FinPow_def by auto
with assms(2) have "∃𝒯∈FinPow(𝒥). t∈(⊕⇩I𝒯)"
using sum_ideals_finite_sum by simp
ultimately have "?N`(t)≠0" using assms(2) sum_ideals_finite_sum
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∈S" and "⟨x,y⟩ ∈ f" by auto
with f(1) have "y∈?N`(x)" unfolding Pi_def by auto
with ‹x∈S› have "Finite(y)" using lamE unfolding FinPow_def
by simp
}
moreover
from f(1) have f_Fun: "f:S→ (⋃{?N`(t). t∈S})"
unfolding Pi_def Sigma_def by blast
with ‹Finite(S)› have "Finite(f``(S))"
using Finite1_L6A Finite_Fin_iff Fin_into_Finite by blast
ultimately have "Finite(⋃(f``(S)))" using Finite_Union
by auto
with f_Fun f(2) have B: "(⋃(f``(S))) ∈ FinPow(𝒥)"
using func_imagedef lamE unfolding FinPow_def
by auto
then have "(⋃(f``(S))) ⊆ 𝒥" unfolding FinPow_def by auto
with assms(2) have "(⋃(f``(S))) ⊆ ℐ" by auto
hence sub: "⋃(⋃(f``(S))) ⊆ R" by auto
{ fix t assume "t∈S"
with f(2) have "f`(t) ∈ FinPow(𝒥)" "t ∈ (⊕⇩I(f`(t)))"
using lamE by auto
from assms(2) ‹f`(t) ∈ FinPow(𝒥)› have "f`(t) ⊆ ℐ"
unfolding FinPow_def by auto
from f_Fun ‹t∈S› have "⋃(f`t) ⊆ ⋃(⋃(f``S))" using func_imagedef
by auto
with sub have "⋃(f`(t)) ⊆ ⟨⋃(⋃(f``(S)))⟩⇩I"
using generated_ideal_contains_set by blast
with sub have "⟨⋃(f`t)⟩⇩I ⊆ ⟨⋃(⋃(f``S))⟩⇩I"
using generated_ideal_is_ideal generated_ideal_small by auto
with ‹f`(t) ⊆ ℐ› ‹t ∈ (⊕⇩I(f`(t)))› ‹(⋃(f``(S))) ⊆ ℐ›
have "t ∈ (⊕⇩I(⋃(f``(S))))"
using sumArbitraryIdeals_def by auto
} hence "S ⊆ ⊕⇩I(⋃(f``(S)))" by auto
with sub ‹(⋃(f``(S))) ⊆ ℐ› ‹(⊕⇩I𝒥) = ⟨S⟩⇩I› have "(⊕⇩I𝒥) ⊆ ⊕⇩I(⋃(f``(S)))"
using generated_ideal_small generated_ideal_is_ideal sumArbitraryIdeals_def
by auto
moreover
from ‹⋃𝒥 ⊆ R› ‹(⋃(f``(S))) ⊆ 𝒥› have "⋃(⋃(f``(S))) ⊆ ⟨⋃𝒥⟩⇩I"
using generated_ideal_contains_set by blast
with assms(2) ‹(⋃(f``(S))) ⊆ ℐ› ‹⟨⋃𝒥⟩⇩I ◃R› have "(⊕⇩I(⋃(f``(S)))) ⊆(⊕⇩I𝒥)"
using generated_ideal_small sumArbitraryIdeals_def sumArbitraryIdeals_def
by simp
ultimately have "(⊕⇩I𝒥) = ⊕⇩I(⋃(f``(S)))" by auto
with B show ?thesis by auto
qed
end