Theory HOL-Algebra.Ideal_Product

(*  Title:      HOL/Algebra/Ideal_Product.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Ideal_Product
  imports Ideal
begin

section ‹Product of Ideals›

text ‹In this section, we study the structure of the set of ideals of a given ring.›

inductive_set
  ideal_prod :: "[ ('a, 'b) ring_scheme, 'a set, 'a set ]  'a set" (infixl "ı" 80)
  for R and I and J (* both I and J are supposed ideals *) where
    prod: " i  I; j  J   i Rj  ideal_prod R I J"
  |  sum: " s1  ideal_prod R I J; s2  ideal_prod R I J   s1 Rs2  ideal_prod R I J"

definition ideals_set :: "('a, 'b) ring_scheme  ('a set) ring"
  where "ideals_set R =  carrier = { I. ideal I R },
                             mult = ideal_prod R,
                              one = carrier R,
                             zero = { 𝟬R},
                              add = set_add R "


subsection ‹Basic Properties›

lemma (in ring) ideal_prod_in_carrier:
  assumes "ideal I R" "ideal J R"
  shows "I  J  carrier R"
proof
  fix s assume "s  I  J" thus "s  carrier R"
    by (induct s rule: ideal_prod.induct) (auto, meson assms ideal.I_l_closed ideal.Icarr) 
qed

lemma (in ring) ideal_prod_inter:
  assumes "ideal I R" "ideal J R"
  shows "I  J  I  J"
proof
  fix s assume "s  I  J" thus "s  I  J"
    apply (induct s rule: ideal_prod.induct)
    apply (auto, (meson assms ideal.I_r_closed ideal.I_l_closed ideal.Icarr)+)
    apply (simp_all add: additive_subgroup.a_closed assms ideal.axioms(1))
    done
qed

lemma (in ring) ideal_prod_is_ideal:
  assumes "ideal I R" "ideal J R"
  shows "ideal (I  J) R"
proof (rule idealI)
  show "ring R" using ring_axioms .
next
  show "subgroup (I  J) (add_monoid R)"
    unfolding subgroup_def
  proof (auto)
    show "𝟬  I  J" using ideal_prod.prod[of 𝟬 I 𝟬 J R]
      by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
  next
    fix s1 s2 assume s1: "s1  I  J" and s2: "s2  I  J"
    have IJcarr: "a. a  I  J  a  carrier R"
      by (meson assms subsetD ideal_prod_in_carrier)
    show "s1  carrier R" using ideal_prod_in_carrier[OF assms] s1 by blast
    show "s1  s2  I  J" by (simp add: ideal_prod.sum[OF s1 s2])
    show "invadd_monoid Rs1  I  J" using s1
    proof (induct s1 rule: ideal_prod.induct)
      case (prod i j)
      hence "invadd_monoid R(i  j) = (invadd_monoid Ri)  j"
        by (metis a_inv_def assms(1) assms(2) ideal.Icarr l_minus)
      thus ?case using ideal_prod.prod[of "invadd_monoid Ri" I j J R] assms
        by (simp add: additive_subgroup.a_subgroup ideal.axioms(1) prod.hyps subgroup.m_inv_closed)
    next
      case (sum s1 s2) thus ?case
        by (metis (no_types) IJcarr a_inv_def add.inv_mult_group ideal_prod.sum sum.hyps)
    qed
  qed
next
  fix s x assume s: "s  I  J" and x: "x  carrier R"
  show "x  s  I  J" using s
  proof (induct s rule: ideal_prod.induct)
    case (prod i j) thus ?case using ideal_prod.prod[of "x  i" I j J R] assms
      by (simp add: x ideal.I_l_closed ideal.Icarr m_assoc)
  next
    case (sum s1 s2) thus ?case
    proof -
      have IJ: "I  J  carrier R"
        by (metis (no_types) assms(1) assms(2) ideal.axioms(2) ring.ideal_prod_in_carrier)
      then have "s2  carrier R"
        using sum.hyps(3) by blast
      moreover have "s1  carrier R"
        using IJ sum.hyps(1) by blast
      ultimately show ?thesis
        by (simp add: ideal_prod.sum r_distr sum.hyps x)
    qed
  qed
  show "s  x  I  J" using s
  proof (induct s rule: ideal_prod.induct)
    case (prod i j) thus ?case using ideal_prod.prod[of i I "j  x" J R] assms x
      by (simp add: x ideal.I_r_closed ideal.Icarr m_assoc)
  next
    case (sum s1 s2) thus ?case 
    proof -
      have "s1  carrier R" "s2  carrier R"
        by (meson assms subsetD ideal_prod_in_carrier sum.hyps)+
      then show ?thesis
        by (metis ideal_prod.sum l_distr sum.hyps(2) sum.hyps(4) x)
    qed
  qed
qed

lemma (in ring) ideal_prod_eq_genideal:
  assumes "ideal I R" "ideal J R"
  shows "I  J = Idl (I <#> J)"
proof
  have "I <#> J  I  J"
  proof
    fix s assume "s  I <#> J"
    then obtain i j where "i  I" "j  J" "s = i  j"
      unfolding set_mult_def by blast
    thus "s  I  J" using ideal_prod.prod by simp
  qed
  thus "Idl (I <#> J)  I  J"
    unfolding genideal_def using ideal_prod_is_ideal[OF assms] by blast
next
  show "I  J  Idl (I <#> J)"
  proof
    fix s assume "s  I  J" thus "s  Idl (I <#> J)"
    proof (induct s rule: ideal_prod.induct)
      case (prod i j) hence "i  j  I <#> J" unfolding set_mult_def by blast
      thus ?case unfolding genideal_def by blast 
    next
      case (sum s1 s2) thus ?case
        by (simp add: additive_subgroup.a_closed additive_subgroup.a_subset
            assms genideal_ideal ideal.axioms(1) set_mult_closed)
    qed
  qed
qed


lemma (in ring) ideal_prod_simp:
  assumes "ideal I R" "ideal J R" (* the second assumption could be suppressed *)
  shows "I = I <+> (I  J)"
proof
  show "I  I <+> I  J"
  proof
    fix i assume "i  I" hence "i  𝟬  I <+> I  J"
      using set_add_def'[of R I "I  J"] ideal_prod_is_ideal[OF assms]
            additive_subgroup.zero_closed[OF ideal.axioms(1), of "I  J" R] by auto
    thus "i  I <+> I  J"
      using i  I assms(1) ideal.Icarr by fastforce 
  qed
next
  show "I <+> I  J  I"
  proof
    fix s assume "s  I <+> I  J"
    then obtain i ij where "i  I" "ij  I  J" "s = i  ij"
      using set_add_def'[of R I "I  J"] by auto
    thus "s  I"
      using ideal_prod_inter[OF assms]
      by (meson additive_subgroup.a_closed assms(1) ideal.axioms(1) inf_sup_ord(1) subsetCE) 
  qed
qed

lemma (in ring) ideal_prod_one:
  assumes "ideal I R"
  shows "I  (carrier R) = I"
proof
  show "I  (carrier R)  I"
  proof
    fix s assume "s  I  (carrier R)" thus "s  I"
      by (induct s rule: ideal_prod.induct)
         (simp_all add: assms ideal.I_r_closed additive_subgroup.a_closed ideal.axioms(1))
  qed
next
  show "I  I  (carrier R)"
  proof
    fix i assume "i  I" thus "i   I  (carrier R)"
      by (metis assms ideal.Icarr ideal_prod.simps one_closed r_one)
  qed
qed

lemma (in ring) ideal_prod_zero:
  assumes "ideal I R"
  shows "I  { 𝟬 } = { 𝟬 }"
proof
  show "I  { 𝟬 }  { 𝟬 }"
  proof
    fix s assume "s  I  {𝟬}" thus "s  { 𝟬 }"
      using assms ideal.Icarr by (induct s rule: ideal_prod.induct) (fastforce, simp)
  qed
next
  show "{ 𝟬 }  I  { 𝟬 }"
    by (simp add: additive_subgroup.zero_closed assms
                  ideal.axioms(1) ideal_prod_is_ideal zeroideal)
qed

lemma (in ring) ideal_prod_assoc:
  assumes "ideal I R" "ideal J R" "ideal K R"
  shows "(I  J)  K = I  (J  K)"
proof
  show "(I  J)  K  I  (J  K)"
  proof
    fix s assume "s  (I  J)  K" thus "s  I  (J  K)"
    proof (induct s rule: ideal_prod.induct)
      case (sum s1 s2) thus ?case
        by (simp add: ideal_prod.sum)
    next
      case (prod i k) thus ?case
      proof (induct i rule: ideal_prod.induct)
        case (prod i j) thus ?case
          using ideal_prod.prod[OF prod(1) ideal_prod.prod[OF prod(2-3),of R], of R]
          by (metis assms ideal.Icarr m_assoc) 
      next
        case (sum s1 s2) thus ?case
        proof -
          have "s1  carrier R" "s2  carrier R"
            by (meson assms subsetD ideal.axioms(2) ring.ideal_prod_in_carrier sum.hyps)+
          moreover have "k  carrier R"
            by (meson additive_subgroup.a_Hcarr assms(3) ideal.axioms(1) sum.prems)
          ultimately show ?thesis
            by (metis ideal_prod.sum l_distr sum.hyps(2) sum.hyps(4) sum.prems)
        qed
      qed
    qed
  qed
next
  show "I  (J  K)  (I  J)  K"
  proof
    fix s assume "s  I  (J  K)" thus "s  (I  J)  K"
    proof (induct s rule: ideal_prod.induct)
      case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum)
    next
      case (prod i j) show ?case using prod(2) prod(1)
      proof (induct j rule: ideal_prod.induct)
        case (prod j k) thus ?case
          using ideal_prod.prod[OF ideal_prod.prod[OF prod(3) prod(1), of R] prod (2), of R]
          by (metis assms ideal.Icarr m_assoc)
      next
        case (sum s1 s2) thus ?case
        proof -
          have "a A B. a  B  A; ideal A R; ideal B R  a  carrier R"
            by (meson subsetD ideal_prod_in_carrier)
          moreover have "i  carrier R"
            by (meson additive_subgroup.a_Hcarr assms(1) ideal.axioms(1) sum.prems)
          ultimately show ?thesis
            by (metis (no_types) assms(2) assms(3) ideal_prod.sum r_distr sum)
        qed
      qed
    qed
  qed
qed

lemma (in ring) ideal_prod_r_distr:
  assumes "ideal I R" "ideal J R" "ideal K R"
  shows "I  (J <+> K) = (I  J) <+>  (I  K)"
proof
  show "I  (J <+> K)  I  J <+> I  K"
  proof
    fix s assume "s  I  (J <+> K)" thus "s  I  J <+> I  K"
    proof(induct s rule: ideal_prod.induct)
      case (prod i jk)
      then obtain j k where j: "j  J" and k: "k  K" and jk: "jk = j  k"
        using set_add_def'[of R J K] by auto
      hence "i  j  i  k  I  J <+> I  K"
        using ideal_prod.prod[OF prod(1) j,of R]
              ideal_prod.prod[OF prod(1) k,of R]
              set_add_def'[of R "I  J" "I  K"] by auto
      thus ?case
        using assms ideal.Icarr r_distr jk j k prod(1) by metis 
    next
      case (sum s1 s2) thus ?case
        by (simp add: add_ideals additive_subgroup.a_closed assms ideal.axioms(1)
                      local.ring_axioms ring.ideal_prod_is_ideal) 
    qed
  qed
next
  { fix s J K assume A: "ideal J R" "ideal K R" "s  I  J"
    have "s  I  (J <+> K)  s  I  (K <+> J)"
    proof -
      from s  I  J have "s  I  (J <+> K)"
      proof (induct s rule: ideal_prod.induct)
        case (prod i j)
        hence "(j  𝟬)  J <+> K"
          using set_add_def'[of R J K]
                additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
        thus ?case
          by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)  
      next
        case (sum s1 s2) thus ?case
          by (simp add: ideal_prod.sum) 
      qed
      thus ?thesis
        by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute) 
    qed } note aux_lemma = this

  show "I  J <+> I  K  I  (J <+> K)"
  proof
    fix s assume "s  I  J <+> I  K"
    then obtain s1 s2 where s1: "s1  I  J" and s2: "s2  I  K" and  s: "s = s1  s2"
      using set_add_def'[of R "I  J" "I  K"] by auto
    thus "s  I  (J <+> K)"
      using aux_lemma[OF assms(2) assms(3) s1]
            aux_lemma[OF assms(3) assms(2) s2] by (simp add: ideal_prod.sum)
  qed
qed

lemma (in cring) ideal_prod_commute:
  assumes "ideal I R" "ideal J R"
  shows "I  J = J  I"
proof -
  { fix I J assume A: "ideal I R" "ideal J R"
    have "I  J  J  I"
    proof
      fix s assume "s  I  J" thus "s  J  I"
      proof (induct s rule: ideal_prod.induct)
        case (prod i j) thus ?case
          using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
          by (simp add: ideal_prod.prod)
      next
        case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum) 
      qed
    qed }
  thus ?thesis using assms by blast 
qed

text ‹The following result would also be true for locale ring›
lemma (in cring) ideal_prod_distr:
  assumes "ideal I R" "ideal J R" "ideal K R"
  shows "I  (J <+> K) = (I  J) <+>  (I  K)"
    and "(J <+> K)  I = (J  I) <+>  (K  I)"
  by (simp_all add: assms ideal_prod_commute local.ring_axioms
                    ring.add_ideals ring.ideal_prod_r_distr)

lemma (in cring) ideal_prod_eq_inter:
  assumes "ideal I R" "ideal J R"
    and "I <+> J = carrier R"
  shows "I  J = I  J"
proof
  show "I  J  I  J"
    using assms ideal_prod_inter by auto
next
  show "I  J  I  J"
  proof
    have "𝟭  I <+> J" using assms(3) one_closed by simp 
    then obtain i j where ij: "i  I" "j  J" "𝟭 = i  j"
      using set_add_def'[of R I J] by auto

    fix s assume s: "s  I  J"
    hence "(i  s  I  J)  (s  j  I  J)"
      using ij(1-2) by (simp add: ideal_prod.prod)
    moreover have "s = (i  s)  (s  j)"
      using ideal.Icarr[OF assms(1) ij(1)]
            ideal.Icarr[OF assms(2) ij(2)]
            ideal.Icarr[OF assms(1), of s]
      by (metis ij(3) s m_comm[of s i] Int_iff r_distr r_one)
    ultimately show "s   I  J"
      using ideal_prod.sum by fastforce
  qed
qed


subsection ‹Structure of the Set of Ideals›

text ‹We focus on commutative rings for convenience.›

lemma (in cring) ideals_set_is_semiring: "semiring (ideals_set R)"
proof -
  have "abelian_monoid (ideals_set R)"
    apply (rule abelian_monoidI) unfolding ideals_set_def
    apply (simp_all add: add_ideals zeroideal)
    apply (simp add: add.set_mult_assoc additive_subgroup.a_subset ideal.axioms(1) set_add_defs(1))
    apply (metis Un_absorb1 additive_subgroup.a_subset additive_subgroup.zero_closed
        cgenideal_minimal cgenideal_self empty_iff genideal_minimal ideal.axioms(1)
        local.ring_axioms order_refl ring.genideal_self subset_antisym subset_singletonD
        union_genideal zero_closed zeroideal)
    by (metis sup_commute union_genideal)

  moreover have "monoid (ideals_set R)"
    apply (rule monoidI) unfolding ideals_set_def
    apply (simp_all add: ideal_prod_is_ideal oneideal
                         ideal_prod_commute ideal_prod_one)
    by (metis ideal_prod_assoc ideal_prod_commute)

  ultimately show ?thesis
    unfolding semiring_def semiring_axioms_def ideals_set_def
    by (simp_all add: ideal_prod_distr ideal_prod_commute ideal_prod_zero zeroideal) 
qed

lemma (in cring) ideals_set_is_comm_monoid: "comm_monoid (ideals_set R)"
proof -
  have "monoid (ideals_set R)"
    apply (rule monoidI) unfolding ideals_set_def
    apply (simp_all add: ideal_prod_is_ideal oneideal
                         ideal_prod_commute ideal_prod_one)
    by (metis ideal_prod_assoc ideal_prod_commute)
  thus ?thesis
    unfolding comm_monoid_def comm_monoid_axioms_def
    by (simp add: ideal_prod_commute ideals_set_def)
qed

lemma (in cring) ideal_prod_eq_Inter_aux:
  assumes "I: {..(Suc n)}  { J. ideal J R }" 
    and "i j.  i  Suc n; j  Suc n  
                 i  j  (I i) <+> (I j) = carrier R"
  shows "((ideals_set R)k  {..n}. I k) <+> (I (Suc n)) = carrier R" using assms
proof (induct n arbitrary: I)
  case 0
  hence "((ideals_set R)k  {..0}. I k) <+> I (Suc 0) = (I 0) <+> (I (Suc 0))"
    using comm_monoid.finprod_0[OF ideals_set_is_comm_monoid, of I]
    by (simp add: atMost_Suc ideals_set_def)
  also have " ... = carrier R"
    using 0(2)[of 0 "Suc 0"] by simp
  finally show ?case .
next
  interpret ISet: comm_monoid "ideals_set R"
    by (simp add: ideals_set_is_comm_monoid)

  case (Suc n)
  let ?I' = "λi. I (Suc i)"
  have "?I': {..(Suc n)}  { J. ideal J R }"
    using Suc.prems(1) by auto
  moreover have "i j.  i  Suc n; j  Suc n  
                         i  j  (?I' i) <+> (?I' j) = carrier R"
    by (simp add: Suc.prems(2))
  ultimately have "((ideals_set R)k  {..n}. ?I' k) <+> (?I' (Suc n)) = carrier R"
    using Suc.hyps by metis

  moreover have I_carr: "I: {..Suc (Suc n)}  carrier (ideals_set R)"
    unfolding ideals_set_def using Suc by simp
  hence I'_carr: "I  Suc ` {..n}  carrier (ideals_set R)" by auto
  ultimately have "((ideals_set R)k  {(Suc 0)..Suc n}. I k) <+> (I (Suc (Suc n))) = carrier R"
    using ISet.finprod_reindex[of I "λi. Suc i" "{..n}"] by (simp add: atMost_atLeast0) 

  hence "(carrier R)  (I 0) = (((ideals_set R)k  {Suc 0..Suc n}. I k) <+> I (Suc (Suc n)))  (I 0)"
    by auto
  moreover have fprod_cl1: "ideal ((ideals_set R)k  {Suc 0..Suc n}. I k) R"
    by (metis I'_carr ISet.finprod_closed One_nat_def ideals_set_def image_Suc_atMost
        mem_Collect_eq partial_object.select_convs(1))
  ultimately
  have "I 0 = ((ideals_set R)k  {Suc 0..Suc n}. I k)  (I 0) <+> I (Suc (Suc n))  (I 0)"
    by (metis PiE Suc.prems(1) atLeast0_atMost_Suc atLeast0_atMost_Suc_eq_insert_0
        atMost_atLeast0 ideal_prod_commute ideal_prod_distr(2) ideal_prod_one insertI1
        mem_Collect_eq oneideal)
  also have " ... = (I 0)  ((ideals_set R)k  {Suc 0..Suc n}. I k) <+> I (Suc (Suc n))  (I 0)"
    using fprod_cl1 ideal_prod_commute Suc.prems(1)
    by (simp add: atLeast0_atMost_Suc_eq_insert_0 atMost_atLeast0) 
  also have " ... = (I 0) (ideals_set R)((ideals_set R)k  {Suc 0..Suc n}. I k) <+>
                     I (Suc (Suc n))  (I 0)"
    by (simp add: ideals_set_def)
  finally have I0: "I 0 = ((ideals_set R)k  {..Suc n}. I k) <+> I (Suc (Suc n))  (I 0)"
    using ISet.finprod_insert[of "{Suc 0..Suc n}" 0 I]
          I_carr I'_carr atMost_atLeast0 ISet.finprod_0' atMost_Suc by auto

  have I_SucSuc_I0: "ideal (I (Suc (Suc n))) R  ideal (I 0) R"
    using Suc.prems(1) by auto
  have fprod_cl2: "ideal ((ideals_set R)k  {..Suc n}. I k) R"
    by (metis (no_types) ISet.finprod_closed I_carr Pi_split_insert_domain atMost_Suc ideals_set_def mem_Collect_eq partial_object.select_convs(1))
  have "carrier R = I (Suc (Suc n)) <+> I 0"
    by (simp add: Suc.prems(2))
  also have " ... = I (Suc (Suc n)) <+>
                    (((ideals_set R)k  {..Suc n}. I k) <+> I (Suc (Suc n))  (I 0))"
    using I0 by auto
  also have " ... = I (Suc (Suc n)) <+>
                    (I (Suc (Suc n))  (I 0) <+> ((ideals_set R)k  {..Suc n}. I k))"
    using fprod_cl2 I_SucSuc_I0 by (metis Un_commute ideal_prod_is_ideal union_genideal)
  also have " ... = (I (Suc (Suc n)) <+> I (Suc (Suc n))  (I 0)) <+>
                    ((ideals_set R)k  {..Suc n}. I k)"
    using fprod_cl2 I_SucSuc_I0 by (metis add.set_mult_assoc ideal_def ideal_prod_in_carrier
                                          oneideal ring.ideal_prod_one set_add_defs(1)) 
  also have " ... = I (Suc (Suc n)) <+> ((ideals_set R)k  {..Suc n}. I k)"
    using ideal_prod_simp[of "I (Suc (Suc n))" "I 0"] I_SucSuc_I0 by simp 
  also have " ... = ((ideals_set R)k  {..Suc n}. I k) <+> I (Suc (Suc n))"
    using fprod_cl2 I_SucSuc_I0 by (metis Un_commute union_genideal)
  finally show ?case by simp
qed

theorem (in cring) ideal_prod_eq_Inter:
  assumes "I: {..n :: nat}  { J. ideal J R }" 
    and "i j.  i  {..n}; j  {..n}   i  j  (I i) <+> (I j) = carrier R"
  shows "((ideals_set R)k  {..n}. I k) = ( k  {..n}. I k)" using assms
proof (induct n)
  case 0 thus ?case
    using comm_monoid.finprod_0[OF ideals_set_is_comm_monoid] by (simp add: ideals_set_def) 
next
  interpret ISet: comm_monoid "ideals_set R"
    by (simp add: ideals_set_is_comm_monoid)

  case (Suc n)
  hence IH: "((ideals_set R)k  {..n}. I k) = ( k  {..n}. I k)"
    by (simp add: atMost_Suc)
  hence "((ideals_set R)k  {..Suc n}. I k) = I (Suc n) (ideals_set R)( k  {..n}. I k)"
    using ISet.finprod_insert[of "{Suc 0..Suc n}" 0 I] atMost_Suc_eq_insert_0[of n]
    by (metis ISet.finprod_Suc Suc.prems(1) ideals_set_def partial_object.select_convs(1))
  hence "((ideals_set R)k  {..Suc n}. I k) = I (Suc n)  ( k  {..n}. I k)"
    by (simp add: ideals_set_def)
  moreover have "( k  {..n}. I k) <+> I (Suc n) = carrier R"
    using ideal_prod_eq_Inter_aux[of I n] by (simp add: Suc.prems IH)
  moreover have "ideal ( k  {..n}. I k) R"
    using ring.i_Intersect[of R "I ` {..n}"]
    by (metis IH ISet.finprod_closed Pi_split_insert_domain Suc.prems(1) atMost_Suc
              ideals_set_def mem_Collect_eq partial_object.select_convs(1))
  ultimately
  have "((ideals_set R)k  {..Suc n}. I k) = ( k  {..n}. I k)  I (Suc n)"
    using ideal_prod_eq_inter[of " k  {..n}. I k" "I (Suc n)"]
          ideal_prod_commute[of " k  {..n}. I k" "I (Suc n)"]
    by (metis PiE Suc.prems(1) atMost_iff mem_Collect_eq order_refl)
  thus ?case by (simp add: Int_commute atMost_Suc) 
qed

corollary (in cring) inter_plus_ideal_eq_carrier:
  assumes "i. i  Suc n  ideal (I i) R" 
      and "i j.  i  Suc n; j  Suc n; i  j   I i <+> I j = carrier R"
  shows "( i  n. I i) <+> (I (Suc n)) = carrier R"
  using ideal_prod_eq_Inter[of I n] ideal_prod_eq_Inter_aux[of I n] by (auto simp add: assms)

corollary (in cring) inter_plus_ideal_eq_carrier_arbitrary:
  assumes "i. i  Suc n  ideal (I i) R" 
      and "i j.  i  Suc n; j  Suc n; i  j   I i <+> I j = carrier R"
      and "j  Suc n"
  shows "( i  ({..(Suc n)} - { j }). I i) <+> (I j) = carrier R"
proof -
  define I' where "I' = (λi. if i = Suc n then (I j) else
                             if i = j     then (I (Suc n))
                                          else (I i))"
  have "i. i  Suc n  ideal (I' i) R"
    using I'_def assms(1) assms(3) by auto
  moreover have "i j.  i  Suc n; j  Suc n; i  j   I' i <+> I' j = carrier R"
    using I'_def assms(2-3) by force
  ultimately have "( i  n. I' i) <+> (I' (Suc n)) = carrier R"
    using inter_plus_ideal_eq_carrier by simp

  moreover have "I' ` {..n} = I ` ({..(Suc n)} - { j })"
  proof
    show "I' ` {..n}  I ` ({..Suc n} - {j})"
    proof
      fix x assume "x  I' ` {..n}"
      then obtain i where i: "i  {..n}" "I' i = x" by blast
      thus "x  I ` ({..Suc n} - {j})"
      proof (cases)
        assume "i = j" thus ?thesis using i I'_def by auto
      next
        assume "i  j" thus ?thesis using I'_def i insert_iff by auto
      qed
    qed
  next
    show "I ` ({..Suc n} - {j})  I' ` {..n}"
    proof
      fix x assume "x  I ` ({..Suc n} - {j})"
      then obtain i where i: "i  {..Suc n}" "i  j" "I i = x" by blast
      thus "x  I' ` {..n}"
      proof (cases)
        assume "i = Suc n" thus ?thesis using I'_def assms(3) i(2-3) by auto
      next
        assume "i  Suc n" thus ?thesis using I'_def i by auto
      qed
    qed
  qed
  ultimately show ?thesis using I'_def by metis 
qed


subsection ‹Another Characterization of Prime Ideals›

text ‹With product of ideals being defined, we can give another definition of a prime ideal›

lemma (in ring) primeideal_divides_ideal_prod:
  assumes "primeideal P R" "ideal I R" "ideal J R"
      and "I  J  P"
    shows "I  P  J  P"
proof (cases)
  assume " i  I. i  P"
  then obtain i where i: "i  I" "i  P" by blast
  have "J  P"
  proof
    fix j assume j: "j  J"
    hence "i  j  P"
      using ideal_prod.prod[OF i(1) j, of R] assms(4) by auto
    thus "j  P"
      using primeideal.I_prime[OF assms(1), of i j] i j
      by (meson assms(2-3) ideal.Icarr) 
  qed
  thus ?thesis by blast
next
  assume "¬ ( i  I. i  P)" thus ?thesis by blast
qed

lemma (in cring) divides_ideal_prod_imp_primeideal:
  assumes "ideal P R"
    and "P  carrier R"
    and "I J.  ideal I R; ideal J R; I  J  P   I  P  J  P"
  shows "primeideal P R"
proof -
  have "a b.  a  carrier R; b  carrier R; a  b  P   a  P  b  P"
  proof -
    fix a b assume A: "a  carrier R" "b  carrier R" "a  b  P"
    have "(PIdl a)  (PIdl b) = Idl (PIdl (a  b))"
      using ideal_prod_eq_genideal[of "Idl { a }" "Idl { b }"]
            A(1-2) cgenideal_eq_genideal cgenideal_ideal cgenideal_prod by auto
    hence "(PIdl a)  (PIdl b) = PIdl (a  b)"
      by (simp add: A Idl_subset_ideal cgenideal_ideal cgenideal_minimal
                    genideal_self oneideal subset_antisym)
    hence "(PIdl a)  (PIdl b)  P"
      by (simp add: A(3) assms(1) cgenideal_minimal)
    hence "(PIdl a)  P  (PIdl b)  P"
      by (simp add: A assms(3) cgenideal_ideal)
    thus "a  P  b  P"
      using A cgenideal_self by blast
  qed
  thus ?thesis
    using assms is_cring by (simp add: primeidealI)
qed

end