Theory Ideal_Theory

section ‹Prime and Maximal Ideals›

theory Ideal_Theory
  imports Ring_Theory "HOL.Zorn"
begin

text ‹Phase B: prime and maximal ideals, and the quotient characterisations.›

context Ideal
begin

text ‹Prime and maximal ideals: proper ideals with the usual closure / maximality property.›
definition prime_ideal :: bool
  where "prime_ideal ⟷ I ≠ R ∧ (∀a∈R. ∀b∈R. a ⋅ b ∈ I ⟶ a ∈ I ∨ b ∈ I)"

definition maximal_ideal :: bool
  where "maximal_ideal ⟷ I ≠ R ∧ (∀J. Ideal J R (+) (⋅) 𝟬 𝟭 ⟶ I ⊆ J ⟶ J = I ∨ J = R)"

text ‹The coset of an element and the set of all cosets (the quotient @{text "R/I"}), given clean
  names so they can be referred to from interpretations at the top level (the underlying
  @{text additive.Class}/@{text additive.Partition} live behind several sublocale hops and have no
  stable qualified name).›
definition coset :: "'a ⇒ 'a set"
  where "coset a = additive.Class a"

definition quotient_set :: "'a set set"
  where "quotient_set = additive.Partition"

lemma coset_eq_iff:
  assumes "a ∈ R" "b ∈ R" shows "coset a = coset b ⟷ a + (- b) ∈ I"
proof -
  have "coset a = coset b ⟷ (a, b) ∈ Ring_Congruence"
    unfolding coset_def
    using assms by (simp add: additive.Class_equivalence additive_congruence)
  also have "… ⟷ a + (- b) ∈ I" using assms by (auto simp: Ring_Congruence_def)
  finally show ?thesis .
qed

lemma coset_in_quotient_set: "a ∈ R ⟹ coset a ∈ quotient_set"
  unfolding coset_def quotient_set_def by (rule additive.Class_in_Partition)

lemma quotient_set_repr: "C ∈ quotient_set ⟹ ∃a∈R. C = coset a"
  unfolding coset_def quotient_set_def using additive.representant_exists by blast

text ‹Membership criterion: a coset is the zero coset iff its representative is in the ideal.›
lemma Class_eq_zero_iff:
  assumes "a ∈ R"
  shows "additive.Class a = additive.Class 𝟬 ⟷ a ∈ I"
proof -
  have "additive.Class a = additive.Class 𝟬 ⟷ (a, 𝟬) ∈ Ring_Congruence"
    using assms by (simp add: additive.Class_equivalence additive_congruence)
  also have "… ⟷ a ∈ I"
    using assms by (auto simp: Ring_Congruence_def)
  finally show ?thesis .
qed

end

text ‹An ideal of a commutative ring: add only the commutativity axiom on top of @{locale Ideal}
  (so the @{text Ring}/@{text multiplicative} structure is shared, avoiding a locale-merge clash).›
locale ideal_in_comm_ring = Ideal + commutative_ring
begin

lemmas comm = multiplicative.commutative

text ‹The quotient multiplication is commutative.›
lemma quot_mult_comm:
  assumes "a ∈ R" "b ∈ R"
  shows "additive.Class a [⋅] additive.Class b = additive.Class b [⋅] additive.Class a"
proof -
  have "additive.Class a [⋅] additive.Class b = additive.Class (a ⋅ b)"
    by (rule multiplicative.Class_commutes_with_composition[OF assms])
  also have "… = additive.Class (b ⋅ a)" using comm[OF assms] by simp
  also have "… = additive.Class b [⋅] additive.Class a"
    by (rule multiplicative.Class_commutes_with_composition[OF assms(2,1), symmetric])
  finally show ?thesis .
qed

text ‹Quotient multiplication in terms of representatives.›
lemma quot_mult_Class:
  assumes "a ∈ R" "b ∈ R"
  shows "additive.Class a [⋅] additive.Class b = additive.Class (a ⋅ b)"
  by (rule multiplicative.Class_commutes_with_composition[OF assms])

text ‹B1: the ideal is prime iff the quotient has no zero divisors (is an integral domain,
  given nontriviality @{term "I ≠ R"}).›
theorem prime_ideal_iff_quotient_no_zero_divisors:
  "prime_ideal ⟷ I ≠ R ∧
     (∀a∈R. ∀b∈R. additive.Class a [⋅] additive.Class b = additive.Class 𝟬
                  ⟶ additive.Class a = additive.Class 𝟬 ∨ additive.Class b = additive.Class 𝟬)"
proof -
  have "(∀a∈R. ∀b∈R. additive.Class a [⋅] additive.Class b = additive.Class 𝟬
                  ⟶ additive.Class a = additive.Class 𝟬 ∨ additive.Class b = additive.Class 𝟬)
      = (∀a∈R. ∀b∈R. a ⋅ b ∈ I ⟶ a ∈ I ∨ b ∈ I)"
  proof (intro ball_cong refl iff_allI)
    fix a b assume ab: "a ∈ R" "b ∈ R"
    have abR: "a ⋅ b ∈ R" using ab by simp
    show "(additive.Class a [⋅] additive.Class b = additive.Class 𝟬
            ⟶ additive.Class a = additive.Class 𝟬 ∨ additive.Class b = additive.Class 𝟬)
        = (a ⋅ b ∈ I ⟶ a ∈ I ∨ b ∈ I)"
      by (simp add: quot_mult_Class[OF ab] Class_eq_zero_iff abR Class_eq_zero_iff[OF ab(1)]
                    Class_eq_zero_iff[OF ab(2)])
  qed
  then show ?thesis unfolding prime_ideal_def by blast
qed

text ‹The ideal generated by @{term I} together with one element @{term a}, i.e. ‹I + (a)›.›
definition ext_ideal :: "'a ⇒ 'a set"
  where "ext_ideal a = {m + r ⋅ a | m r. m ∈ I ∧ r ∈ R}"

lemma ext_ideal_memI: "⟦ m ∈ I; r ∈ R ⟧ ⟹ m + r ⋅ a ∈ ext_ideal a"
  unfolding ext_ideal_def by blast

lemma ext_ideal_contains_I:
  assumes "a ∈ R"
  shows "I ⊆ ext_ideal a"
proof
  fix m assume m: "m ∈ I"
  then have mR: "m ∈ R" using additive.subset by blast
  have "m + 𝟬 ⋅ a = m" using assms mR by (simp add: additive.right_unit)
  moreover have "m + 𝟬 ⋅ a ∈ ext_ideal a" using m ext_ideal_memI[of m 𝟬] by simp
  ultimately show "m ∈ ext_ideal a" by simp
qed

lemma ext_ideal_contains_elt:
  assumes "a ∈ R"
  shows "a ∈ ext_ideal a"
proof -
  have "𝟬 + 𝟭 ⋅ a = a" using assms by (simp add: additive.left_unit)
  moreover have "𝟬 + 𝟭 ⋅ a ∈ ext_ideal a" using ext_ideal_memI[of 𝟬 𝟭] by simp
  ultimately show ?thesis by simp
qed

text ‹@{term "ext_ideal a"} is closed under addition and additive inverses, hence an additive
  subgroup of @{term R}.›
lemma ext_ideal_subgroup:
  assumes a: "a ∈ R"
  shows "Subgroup (ext_ideal a) R (+) 𝟬"
proof (rule additive.subgroupI)
  show "ext_ideal a ⊆ R"
  proof
    fix x assume "x ∈ ext_ideal a"
    then obtain m r where "m ∈ I" "r ∈ R" "x = m + r ⋅ a"
      unfolding ext_ideal_def by blast
    then show "x ∈ R" using a additive.subset by auto
  qed
next
  have "𝟬 ∈ I" by (rule additive.sub_unit_closed)
  then have "𝟬 + 𝟬 ⋅ a ∈ ext_ideal a" using a ext_ideal_memI[of 𝟬 𝟬] by blast
  moreover have "𝟬 + 𝟬 ⋅ a = 𝟬" using a by simp
  ultimately show "𝟬 ∈ ext_ideal a" by simp
next
  fix g h assume "g ∈ ext_ideal a" "h ∈ ext_ideal a"
  then obtain m1 r1 m2 r2 where
    g: "m1 ∈ I" "r1 ∈ R" "g = m1 + r1 ⋅ a" and
    h: "m2 ∈ I" "r2 ∈ R" "h = m2 + r2 ⋅ a"
    unfolding ext_ideal_def by blast
  have m1R: "m1 ∈ R" and m2R: "m2 ∈ R" using g h additive.subset by auto
  have ra1: "r1 ⋅ a ∈ R" and ra2: "r2 ⋅ a ∈ R" using g h a by auto
  ― ‹Rearrange @{text "(m1 + x) + (m2 + y) = (m1 + m2) + (x + y)"} in the abelian group.›
  have rearr: "(p + x) + (q + y) = (p + q) + (x + y)"
    if "p ∈ R" "x ∈ R" "q ∈ R" "y ∈ R" for p x q y
  proof -
    have "(p + x) + (q + y) = p + (x + (q + y))"
      using that by (simp add: additive.associative)
    also have "… = p + ((x + q) + y)"
      using that by (simp add: additive.associative)
    also have "… = p + ((q + x) + y)"
      using that by (simp add: additive.commutative)
    also have "… = p + (q + (x + y))"
      using that by (simp add: additive.associative)
    also have "… = (p + q) + (x + y)"
      using that by (simp add: additive.associative)
    finally show ?thesis .
  qed
  have "g + h = (m1 + r1 ⋅ a) + (m2 + r2 ⋅ a)" using g h by simp
  also have "… = (m1 + m2) + (r1 ⋅ a + r2 ⋅ a)"
    using rearr[OF m1R ra1 m2R ra2] .
  also have "… = (m1 + m2) + (r1 + r2) ⋅ a"
    using g h a by (simp add: distributive)
  finally have "g + h = (m1 + m2) + (r1 + r2) ⋅ a" .
  moreover have "m1 + m2 ∈ I" using g h by (simp add: additive.sub_composition_closed)
  ultimately show "g + h ∈ ext_ideal a" using g h ext_ideal_memI[of "m1+m2" "r1+r2"] by simp
next
  fix g assume "g ∈ ext_ideal a"
  then obtain m r where "m ∈ I" "r ∈ R" "g = m + r ⋅ a" unfolding ext_ideal_def by blast
  then have "g ∈ R" using a additive.subset by auto
  then show "additive.invertible g" by simp
next
  fix g assume "g ∈ ext_ideal a"
  then obtain m r where g: "m ∈ I" "r ∈ R" "g = m + r ⋅ a"
    unfolding ext_ideal_def by blast
  have mR: "m ∈ R" using g additive.subset by auto
  have "additive.inverse g = (additive.inverse m) + (additive.inverse r) ⋅ a"
    using g mR a by (simp add: additive.inverse_composition_commute additive.commutative left_minus)
  moreover have "additive.inverse m ∈ I" using g by simp
  moreover have "additive.inverse r ∈ R" using g by simp
  ultimately show "additive.inverse g ∈ ext_ideal a"
    using ext_ideal_memI[of "additive.inverse m" "additive.inverse r"] by simp
qed

text ‹Hence @{term "ext_ideal a"} is an ideal of @{term R}: the absorption laws follow from
  @{term I}'s absorption and commutativity of multiplication.›
lemma ext_ideal_is_ideal:
  assumes a: "a ∈ R"
  shows "Ideal (ext_ideal a) R (+) (⋅) 𝟬 𝟭"
proof -
  interpret sub: Subgroup "ext_ideal a" R "(+)" 𝟬 by (rule ext_ideal_subgroup[OF a])
  show ?thesis
  proof (unfold_locales)
    fix x y assume x: "x ∈ R" and y: "y ∈ ext_ideal a"
    obtain m r where mr: "m ∈ I" "r ∈ R" "y = m + r ⋅ a"
      using y unfolding ext_ideal_def by blast
    have mR: "m ∈ R" using mr additive.subset by auto
    show "x ⋅ y ∈ ext_ideal a"
    proof -
      have "x ⋅ y = x ⋅ m + (x ⋅ r) ⋅ a"
        using x mr mR a by (simp add: distributive multiplicative.associative)
      moreover have "x ⋅ m ∈ I" using x mr by (simp add: Ideal)
      moreover have "x ⋅ r ∈ R" using x mr by simp
      ultimately show ?thesis using ext_ideal_memI[of "x ⋅ m" "x ⋅ r"] by simp
    qed
    show "y ⋅ x ∈ ext_ideal a"
    proof -
      have rax: "(r ⋅ a) ⋅ x = (r ⋅ x) ⋅ a"
      proof -
        have "(r ⋅ a) ⋅ x = r ⋅ (a ⋅ x)" using mr a x by (simp add: multiplicative.associative)
        also have "… = r ⋅ (x ⋅ a)" using a x by (simp add: comm)
        also have "… = (r ⋅ x) ⋅ a" using mr a x by (simp add: multiplicative.associative)
        finally show ?thesis .
      qed
      have "y ⋅ x = m ⋅ x + (r ⋅ a) ⋅ x"
        using x mr mR a by (simp add: distributive)
      also have "… = m ⋅ x + (r ⋅ x) ⋅ a" using rax by simp
      finally have "y ⋅ x = m ⋅ x + (r ⋅ x) ⋅ a" .
      moreover have "m ⋅ x ∈ I" using x mr by (simp add: Ideal)
      moreover have "r ⋅ x ∈ R" using x mr by simp
      ultimately show ?thesis using ext_ideal_memI[of "m ⋅ x" "r ⋅ x"] by simp
    qed
  qed
qed


text ‹For a maximal ideal, any element outside @{term I} generates (with @{term I}) the whole
  ring, giving a representation @{text "𝟭 = m + r ⋅ a"} with @{term "m ∈ I"}.›
lemma maximal_ext_ideal_eq_whole:
  assumes max: maximal_ideal and a: "a ∈ R" and aI: "a ∉ I"
  shows "ext_ideal a = R"
proof -
  have "Ideal (ext_ideal a) R (+) (⋅) 𝟬 𝟭" by (rule ext_ideal_is_ideal[OF a])
  moreover have "I ⊆ ext_ideal a" by (rule ext_ideal_contains_I[OF a])
  moreover have "ext_ideal a ≠ I"
    using ext_ideal_contains_elt[OF a] aI by blast
  ultimately show ?thesis using max unfolding maximal_ideal_def by blast
qed

text ‹∗‹A maximal ideal is prime.›  If ‹a ⋅ b ∈ I› but ‹a ∉ I›, then adjoining @{term a}
  generates the whole ring, giving ‹𝟭 = m + r ⋅ a› with ‹m ∈ I›; hence
  ‹b = m ⋅ b + r ⋅ (a ⋅ b) ∈ I›.›
theorem maximal_imp_prime_ideal:
  assumes max: maximal_ideal shows "prime_ideal"
proof (unfold prime_ideal_def, intro conjI ballI impI)
  show "I ≠ R" using max unfolding maximal_ideal_def by simp
next
  fix a b assume a: "a ∈ R" and b: "b ∈ R" and abI: "a ⋅ b ∈ I"
  show "a ∈ I ∨ b ∈ I"
  proof (cases "a ∈ I")
    case True then show ?thesis ..
  next
    case False
    ― ‹@{term a} generates the whole ring together with @{term I}: @{text "𝟭 = m + r ⋅ a"}.›
    have "𝟭 ∈ ext_ideal a" using maximal_ext_ideal_eq_whole[OF max a False] by simp
    then obtain m r where m: "m ∈ I" and r: "r ∈ R" and one: "𝟭 = m + r ⋅ a"
      unfolding ext_ideal_def by blast
    have mR: "m ∈ R" using m additive.subset by auto
    ― ‹Then @{term "b = m ⋅ b + r ⋅ (a ⋅ b)"}, both summands in @{term I}.›
    have "b = 𝟭 ⋅ b" using b by simp
    also have "… = (m + r ⋅ a) ⋅ b" using one by simp
    also have "… = m ⋅ b + (r ⋅ a) ⋅ b" using mR r a b by (simp add: distributive)
    also have "(r ⋅ a) ⋅ b = r ⋅ (a ⋅ b)" using r a b by (simp add: multiplicative.associative)
    finally have beq: "b = m ⋅ b + r ⋅ (a ⋅ b)" .
    have "m ⋅ b ∈ I" using Ideal(2)[OF b m] .
    moreover have "r ⋅ (a ⋅ b) ∈ I" using Ideal(1)[OF r abI] .
    ultimately have "m ⋅ b + r ⋅ (a ⋅ b) ∈ I" by (rule additive.sub_composition_closed)
    then have "b ∈ I" using beq by simp
    then show ?thesis ..
  qed
qed

lemma maximal_quotient_invertible:
  assumes max: maximal_ideal and a: "a ∈ R" and aI: "a ∉ I"
  shows "∃r∈R. additive.Class r [⋅] additive.Class a = additive.Class 𝟭"
proof -
  have "𝟭 ∈ ext_ideal a" using maximal_ext_ideal_eq_whole[OF max a aI] by simp
  then obtain m r where m: "m ∈ I" and r: "r ∈ R" and one: "𝟭 = m + r ⋅ a"
    unfolding ext_ideal_def by blast
  have mR: "m ∈ R" using m additive.subset by auto
  have raR: "r ⋅ a ∈ R" using r a by simp
  have "additive.Class 𝟭 = additive.Class (m + r ⋅ a)" using one by simp
  also have "… = additive.Class m [+] additive.Class (r ⋅ a)"
    using mR raR by (simp add: additive.Class_commutes_with_composition)
  also have "additive.Class m = additive.Class 𝟬" using m by (simp add: Class_eq_zero_iff mR)
  finally have "additive.Class 𝟭 = additive.Class 𝟬 [+] additive.Class (r ⋅ a)" .
  also have "… = additive.Class (r ⋅ a)"
    using raR by (simp add: additive.Class_commutes_with_composition[symmetric] additive.left_unit)
  also have "additive.Class (r ⋅ a) = additive.Class r [⋅] additive.Class a"
    using r a by (simp add: quot_mult_Class)
  finally have "additive.Class 𝟭 = additive.Class r [⋅] additive.Class a" .
  then show ?thesis using r by auto
qed


text ‹If two ring elements have equal cosets, their difference lies in @{term I}.›
lemma Class_eq_imp_diff_in_I:
  assumes "a ∈ R" "b ∈ R" "additive.Class a = additive.Class b"
  shows "a - b ∈ I"
proof -
  have "(a, b) ∈ Ring_Congruence"
    using assms by (simp add: additive.Class_equivalence additive_congruence)
  then show ?thesis by (rule Ring_CongruenceD)
qed

theorem maximal_ideal_iff_quotient_field:
  "maximal_ideal ⟷ I ≠ R ∧
     (∀a∈R. additive.Class a ≠ additive.Class 𝟬
            ⟶ (∃r∈R. additive.Class r [⋅] additive.Class a = additive.Class 𝟭))"
proof
  assume max: maximal_ideal
  have "I ≠ R" using max unfolding maximal_ideal_def by simp
  moreover have "∃r∈R. additive.Class r [⋅] additive.Class a = additive.Class 𝟭"
    if aR: "a ∈ R" and ane: "additive.Class a ≠ additive.Class 𝟬" for a
  proof -
    have "a ∉ I" using aR ane by (simp add: Class_eq_zero_iff)
    then show ?thesis by (rule maximal_quotient_invertible[OF max aR])
  qed
  ultimately show "I ≠ R ∧
     (∀a∈R. additive.Class a ≠ additive.Class 𝟬
            ⟶ (∃r∈R. additive.Class r [⋅] additive.Class a = additive.Class 𝟭))" by blast
next
  assume rhs: "I ≠ R ∧
     (∀a∈R. additive.Class a ≠ additive.Class 𝟬
            ⟶ (∃r∈R. additive.Class r [⋅] additive.Class a = additive.Class 𝟭))"
  show maximal_ideal
    unfolding maximal_ideal_def
  proof (intro conjI allI impI)
    show "I ≠ R" using rhs by simp
    fix J assume J: "Ideal J R (+) (⋅) 𝟬 𝟭" and IJ: "I ⊆ J"
    show "J = I ∨ J = R"
    proof (rule ccontr)
      assume "¬ (J = I ∨ J = R)"
      then have JnI: "J ≠ I" and JnR: "J ≠ R" by auto
      interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule J)
      from JnI IJ obtain a where aJ: "a ∈ J" and aI: "a ∉ I" by blast
      have aR: "a ∈ R" using aJ J.additive.subset by auto
      have ane: "additive.Class a ≠ additive.Class 𝟬" using aR aI by (simp add: Class_eq_zero_iff)
      then obtain r where r: "r ∈ R" and inv: "additive.Class r [⋅] additive.Class a = additive.Class 𝟭"
        using rhs aR by blast
      have raJ: "r ⋅ a ∈ J" using r aJ by (simp add: J.Ideal)
      have raR: "r ⋅ a ∈ R" using r aR by simp
      have ClassEq: "additive.Class (r ⋅ a) = additive.Class 𝟭"
        using r aR inv by (simp add: quot_mult_Class)
      ― ‹So @{text "r⋅a - 𝟭 ∈ I"}, hence @{text "𝟭 - r⋅a ∈ I ⊆ J"}, giving @{text "𝟭 ∈ J"}.›
      have "r ⋅ a - 𝟭 ∈ I" using Class_eq_imp_diff_in_I[OF raR _ ClassEq] by simp
      then have negI: "- (r ⋅ a - 𝟭) ∈ I" by simp
      have "- (r ⋅ a - 𝟭) = 𝟭 - r ⋅ a"
        using raR by (simp add: additive.inverse_composition_commute additive.commutative)
      then have oneI: "𝟭 - r ⋅ a ∈ I" using negI by simp
      have oneJ: "𝟭 - r ⋅ a ∈ J" using oneI IJ by blast
      have "(𝟭 - r ⋅ a) + r ⋅ a ∈ J" using oneJ raJ by (simp add: J.additive.sub_composition_closed)
      moreover have "(𝟭 - r ⋅ a) + r ⋅ a = 𝟭"
      proof -
        have "(𝟭 - r ⋅ a) + r ⋅ a = 𝟭 + ((- r ⋅ a) + r ⋅ a)"
          using raR by (simp add: additive.associative)
        also have "… = 𝟭" using raR by simp
        finally show ?thesis .
      qed
      ultimately have "𝟭 ∈ J" by simp
      then have "J = R" using J.additive.subset
        by (metis J.Ideal(1) multiplicative.right_unit subsetI subset_antisym)
      then show False using JnR by simp
    qed
  qed
qed

end


section ‹Principal Ideals›

text ‹The principal ideal generated by a single element of a commutative ring: the set of all
  multiples @{text "r ⋅ a"}.  This is the smallest ideal containing @{term a}, and it is the
  building block for principal ideal domains (e.g. @{text "F[X]"} over a field).›

subsection ‹Existence of maximal ideals›

text ‹Every proper ideal is contained in a maximal one.  This is the standard application of
  Zorn's lemma (@{thm [source] Zorn_Lemma2}) to the family of proper ideals containing a given one:
  the union of a chain of such ideals is again one, so the family has a maximal element.

  The only delicate point is ∗‹properness› of the union.  An ideal is proper exactly when it omits
  the unit ‹𝟭›: if ‹𝟭› lies in an ideal then so does ‹a ⋅ 𝟭 = a› for every ‹a›, making it the
  whole ring.  Since every member of the chain omits ‹𝟭›, so does the union --- which is why the
  chain condition can be checked at all, and why the argument needs a ring with a unit.›

context Ring
begin

text ‹An ideal is proper if and only if it does not contain @{term 𝟭}.›
lemma ideal_proper_iff_one_notin:
  assumes I: "Ideal I R (+) (⋅) 𝟬 𝟭"
  shows "I ≠ R ⟷ 𝟭 ∉ I"
proof -
  interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
  show ?thesis
  proof
    assume "I ≠ R"
    show "𝟭 ∉ I"
    proof
      assume one: "𝟭 ∈ I"
      have "R ⊆ I"
      proof
        fix a assume a: "a ∈ R"
        have "a ⋅ 𝟭 ∈ I" using a one by (rule I.Ideal(1))
        then show "a ∈ I" using a by simp
      qed
      with I.additive.subset have "I = R" by blast
      with ‹I ≠ R› show False by simp
    qed
  next
    assume "𝟭 ∉ I"
    then show "I ≠ R" using multiplicative.unit_closed by blast
  qed
qed

text ‹The union of a nonempty chain of ideals is an ideal.  Directedness is what makes the additive
  closure work: two elements of the union lie in a common member of the chain.›
lemma ideal_Union_chain:
  assumes ne: "𝒞 ≠ {}"
    and id: "⋀I. I ∈ 𝒞 ⟹ Ideal I R (+) (⋅) 𝟬 𝟭"
    and chain: "⋀I J. ⟦ I ∈ 𝒞; J ∈ 𝒞 ⟧ ⟹ I ⊆ J ∨ J ⊆ I"
  shows "Ideal (⋃ 𝒞) R (+) (⋅) 𝟬 𝟭"
proof -
  obtain I0 where I0: "I0 ∈ 𝒞" using ne by blast
  interpret I0: Ideal I0 R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF I0])
  have sub: "⋃ 𝒞 ⊆ R"
  proof
    fix x assume "x ∈ ⋃ 𝒞"
    then obtain I where I: "I ∈ 𝒞" and x: "x ∈ I" by blast
    interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF I])
    show "x ∈ R" using x I.additive.subset by blast
  qed
  have sg: "Subgroup (⋃ 𝒞) R (+) 𝟬"
  proof (rule additive.subgroupI)
    show "⋃ 𝒞 ⊆ R" by (rule sub)
    show "𝟬 ∈ ⋃ 𝒞" using I0 I0.additive.sub_unit_closed by blast
  next
    ― ‹Directedness: pick the larger of the two members containing @{term g} and @{term h}.›
    fix g h assume "g ∈ ⋃ 𝒞" and "h ∈ ⋃ 𝒞"
    then obtain I J where I: "I ∈ 𝒞" "g ∈ I" and J: "J ∈ 𝒞" "h ∈ J" by blast
    show "g + h ∈ ⋃ 𝒞"
    proof (cases "I ⊆ J")
      case True
      interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF J(1)])
      have "g + h ∈ J" using True I(2) J(2) by (blast intro: J.additive.sub_composition_closed)
      then show ?thesis using J(1) by blast
    next
      case False
      then have "J ⊆ I" using chain[OF I(1) J(1)] by blast
      interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF I(1)])
      have "g + h ∈ I" using ‹J ⊆ I› I(2) J(2) by (blast intro: I.additive.sub_composition_closed)
      then show ?thesis using I(1) by blast
    qed
  next
    fix g assume "g ∈ ⋃ 𝒞"
    then show "additive.invertible g" using sub by blast
  next
    fix g assume "g ∈ ⋃ 𝒞"
    then obtain I where I: "I ∈ 𝒞" and g: "g ∈ I" by blast
    interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF I])
    have "additive.inverse g ∈ I"
      using g I.additive.submonoid_inverse_closed I.additive.sub.invertible by blast
    then show "additive.inverse g ∈ ⋃ 𝒞" using I by blast
  qed
  interpret S: Subgroup "⋃ 𝒞" R "(+)" 𝟬 by (rule sg)
  show ?thesis
  proof unfold_locales
    fix a b assume a: "a ∈ R" and b: "b ∈ ⋃ 𝒞"
    from b obtain I where I: "I ∈ 𝒞" and bI: "b ∈ I" by blast
    interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule id[OF I])
    show "a ⋅ b ∈ ⋃ 𝒞" using I a bI by (blast intro: I.Ideal(1))
    show "b ⋅ a ∈ ⋃ 𝒞" using I a bI by (blast intro: I.Ideal(2))
  qed
qed

text ‹∗‹Krull's theorem.›  Every proper ideal extends to a maximal one.  Apply
  @{thm [source] Zorn_Lemma2} to the family of proper ideals containing @{term I}: a nonempty chain's
  union is an ideal by @{thm [source] ideal_Union_chain}, is proper because no member contains ‹𝟭›,
  and contains @{term I}; the empty chain is bounded by @{term I} itself.›
theorem maximal_ideal_exists:
  assumes I: "Ideal I R (+) (⋅) 𝟬 𝟭" and proper: "I ≠ R"
  shows "∃M. Ideal M R (+) (⋅) 𝟬 𝟭 ∧ I ⊆ M ∧ Ideal.maximal_ideal M R (+) (⋅) 𝟬 𝟭"
proof -
  interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
  have Ione: "𝟭 ∉ I" using I proper by (simp add: ideal_proper_iff_one_notin)
  ― ‹The family: proper ideals containing @{term I}.›
  define 𝒜 where "𝒜 = {J. Ideal J R (+) (⋅) 𝟬 𝟭 ∧ I ⊆ J ∧ 𝟭 ∉ J}"
  have IA: "I ∈ 𝒜" unfolding 𝒜_def using I Ione by blast
  ― ‹Every chain in the family has an upper bound ∗‹in› the family.  We use
    @{thm [source] Zorn_Lemma2} rather than @{thm [source] Zorn_Lemma} precisely because of the empty
    chain: the latter would demand ‹⋃ {} = {} ∈ 𝒜›, which is false, whereas an upper bound for the
    empty chain is supplied by @{term I} itself.›
  have bound: "∃U ∈ 𝒜. ∀X ∈ 𝒞. X ⊆ U" if C: "𝒞 ∈ chains 𝒜" for 𝒞
  proof (cases "𝒞 = {}")
    case True
    then show ?thesis using IA by blast
  next
    case False
    have sub: "𝒞 ⊆ 𝒜" and ch: "chain⇩⊆ 𝒞" using C by (auto simp: chains_def)
    have id: "⋀J. J ∈ 𝒞 ⟹ Ideal J R (+) (⋅) 𝟬 𝟭" using sub by (auto simp: 𝒜_def)
    have le: "⋀J K. ⟦ J ∈ 𝒞; K ∈ 𝒞 ⟧ ⟹ J ⊆ K ∨ K ⊆ J"
      using ch by (auto simp: chain_subset_def)
    have "Ideal (⋃ 𝒞) R (+) (⋅) 𝟬 𝟭" using False id le by (rule ideal_Union_chain)
    moreover have "I ⊆ ⋃ 𝒞" using False sub by (auto simp: 𝒜_def)
    moreover have "𝟭 ∉ ⋃ 𝒞" using sub by (auto simp: 𝒜_def)
    ultimately have "⋃ 𝒞 ∈ 𝒜" unfolding 𝒜_def by blast
    then show ?thesis by blast
  qed
  ― ‹Zorn gives a maximal member of the family; maximality ∗‹among proper ideals over› @{term I}
    upgrades to maximality among all ideals, since a strictly larger ideal either contains ‹𝟭› ---
    hence is @{term R} --- or would still be in the family.›
  ― ‹Zorn's premise is discharged as an explicit @{text ∀}-statement first: handed to
    @{method blast} as the conditional rule @{text bound}, the set-valued unknown sends it into a
    search that does not terminate.›
  have prem: "∀𝒞 ∈ chains 𝒜. ∃U ∈ 𝒜. ∀X ∈ 𝒞. X ⊆ U" using bound by blast
  obtain M where M: "M ∈ 𝒜" and max: "⋀X. X ∈ 𝒜 ⟹ M ⊆ X ⟹ X = M"
    using Zorn_Lemma2[OF prem] by blast
  from M have Mid: "Ideal M R (+) (⋅) 𝟬 𝟭" and IM: "I ⊆ M" and Mone: "𝟭 ∉ M"
    by (auto simp: 𝒜_def)
  interpret M: Ideal M R "(+)" "(⋅)" 𝟬 𝟭 by (rule Mid)
  have "Ideal.maximal_ideal M R (+) (⋅) 𝟬 𝟭"
    unfolding M.maximal_ideal_def
  proof (intro conjI allI impI)
    show "M ≠ R" using Mid Mone by (simp add: ideal_proper_iff_one_notin)
    fix J assume J: "Ideal J R (+) (⋅) 𝟬 𝟭" and MJ: "M ⊆ J"
    show "J = M ∨ J = R"
    proof (cases "𝟭 ∈ J")
        case True
      ― ‹@{text ideal_proper_iff_one_notin} read contrapositively: containing ‹𝟭› forces ‹J = R›.›
      then have "J = R" using ideal_proper_iff_one_notin[OF J] by blast
      then show ?thesis by simp
    next
      case False
      then have "J ∈ 𝒜" unfolding 𝒜_def using J IM MJ by blast
      then show ?thesis using max MJ by blast
    qed
  qed
  then show ?thesis using Mid IM by blast
qed


end (* Ring *)


context commutative_ring
begin

definition principal_ideal :: "'a ⇒ 'a set"
  where "principal_ideal a = {r ⋅ a | r. r ∈ R}"

lemma principal_ideal_memI: "r ∈ R ⟹ r ⋅ a ∈ principal_ideal a"
  unfolding principal_ideal_def by blast

lemma principal_ideal_subset:
  assumes "a ∈ R" shows "principal_ideal a ⊆ R"
proof
  fix x assume "x ∈ principal_ideal a"
  then obtain r where "r ∈ R" "x = r ⋅ a" unfolding principal_ideal_def by blast
  then show "x ∈ R" using assms by auto
qed

text ‹@{term a} itself lies in @{term "principal_ideal a"} (take @{text "r = 𝟭"}).›
lemma principal_ideal_contains:
  assumes "a ∈ R" shows "a ∈ principal_ideal a"
proof -
  have "𝟭 ⋅ a = a" using assms by simp
  moreover have "𝟭 ⋅ a ∈ principal_ideal a" using principal_ideal_memI[of 𝟭 a] by simp
  ultimately show ?thesis by simp
qed

text ‹@{term "principal_ideal a"} is an additive subgroup: closed under @{text "+"} via
  distributivity, and under inverses via @{thm [source] left_minus}.›
lemma principal_ideal_subgroup:
  assumes a: "a ∈ R" shows "Subgroup (principal_ideal a) R (+) 𝟬"
proof (rule additive.subgroupI)
  show "principal_ideal a ⊆ R" using a by (rule principal_ideal_subset)
next
  have "𝟬 ⋅ a = 𝟬" using a by simp
  moreover have "𝟬 ⋅ a ∈ principal_ideal a" using principal_ideal_memI[of 𝟬 a] by simp
  ultimately show "𝟬 ∈ principal_ideal a" by simp
next
  fix g h assume "g ∈ principal_ideal a" "h ∈ principal_ideal a"
  then obtain r1 r2 where g: "r1 ∈ R" "g = r1 ⋅ a" and h: "r2 ∈ R" "h = r2 ⋅ a"
    unfolding principal_ideal_def by blast
  have "g + h = r1 ⋅ a + r2 ⋅ a" using g h by simp
  also have "… = (r1 + r2) ⋅ a" using g h a by (simp add: distributive)
  finally have "g + h = (r1 + r2) ⋅ a" .
  moreover have "r1 + r2 ∈ R" using g h by simp
  ultimately show "g + h ∈ principal_ideal a" using principal_ideal_memI[of "r1 + r2" a] by simp
next
  fix g assume "g ∈ principal_ideal a"
  then obtain r where "r ∈ R" "g = r ⋅ a" unfolding principal_ideal_def by blast
  then have "g ∈ R" using a by auto
  then show "additive.invertible g" by simp
next
  fix g assume "g ∈ principal_ideal a"
  then obtain r where g: "r ∈ R" "g = r ⋅ a" unfolding principal_ideal_def by blast
  have "additive.inverse g = (additive.inverse r) ⋅ a" using g a by (simp add: left_minus)
  moreover have "additive.inverse r ∈ R" using g by simp
  ultimately show "additive.inverse g ∈ principal_ideal a"
    using principal_ideal_memI[of "additive.inverse r" a] by simp
qed

text ‹Hence @{term "principal_ideal a"} is an ideal: the absorption laws follow from
  associativity and commutativity of multiplication.›
lemma principal_ideal_is_ideal:
  assumes a: "a ∈ R" shows "Ideal (principal_ideal a) R (+) (⋅) 𝟬 𝟭"
proof -
  interpret sub: Subgroup "principal_ideal a" R "(+)" 𝟬 by (rule principal_ideal_subgroup[OF a])
  show ?thesis
  proof unfold_locales
    fix x y assume x: "x ∈ R" and y: "y ∈ principal_ideal a"
    obtain r where r: "r ∈ R" "y = r ⋅ a" using y unfolding principal_ideal_def by blast
    have yR: "y ∈ R" using r a by simp
    show "x ⋅ y ∈ principal_ideal a"
    proof -
      have "x ⋅ y = (x ⋅ r) ⋅ a" using x r a by (simp add: multiplicative.associative)
      moreover have "x ⋅ r ∈ R" using x r by simp
      ultimately show ?thesis using principal_ideal_memI[of "x ⋅ r" a] by simp
    qed
    show "y ⋅ x ∈ principal_ideal a"
    proof -
      have "y ⋅ x = x ⋅ y" using multiplicative.commutative[OF yR x] .
      also have "… = (x ⋅ r) ⋅ a" using x r a by (simp add: multiplicative.associative)
      finally have "y ⋅ x = (x ⋅ r) ⋅ a" .
      moreover have "x ⋅ r ∈ R" using x r by simp
      ultimately show ?thesis using principal_ideal_memI[of "x ⋅ r" a] by simp
    qed
  qed
qed

end

end