Theory Ring_ZF_2

(*
    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‹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 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
      with assms(1) have "⋃Ty ⊆ ⋃(Ty∪Tz)" "⋃Tz ⊆ ⋃(Ty∪Tz)" and 
        sub: "⋃(Ty∪Tz) ⊆ R"
        unfolding FinPow_def by auto
      then have "⋃(Ty∪Tz) ⊆ ⟨⋃(Ty∪Tz)⟩I" 
        using generated_ideal_contains_set by simp
      hence "⋃Ty ⊆ ⟨⋃(Ty∪Tz)⟩I" "⋃Tz ⊆ ⟨⋃(Ty∪Tz)⟩I" by auto
      with sub have "⟨⋃Ty⟩I⊆ ⟨⋃(Ty∪Tz)⟩I" "⟨⋃Tz⟩I ⊆ ⟨⋃(Ty∪Tz)⟩I"
        using generated_ideal_small generated_ideal_is_ideal
        by auto
      moreover from assms(1) T(1,3) have "Ty⊆ℐ" "Tz⊆ℐ" 
        unfolding FinPow_def by auto
      moreover note T(2,4)
      ultimately have "y ∈ ⟨⋃(Ty∪Tz)⟩I" "z ∈ ⟨⋃(Ty∪Tz)⟩I"
        using sumArbitraryIdeals_def sumArbitraryIdeals_def 
        by auto
      with ‹⋃(Ty∪Tz) ⊆ R› have "y\<ra>z ∈ ⟨⋃(Ty∪Tz)⟩I" 
        using generated_ideal_is_ideal ideal_dest_sum by auto
      moreover
      from ‹Ty⊆ℐ› ‹Tz⊆ℐ› have "Ty∪Tz ⊆ ℐ" by auto
      then have "(⊕I(Ty∪Tz)) = ⟨⋃(Ty∪Tz)⟩I" 
        using sumArbitraryIdeals_def by auto
      ultimately have "y\<ra>z ∈ (⊕I(Ty∪Tz))" 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 yi yj where y: "yi∈I" "yj∈J" "⟨⟨yi,yj⟩,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 yi yj where 
      y: "y=yi\<ra>yj" "yi∈I" "yj∈J"
      using add_group.group_oper_fun func_imagedef by auto
    from ‹x∈R› y ij have 
      "x⋅y = (x⋅yi)\<ra>(x⋅yj)" and "y⋅x = (yi⋅x)\<ra>(yj⋅x)"
      using ring_oper_distr add_group.group_op_closed by auto
    moreover from assms ‹x∈R› y(2,3) have 
      "x⋅yi ∈ I" "yi⋅x ∈ I" "x⋅yj ∈ J" "yj⋅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 xi xj yi yj where 
        "xi∈I" "xj∈J" "x=xi\<ra>xj" "yi∈I" "yj∈J" "y=yi\<ra>yj"
        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 ‹xi∈I› ‹xj∈J› ‹yi∈I› ‹yj∈J› 
        have "xi∈R" "xj∈R" "yi∈R" "yj∈R" 
          using ideal_dest_subset by auto
      from ij ‹x∈R› ‹yi∈R› ‹yj∈R› ‹y=yi\<ra>yj› 
        have "x\<ra>y = (x\<ra>yi)\<ra>yj" 
        using Ring_ZF_1_L10(1) by simp
      with ‹x=xi\<ra>xj› ‹xi∈R› ‹xj∈R› ‹yi∈R› ‹yj∈R› 
        have "x\<ra>y = (xi\<ra>yi)\<ra>(xj\<ra>yj)"
        using Ring_ZF_2_L5(4) by simp
      moreover from assms ‹xi∈I› ‹xj∈J› ‹yi∈I› ‹yj∈J›
        have "xi\<ra>yi ∈ I" and "xj\<ra>yj ∈ 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 xi xj where "xi∈I" "xj∈J" "x=xi\<ra>xj" 
        using add_group.group_oper_fun func_imagedef by auto
      with assms have "(\<rm>x) = (\<rm>xi)\<rs>xj" 
        using Ring_ZF_1_L9(2) ideal_dest_subset by auto
      moreover from assms ‹xi∈I› ‹xj∈J› 
      have "(\<rm>xi)∈I" and "(\<rm>xj)∈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 xm xi where "xm∈Q" "xi∈I" "𝟭=xm\<ra>xi"
        using func_imagedef add_group.group_oper_fun by auto
      { fix y assume "y∈J"
        with ‹xm∈Q› ‹xi∈I› ‹Q∈ℐ› ‹I∈ℐ› ‹J∈ℐ› 
        have "y∈R" "xm∈R" "xi∈R" by auto
        with ‹y∈J› ‹J∈ℐ› ‹𝟭=xm\<ra>xi› have "(xm⋅y)\<ra>(xi⋅y) = y"
          using Ring_ZF_1_L3(6) ring_oper_distr(2) by simp
        from ‹Q∈ℐ› ‹xm∈Q›  ‹y∈R› have "xm⋅y∈Q" 
          using ideal_dest_mult(1) by auto
        from sub ‹y∈J› ‹xi∈I› ‹I∈ℐ› ‹J∈ℐ› ‹I⋅IJ⊆Q› have "xi⋅y∈Q"  
          using func_imagedef mult_monoid.monoid_oper_fun 
            product_in_intersection(3) by force
        with ‹Q∈ℐ› ‹(xm⋅y)\<ra>(xi⋅y) = y› ‹xm⋅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 xi xj where "xi≠𝟬" "xj≠𝟬" "xi∈I" "xj∈J" 
        by auto
      from ij(1,2) ‹xi∈I› ‹xj∈J› have "xi∈R" "xj∈R" by auto
      { fix u assume "u∈R"
        with ‹I∈ℐ› ‹xi∈I› ‹xj∈J› ‹I×J ⊆ R×R›
          have "xi⋅u⋅xj ∈ M``(I×J)"
          using ideal_dest_mult(1) func_imagedef 
            mult_monoid.monoid_oper_fun by auto
        with ij have "xi⋅u⋅xj = 𝟬"
          using product_in_intersection(3) by blast
      } hence "∀u∈R. xi⋅u⋅xj = 𝟬" by simp
      with ringAssum assms(1) ‹xi∈R› ‹xj∈R› ‹xi≠𝟬› ‹xj≠𝟬› 
        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 "∀za∈R. x⋅za⋅(s⋅q⋅t) = 𝟬" by simp
      } hence "∀t∈R. ∀z∈R. ∀q∈⟨{y}⟩I. 
        (∀z∈R. x⋅z⋅q = 𝟬) ⟶ (∀za∈R. x⋅za⋅(t⋅q⋅z) = 𝟬)" by simp
      moreover from ‹x∈R› have "∀y∈R. ∀z∈R. 
             (∀z∈R. x⋅z⋅y = 𝟬) ∧ (∀za∈R. x⋅za⋅z = 𝟬) ⟶
             (∀za∈R. x⋅za⋅(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 "∀xa∈{y}. ∀z∈R. x⋅z⋅xa = 𝟬" 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 q1 q2 q3
        assume q: "q1∈R" "q2∈R" "q3 ∈ ⟨{x}⟩I" "∀k∈?Y. q3⋅k = 𝟬"
        from ‹x∈R› ‹q3 ∈ ⟨{x}⟩I› have "q3∈R" 
          using generated_ideal_is_ideal ideal_dest_subset by auto
        with ‹?Y◃R› ‹?Y⊆R› q(1,2,4) have "∀za∈⟨{y}⟩I. q1⋅q3⋅q2 ⋅ za = 𝟬"
          using ideal_dest_mult(2) Ring_ZF_1_L4(3) Ring_ZF_1_L11(2) 
            Ring_ZF_1_L6(2) by auto
      } hence "∀ya∈R. ∀z∈R. ∀q∈⟨{x}⟩I. 
              (∀z∈⟨{y}⟩I. q⋅z = 𝟬) ⟶ (∀za∈⟨{y}⟩I. ya⋅q⋅z⋅za = 𝟬)" 
        by auto
      moreover from ‹?Y⊆R› have "∀ya∈R. ∀z∈R. 
        (∀z∈⟨{y}⟩I. ya⋅z = 𝟬) ∧ (∀za∈⟨{y}⟩I. z⋅za = 𝟬) ⟶
          (∀za∈⟨{y}⟩I. (ya\<ra>z)⋅za = 𝟬)"
        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 "∀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 -
      { fix ya z q t u 
        assume "ya∈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 ‹ya∈R› ‹u∈R› have "u⋅ya∈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⋅ya)⋅q)⋅z ∈ P"
          using ideal_dest_mult(1) unfolding primeIdeal_def by auto
        with ‹ya∈R› ‹z∈R› ‹u∈R› ‹q∈R› ‹t∈R› have "t⋅u⋅(ya⋅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 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 ‹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⋅ya)\<ra>(t⋅u⋅z) ∈ P"
          using ideal_dest_sum unfolding primeIdeal_def by simp
        with ‹t∈R› ‹ya∈R› ‹z∈R› ‹u∈R› have "t⋅u⋅(ya\<ra>z) ∈ P"
          using Ring_ZF_1_L4(3) ring_oper_distr(1) by simp     
      } thus ?thesis by simp
    qed
    moreover have "∀ya∈⟨{x}⟩I. ∀u∈R. ya⋅u⋅y ∈ P"
    proof -
      from ‹x∈R› have "{x}≠0" and "{x}⊆R" 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 -
        { fix ya z q u assume
            ass: "ya∈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 "ya⋅(q⋅(z⋅u)⋅y) ∈ P"
            using Ring_ZF_1_L4(3) ideal_dest_mult(2)
            unfolding primeIdeal_def by simp
          with ‹y∈R› ‹ya∈R› ‹z∈R› ‹u ∈ R› ‹q∈R› 
            have "ya⋅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 "∀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 -
        { fix ya z u assume "ya∈R" "z∈R" "u∈R"
            "∀u∈R. ya⋅u⋅y ∈ P" "∀u∈R. z⋅u⋅y ∈ P"
          with assms ‹y∈R› have "((ya\<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 "∀xa∈{y}. ∀t∈⟨{x}⟩I. ∀u∈R. t⋅u⋅xa ∈ 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 tx ty where 
        "tx∈?X" "ty∈?Y" and t: "t= tx⋅ty"
        using func_imagedef mult_monoid.monoid_oper_fun 
        by auto
      with R ‹tx∈?X› ‹ty∈?Y› have "tx⋅𝟭⋅ty ∈P" 
        using Ring_ZF_1_L2(2) by auto  
      moreover from ‹x∈R› ‹tx∈?X› have "tx∈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 xa 
    assume "I◃R" "I⊆R" "J◃R" "J⊆R" "I⋅IJ ⊆ P" "x∈J" "x∉P" "xa∈I"
    from ‹I⊆R› ‹J⊆R› have "I×J ⊆ R×R" by auto
    { fix z assume "z∈R"
      with ‹I◃R› ‹x∈J› ‹xa∈I› ‹I×J ⊆ R×R› have "(xa⋅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 "xa⋅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› ‹xa∈I› have "xa∈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
  "x2⇧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``{x2} = 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