Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Ideal_Product.thy Sprache: Isabelle

Original von: Isabelle^©

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

theory Ideal_Product
  imports Ideal
begin

section \<open>Product of Ideals\<close>

text \<open>In this section, we study the structure of the set of ideals of a given ring.\<close>

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 \\<^bsub>R\<^esub> j \ ideal_prod R I J"
  |  sum: "\ s1 \ ideal_prod R I J; s2 \ ideal_prod R I J \ \ s1 \\<^bsub>R\<^esub> 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 = { \<zero>\<^bsub>R\<^esub> },
                              add = set_add R \<rparr>"

subsection \<open>Basic Properties\<close>

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 is_ring .
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\<^bsub>add_monoid R\<^esub> s1 \ I \ J" using s1
    proof (induct s1 rule: ideal_prod.induct)
      case (prod i j)
      hence "inv\<^bsub>add_monoid R\<^esub> (i \ j) = (inv\<^bsub>add_monoid R\<^esub> i) \ j"
        by (metis a_inv_def assms(1) assms(2) ideal.Icarr l_minus)
      thus ?case using ideal_prod.prod[of "inv\<^bsub>add_monoid R\<^esub> 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 \<open>i \<in> I\<close> 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 \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (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 \<open>The following result would also be true for locale ring\<close>
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 \<open>Structure of the Set of Ideals\<close>

text \<open>We focus on commutative rings for convenience.\<close>

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 \<noteq> j \<Longrightarrow> (I i) <+> (I j) = carrier R"
  shows "(\\<^bsub>(ideals_set R)\<^esub> k \ {..n}. I k) <+> (I (Suc n)) = carrier R" using assms
proof (induct n arbitrary: I)
  case 0
  hence "(\\<^bsub>(ideals_set R)\<^esub> 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 \<noteq> j \<Longrightarrow> (?I' i) <+> (?I' j) = carrier R"
    by (simp add: Suc.prems(2))
  ultimately have "(\\<^bsub>(ideals_set R)\<^esub> 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 "(\\<^bsub>(ideals_set R)\<^esub> 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) = ((\\<^bsub>(ideals_set R)\<^esub> k \ {Suc 0..Suc n}. I k) <+> I (Suc (Suc n))) \ (I 0)"
    by auto
  moreover have fprod_cl1: "ideal (\\<^bsub>(ideals_set R)\<^esub> 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 = (\\<^bsub>(ideals_set R)\<^esub> 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) \ (\\<^bsub>(ideals_set R)\<^esub> 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) \\<^bsub>(ideals_set R)\<^esub> (\\<^bsub>(ideals_set R)\<^esub> k \ {Suc 0..Suc n}. I k) <+>
                     I (Suc (Suc n)) \<cdot> (I 0)"
    by (simp add: ideals_set_def)
  finally have I0: "I 0 = (\\<^bsub>(ideals_set R)\<^esub> 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 (\\<^bsub>(ideals_set R)\<^esub> 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)) <+>
                    ((\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..Suc n}. I k) <+> I (Suc (Suc n)) \<cdot> (I 0))"
    using I0 by auto
  also have " ... = I (Suc (Suc n)) <+>
                    (I (Suc (Suc n)) \<cdot> (I 0) <+> (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..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)) <+>
                    (\<Otimes>\<^bsub>(ideals_set R)\<^esub> k \<in> {..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)) <+> (\\<^bsub>(ideals_set R)\<^esub> k \ {..Suc n}. I k)"
    using ideal_prod_simp[of "I (Suc (Suc n))" "I 0"] I_SucSuc_I0 by simp
  also have " ... = (\\<^bsub>(ideals_set R)\<^esub> 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 "(\\<^bsub>(ideals_set R)\<^esub> 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: "(\\<^bsub>(ideals_set R)\<^esub> k \ {..n}. I k) = (\ k \ {..n}. I k)"
    by (simp add: atMost_Suc)
  hence "(\\<^bsub>(ideals_set R)\<^esub> k \ {..Suc n}. I k) = I (Suc n) \\<^bsub>(ideals_set R)\<^esub> (\ 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 "(\\<^bsub>(ideals_set R)\<^esub> 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 "(\\<^bsub>(ideals_set R)\<^esub> 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' = (\<lambda>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 \<open>Another Characterization of Prime Ideals\<close>

text \<open>With product of ideals being defined, we can give another definition of a prime ideal\<close>

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

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.