(* 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 ⊗⇘R⇙ j ∈ ideal_prod R I J" | sum: "⟦ s1 ∈ ideal_prod R I J; s2 ∈ ideal_prod R I J ⟧ ⟹ s1 ⊕⇘R⇙ s2 ∈ 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 "inv⇘add_monoid R⇙ s1 ∈ I ⋅ J" using s1 proof (induct s1 rule: ideal_prod.induct) case (prod i j) hence "inv⇘add_monoid R⇙ (i ⊗ j) = (inv⇘add_monoid R⇙ i) ⊗ j" by (metis a_inv_def assms(1) assms(2) ideal.Icarr l_minus) thus ?case using ideal_prod.prod[of "inv⇘add_monoid R⇙ i" 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