Theory Ideal_Lattice

section ‹The lattice of ideals›

theory Ideal_Lattice
  imports Ideal_Theory Order_Theory
begin

text ‹The ideals of a commutative ring ‹R›, ordered by inclusion, form a complete lattice: the
  infimum of a family of ideals is their intersection (with ‹R›, so the empty family has infimum
  ‹R›), and the supremum is the ideal generated by their union.  Together with the subgroup lattice
  this exercises the abstract order theory on the two archetypal substructure lattices.  As a
  by-product we obtain the ideal ∗‹generated by a set›, the analogue of the subgroup ‹generate›.›

context commutative_ring
begin

subsection ‹Intersections of ideals›

text ‹The intersection of a nonempty family of ideals is an ideal.›
lemma ideal_Inter:
  assumes ne: "𝒜 ≠ {}" and id: "⋀I. I ∈ 𝒜 ⟹ Ideal I R (+) (⋅) 𝟬 𝟭"
  shows "Ideal (⋂ 𝒜) R (+) (⋅) 𝟬 𝟭"
proof -
  obtain I0 where I0: "I0 ∈ 𝒜" using ne by blast
  interpret I0: Ideal I0 R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF I0])
  have sg: "Subgroup (⋂ 𝒜) R (+) 𝟬"
  proof (rule additive.subgroupI)
    show "⋂ 𝒜 ⊆ R" using I0 I0.additive.subset by blast
  next
    show "𝟬 ∈ ⋂ 𝒜"
    proof
      fix I assume "I ∈ 𝒜"
      then interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id)
      show "𝟬 ∈ I" by (rule I.additive.sub_unit_closed)
    qed
  next
    fix g h assume g: "g ∈ ⋂ 𝒜" and h: "h ∈ ⋂ 𝒜"
    show "g + h ∈ ⋂ 𝒜"
    proof
      fix I assume I: "I ∈ 𝒜"
      then interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id)
      show "g + h ∈ I" using g h I by (blast intro: I.additive.sub_composition_closed)
    qed
  next
    fix g assume "g ∈ ⋂ 𝒜"
    then have "g ∈ R" using I0 I0.additive.subset by blast
    then show "additive.invertible g" by simp
  next
    fix g assume g: "g ∈ ⋂ 𝒜"
    show "additive.inverse g ∈ ⋂ 𝒜"
    proof
      fix I assume I: "I ∈ 𝒜"
      then interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id)
      have "g ∈ I" using g I by blast
      then show "additive.inverse g ∈ I"
        using I.additive.submonoid_inverse_closed I.additive.sub.invertible by blast
    qed
  qed
  interpret S: Subgroup "⋂ 𝒜" R "(+)" 𝟬 by (rule sg)
  show ?thesis
  proof unfold_locales
    fix a b assume a: "a ∈ R" and b: "b ∈ ⋂ 𝒜"
    show "a ⋅ b ∈ ⋂ 𝒜"
    proof
      fix I assume I: "I ∈ 𝒜"
      then interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id)
      show "a ⋅ b ∈ I" using a b I by (blast intro: I.Ideal(1))
    qed
    show "b ⋅ a ∈ ⋂ 𝒜"
    proof
      fix I assume I: "I ∈ 𝒜"
      then interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id)
      show "b ⋅ a ∈ I" using a b I by (blast intro: I.Ideal(2))
    qed
  qed
qed


text ‹The whole ring is an ideal of itself (the top of the ideal lattice).›
lemma whole_ideal: "Ideal R R (+) (⋅) 𝟬 𝟭"
proof -
  have "Subgroup R R (+) 𝟬"
    by (rule additive.subgroupI) auto
  then interpret S: Subgroup R R "(+)" 𝟬 .
  show ?thesis by unfold_locales auto
qed


subsection ‹The ideal generated by a set›

text ‹The ideal generated by a subset ‹S› of the ring: the intersection of all ideals containing
  ‹S ∩ R›.  (Intersecting with ‹R› in the guard mirrors the subgroup ‹generate›, so elements outside
  the carrier are ignored.)›
definition ideal_generated :: "'a set ⇒ 'a set"
  where "ideal_generated S = ⋂ {I. Ideal I R (+) (⋅) 𝟬 𝟭 ∧ S ∩ R ⊆ I}"

lemma ideal_generated_is_ideal: "Ideal (ideal_generated S) R (+) (⋅) 𝟬 𝟭"
proof -
  have "R ∈ {I. Ideal I R (+) (⋅) 𝟬 𝟭 ∧ S ∩ R ⊆ I}"
    using whole_ideal by auto
  then have ne: "{I. Ideal I R (+) (⋅) 𝟬 𝟭 ∧ S ∩ R ⊆ I} ≠ {}" by blast
  show ?thesis
    unfolding ideal_generated_def by (rule ideal_Inter[OF ne]) auto
qed

lemma ideal_generated_incl: "S ∩ R ⊆ ideal_generated S"
  unfolding ideal_generated_def by blast

lemma ideal_generated_minimal:
  assumes "Ideal J R (+) (⋅) 𝟬 𝟭" "S ∩ R ⊆ J"
  shows "ideal_generated S ⊆ J"
  unfolding ideal_generated_def using assms by (blast intro: Inter_lower)

lemma ideal_generated_subset_carrier: "ideal_generated S ⊆ R"
proof -
  interpret gen: Ideal "ideal_generated S" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideal_generated_is_ideal)
  show ?thesis by (rule gen.additive.subset)
qed


subsection ‹The product of two ideals›

text ‹The product ‹I ⊙ J› of two ideals is the ideal generated by all products ‹i ⋅ j› with
  ‹i ∈ I› and ‹j ∈ J›.  Together with the ideal sum and the intersection this completes the
  semiring of ideals; the product is contained in the intersection (hence, unlike sum and
  intersection, is in general ∗‹not› a lattice operation).›
definition ideal_prod :: "'a set ⇒ 'a set ⇒ 'a set"  (infixl ‹⊙› 70)
  where "I ⊙ J = ideal_generated {i ⋅ j |i j. i ∈ I ∧ j ∈ J}"

lemma ideal_prod_is_ideal: "Ideal (I ⊙ J) R (+) (⋅) 𝟬 𝟭"
  unfolding ideal_prod_def by (rule ideal_generated_is_ideal)

lemma ideal_prod_subset_carrier: "I ⊙ J ⊆ R"
  unfolding ideal_prod_def by (rule ideal_generated_subset_carrier)

text ‹Generators lie in the product.›
lemma ideal_prod_memI:
  assumes I: "Ideal I R (+) (⋅) 𝟬 𝟭" and J: "Ideal J R (+) (⋅) 𝟬 𝟭"
    and i: "i ∈ I" and j: "j ∈ J"
  shows "i ⋅ j ∈ I ⊙ J"
proof -
  interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
  interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule J)
  have "i ⋅ j ∈ R" using i j I.additive.subset J.additive.subset by blast
  moreover have "i ⋅ j ∈ {i ⋅ j |i j. i ∈ I ∧ j ∈ J}" using i j by blast
  ultimately have "i ⋅ j ∈ {i ⋅ j |i j. i ∈ I ∧ j ∈ J} ∩ R" by blast
  also have "… ⊆ ideal_generated {i ⋅ j |i j. i ∈ I ∧ j ∈ J}" by (rule ideal_generated_incl)
  finally show ?thesis unfolding ideal_prod_def .
qed

text ‹The product is contained in both factors, hence in their intersection.›
lemma ideal_prod_subset:
  assumes I: "Ideal I R (+) (⋅) 𝟬 𝟭" and J: "Ideal J R (+) (⋅) 𝟬 𝟭"
  shows "I ⊙ J ⊆ I ∩ J"
proof -
  interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
  interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule J)
  have gen: "{i ⋅ j |i j. i ∈ I ∧ j ∈ J} ∩ R ⊆ I ∩ J"
  proof
    fix x assume "x ∈ {i ⋅ j |i j. i ∈ I ∧ j ∈ J} ∩ R"
    then obtain i j where x: "x = i ⋅ j" and i: "i ∈ I" and j: "j ∈ J" by blast
    have "i ⋅ j ∈ I" using i j J.additive.subset by (blast intro: I.Ideal(2))
    moreover have "i ⋅ j ∈ J" using i j I.additive.subset by (blast intro: J.Ideal(1))
    ultimately show "x ∈ I ∩ J" using x by simp
  qed
  have "Ideal (⋂ {I, J}) R (+) (⋅) 𝟬 𝟭"
    by (rule ideal_Inter) (use I J in auto)
  then have IJ: "Ideal (I ∩ J) R (+) (⋅) 𝟬 𝟭" by simp
  show ?thesis
    unfolding ideal_prod_def by (rule ideal_generated_minimal[OF IJ]) (use gen in simp)
qed

text ‹Commutativity: the generating sets coincide because the ring is commutative.›
lemma ideal_prod_commute:
  assumes I: "Ideal I R (+) (⋅) 𝟬 𝟭" and J: "Ideal J R (+) (⋅) 𝟬 𝟭"
  shows "I ⊙ J = J ⊙ I"
proof -
  interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
  interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule J)
  have "{i ⋅ j |i j. i ∈ I ∧ j ∈ J} = {j ⋅ i |i j. i ∈ I ∧ j ∈ J}"
    using I.additive.subset J.additive.subset by (blast intro: multiplicative.commutative)
  also have "… = {j ⋅ i |j i. j ∈ J ∧ i ∈ I}" by blast
  finally show ?thesis unfolding ideal_prod_def by simp
qed


subsection ‹The complete lattice of ideals›

definition ideals :: "'a set set"
  where "ideals = {I. Ideal I R (+) (⋅) 𝟬 𝟭}"

lemma ideals_iff [simp]: "I ∈ ideals ⟷ Ideal I R (+) (⋅) 𝟬 𝟭"
  by (simp add: ideals_def)

interpretation ideal_order: Partial_Order ideals "(⊆)"
  by unfold_locales auto

interpretation ideal_lattice: Complete_Lattice ideals "(⊆)"
proof (unfold_locales)
  fix 𝒜 :: "'a set set" assume 𝒜: "𝒜 ⊆ ideals"
  ― ‹Supremum: the ideal generated by the union.›
  let ?s = "ideal_generated (⋃ 𝒜)"
  have s_id: "Ideal ?s R (+) (⋅) 𝟬 𝟭" by (rule ideal_generated_is_ideal)
  have "ideal_order.is_sup ?s 𝒜"
  proof (rule ideal_order.is_supI)
    show "ideal_order.upper_bound ?s 𝒜"
    proof (rule ideal_order.upper_boundI)
      show "?s ∈ ideals" using s_id by simp
      fix I assume I: "I ∈ 𝒜"
      then interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 using 𝒜 by auto
      have "I ⊆ ⋃ 𝒜 ∩ R" using I I.additive.subset by blast
      then show "I ⊆ ?s" using ideal_generated_incl by blast
    qed
  next
    fix x assume "ideal_order.upper_bound x 𝒜"
    then have xid: "Ideal x R (+) (⋅) 𝟬 𝟭" and dom: "⋀I. I ∈ 𝒜 ⟹ I ⊆ x"
      by (auto dest: ideal_order.upper_boundD simp: ideal_order.upper_bound_def)
    have "⋃ 𝒜 ∩ R ⊆ x"
    proof
      fix y assume "y ∈ ⋃ 𝒜 ∩ R"
      then obtain I where "I ∈ 𝒜" "y ∈ I" by blast
      then show "y ∈ x" using dom by blast
    qed
    then show "?s ⊆ x" using xid by (intro ideal_generated_minimal) auto
  qed
  then show "∃s. ideal_order.is_sup s 𝒜" ..
next
  fix 𝒜 :: "'a set set" assume 𝒜: "𝒜 ⊆ ideals"
  ― ‹Infimum: the intersection of ‹𝒜› together with ‹R›.›
  let ?i = "⋂ (insert R 𝒜)"
  have all_id: "⋀I. I ∈ insert R 𝒜 ⟹ Ideal I R (+) (⋅) 𝟬 𝟭"
    using 𝒜 whole_ideal by auto
  have i_id: "Ideal ?i R (+) (⋅) 𝟬 𝟭" by (rule ideal_Inter) (use all_id in auto)
  have "ideal_order.is_inf ?i 𝒜"
  proof (rule ideal_order.is_infI)
    show "ideal_order.lower_bound ?i 𝒜"
    proof (rule ideal_order.lower_boundI)
      show "?i ∈ ideals" using i_id by simp
      fix I assume "I ∈ 𝒜" then show "?i ⊆ I" by blast
    qed
  next
    fix x assume "ideal_order.lower_bound x 𝒜"
    then have xid: "Ideal x R (+) (⋅) 𝟬 𝟭" and dom: "⋀I. I ∈ 𝒜 ⟹ x ⊆ I"
      by (auto dest: ideal_order.lower_boundD simp: ideal_order.lower_bound_def)
    interpret x: Ideal x R "(+)" "(⋅)" 𝟬 𝟭 by (rule xid)
    show "x ⊆ ?i" using dom x.additive.subset by blast
  qed
  then show "∃i. ideal_order.is_inf i 𝒜" ..
qed

end

end