(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2022 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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 ("_◃⇩_{m}R") where "I◃⇩_{m}R ≡ 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⋅⇩_{I}J ≡ ⟨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+⇩_{I}J ≡ ⟨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+⇩_{I}J" and "J ⊆ I+⇩_{I}J" and "I∪J ⊆ I+⇩_{I}J" proof - from assms have "I∪J ⊆ R" using ideal_dest_subset by auto with assms show "I ⊆ I+⇩_{I}J" "J ⊆ I+⇩_{I}J" "I∪J ⊆ I+⇩_{I}J" 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 ∈ ⊕⇩_{I}T⇩_{y}" "T⇩_{z}∈FinPow(𝒥)" "z ∈ ⊕⇩_{I}T⇩_{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⋅⇩_{I}J ⊆ I∩J" and "(I⋅⇩_{I}J)◃R" and "M``(I×J) ⊆ I⋅⇩_{I}J" 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⋅⇩_{I}J ⊆ 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⋅⇩_{I}J) ◃R" and "M``(I×J) ⊆ I⋅⇩_{I}J" 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+⇩_{I}J" 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+⇩_{I}J" 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+⇩_{I}J ⊆ 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+⇩_{I}J) ◃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 ("_◃⇩_{p}R") where "P◃⇩_{p}R ≡ P◃R ∧ P≠R ∧ (∀I∈ℐ. ∀J∈ℐ. I⋅⇩_{I}J ⊆ P ⟶ (I⊆P ∨ J⊆P))" text‹Any maximal ideal is a prime ideal.› theorem (in ring0) maximal_is_prime: assumes "Q◃⇩_{m}R" shows "Q◃⇩_{p}R" proof - have "Q∈ℐ" using assms ideal_dest_subset unfolding maximalIdeal_def by auto { fix I J assume "I∈ℐ" "J∈ℐ" "I⋅⇩_{I}J ⊆ 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+⇩_{I}I" from ‹Q∈ℐ› ‹I∈ℐ› ‹x∈I-Q› have "Q∪{x} ⊆ Q+⇩_{I}I" using comp_in_sum_ideals(3) by auto with ‹Q∈ℐ› ‹I∈ℐ› have "?K ⊆ Q+⇩_{I}I" "Q+⇩_{I}I ⊆ R" using sum_ideals_is_ideal generated_ideal_small ideal_dest_subset by simp_all with ‹?K=R› have "𝟭∈Q+⇩_{I}I " 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⋅⇩_{I}J⊆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 "{𝟬} ◃⇩_{p}R" proof - { fix I J assume ij: "I∈ℐ" "J∈ℐ" "I⋅⇩_{I}J ⊆ {𝟬}" 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 "{𝟬}◃⇩_{p}R" 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◃⇩_{p}R" 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◃⇩_{p}R" proof - { fix I J x x⇩_{a}assume "I◃R" "I⊆R" "J◃R" "J⊆R" "I⋅⇩_{I}J ⊆ 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⋅⇩_{I}J ⊆ 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∈(⊕⇩_{I}J)}" 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∈(⊕⇩_{I}J)}" 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