Table of Contents

• Rings and Ideals
  • Special Elements of Ring
    • Facts on Special Elements of Ring
    • Domain VS Field
  • Ideal
    • Definitions of Some Ideals
    • Special Ring
    • Facts on Ideals
  • Ideal Operations
    • Facts on Ideal Operations
    • Properties of the Radical
  • Maximal Ideal
    • Zorn's Lemma
    • Facts on Maximal Ideal
  • Other Special Ideals
    • Facts on Special Ideals
    • Krull Dimension
  • Homomorphisms and Quotient Rings
    • Definition of Quotient Ring
    • Ring Homomorphism
    • Ring Homomorphism Theorems
    • Special Ideals
    • Prime Avoidance Lemma

Note that all rings considered here are commutative and have a multiplicative identity.

Each written proof or proof sketch is followed by a separate folded Lean 4 proof. The snippets are collected and compiled in mathlib-in-lean/commutative-algebra/Ring.lean. They assume that file's imports, namespace CommAlg, and variable {A : Type*} [CommRing A]; later snippets may use earlier declarations.

Rings and Ideals

Special Elements of Ring

1. A set of units, $A^{\ast }=\{a\in A\mid \mathrm{\exists }b\in A,a\cdot b=1\}$

2. A set of zero divisors, $\mathcal{D}(A)=\{a\in A\mid \mathrm{\exists }b\in A\setminus \{0\},a\cdot b=0\}$

3. A set of nilpotent elements, $\mathcal{N}(A)=\{a\in A\mid \mathrm{\exists }n\in \mathbb{N},a^n=0\}$

4. $a$ is idempotent if $a^2=a$

Facts on Special Elements of Ring

1. If $A\ne 0$, then $\mathcal{N}(A)\subseteq \mathcal{D}(A)$, i.e., every nilpotent element is a zero divisor.

   Proof

   It is suffice to show that $\mathrm{\forall }y\in \mathcal{N}(A)\to y\in \mathcal{D}(A)$.

   By definition (3), choose the least $n\in \mathbb{N}$ such that $y^n=0$. Since $y^0=1\ne 0$, we have $n\ge 1$, so $0=y^n=y\cdot y^{n-1}$. By minimality of $n$, $y^{n-1}\ne 0$. By definition (2), use $b=y^{n-1}$, we have $y\cdot b=0$ with $b\ne 0$, hence $y\in \mathcal{D}(A)$.

   Lean 4 proof

   /-- `a` is a zero divisor if `a * b = 0` for some nonzero `b`. -/
   def IsZeroDivisor (a : A) : Prop := ∃ b : A, b ≠ 0 ∧ a * b = 0
   
   /- Fact 1: in a nonzero ring, every nilpotent element is a zero divisor. -/
   theorem isZeroDivisor_of_isNilpotent [Nontrivial A] {y : A} (hy : IsNilpotent y) :
       IsZeroDivisor y := by
     classical
     -- choose the least `n` with `y ^ n = 0`
     set n := Nat.find hy with hn_def
     have hn : y ^ n = 0 := Nat.find_spec hy
     -- `n ≠ 0`, since `y ^ 0 = 1 ≠ 0`
     have hn0 : n ≠ 0 := by
       intro h
       rw [h, pow_zero] at hn
       exact one_ne_zero hn
     obtain ⟨m, hm⟩ := Nat.exists_eq_succ_of_ne_zero hn0
     -- take `b = y ^ (n - 1)`, which is nonzero by minimality of `n`
     refine ⟨y ^ m, fun h => ?_, ?_⟩
     · have : n ≤ m := Nat.find_min' hy h
       omega
     · calc y * y ^ m = y ^ (m + 1) := (pow_succ' y m).symm
         _ = y ^ n := by rw [hm]
         _ = 0 := hn

   
   

2. If $A\ne 0$, then $A^{\ast }\cap \mathcal{D}(A)=\mathrm{\varnothing }$, i.e., no unit is a zero divisor.

   Proof

   By contradiction, assume $A^{\ast }\cap \mathcal{D}(A)\ne \mathrm{\varnothing }$, let $x\in A^{\ast }\cap \mathcal{D}(A)$.

   By definition (1), there exists $y\in A$ such that $x\cdot y=1$. By definition (2), there exists an non-zero $z\in A$ such that $x\cdot z=0$.

   So, we have :

   $$(x\cdot y)\cdot z=1\cdot z=z\ne 0$$

   By the associativity and commutativity of $A$ (as we mentioned earlier that $A$ is commutative ring with identity), the left-hand side $(x\cdot y)\cdot z=(y\cdot x)\cdot z=y\cdot (x\cdot z)=y\cdot 0=0$.

   This is a contradiction since the right-hand side is $z\ne 0$. Hence no unit can be a zero divisor.

   Lean 4 proof

   /- Fact 2: no unit is a zero divisor. -/
   theorem not_isZeroDivisor_of_isUnit {x : A} (hx : IsUnit x) : ¬ IsZeroDivisor x := by
     rintro ⟨z, hz, hxz⟩
     obtain ⟨y, hy⟩ := hx.exists_right_inv
     -- `z = (x * y) * z = y * (x * z) = y * 0 = 0`, contradicting `z ≠ 0`
     apply hz
     calc z = (x * y) * z := by rw [hy, one_mul]
       _ = y * (x * z) := by ring
       _ = 0 := by rw [hxz, mul_zero]
   
   example {x z : A} (hx : IsUnit x) : x * z = 0 ↔ z = 0 := hx.mul_right_eq_zero

   
   

3. Let $A$ be a finite ring. Then, $A=A^{\ast }\cup \mathcal{D}(A)$, i.e., every element of a finite ring is either a unit or a zero divisor.

   Proof

   Firstly, considering $A=\{0\}$, then $0\cdot 0=0=1$, so $A^{\ast }=\{0\}$ and $\mathcal{D}(A)=\mathrm{\varnothing }$. Hence, $A=A^{\ast }\cup \mathcal{D}(A)$ in this case.

   Secondly, if $A\ne \{0\}$. By (b), we have $A^{\ast }\cap \mathcal{D}(A)=\mathrm{\varnothing }$. Since $A^{\ast }\subseteq A$ and $\mathcal{D}(A)\subseteq A$, we have $A^{\ast }\cup \mathcal{D}(A)\subseteq A$. So it is suffice to show that $A\subseteq A^{\ast }\cup \mathcal{D}(A)$, which implies that

   $$\mathrm{\forall }x\in A\to x\in A^{\ast }\cup \mathcal{D}(A)$$

   Assume $x\in A$. Consider the function $f:A\to A$ defined by $f(y)=x\cdot y$. Since $A$ is finite, $f$ is either injective or not.

   • If $f$ is not injective, then there exist distinct $y_1,y_2\in A$ such that $x\cdot y_1=x\cdot y_2$, which implies $x\cdot (y_1-y_2)=0$. Let $z=y_1-y_2\ne 0$, then $x\cdot z=0$, hence $x\in \mathcal{D}(A)$.

   • If $f$ is injective, since $A$ is finite, by the pigeonhole principle, $f$ is also surjective, then there exists $y\in A$ such that $f(y)=x\cdot y=1$, hence $x\in A^{\ast }$.

   Therefore, every element $x\in A$ is either a unit or a zero divisor, i.e., $x\in A^{\ast }\cup \mathcal{D}(A)$.

   Lean 4 proof

   /- Fact 3: every element of a finite ring is a unit or a zero divisor. -/
   theorem isUnit_or_isZeroDivisor [Finite A] (x : A) : IsUnit x ∨ IsZeroDivisor x := by
     -- consider `f : A → A`, `f y = x * y`
     by_cases hinj : Function.Injective (fun y : A => x * y)
     · -- injective ⇒ surjective (pigeonhole), so `x * y = 1` for some `y`
       left
       obtain ⟨y, hy⟩ := Finite.injective_iff_surjective.mp hinj 1
       exact IsUnit.of_mul_eq_one y hy
     · -- not injective ⇒ `x * (y₁ - y₂) = 0` with `y₁ ≠ y₂`
       right
       simp only [Function.Injective, not_forall] at hinj
       obtain ⟨y₁, y₂, h, hne⟩ := hinj
       exact ⟨y₁ - y₂, sub_ne_zero.mpr hne, by rw [mul_sub, h, sub_self]⟩

   
   

Domain VS Field

1. Commutative ring + (multiplicative) identity + $\mathcal{D}(A)=0$ is an integeral domain (or domain)

2. Commutative ring + (multiplicative) identity + $A^{\ast }=A\setminus \{0\}$ is a field.

3. A finite (integral) domain is a field.

   Proof

   By the proof of fact (3), $\mathcal{D}(A)=0$ implies function $f$ is injective for every non-zero $x\in A$.

   By pigeonhole principle, finite implies that every injective function from the domain to itself is also surjective, which ensures that every non-zero element has a multiplicative inverse, hence the domain is a field.

   Lean 4 proof

   /- Fact 3: a finite integral domain is a field. -/
   theorem isField_of_finite_domain [IsDomain A] [Finite A] : IsField A := by
     refine ⟨exists_pair_ne A, mul_comm, ?_⟩
     intro x hx
     -- no zero divisors ⇒ `y ↦ x * y` is injective, hence surjective
     have hinj : Function.Injective (fun y : A => x * y) :=
       fun y₁ y₂ h => mul_left_cancel₀ hx h
     exact Finite.injective_iff_surjective.mp hinj 1
   
   example [IsDomain A] [Finite A] : IsField A := Finite.isField_of_domain A

   
   

Ideal

Ideal is a subset of a ring such that

1. It is an additive subgroup of the ring. i.e. for any $a,b\in I$, we have $a-b\in I$
2. It is closed under multiplication by any element of the ring, i.e., for all $a\in A$ and $x\in I$, we have $a\cdot x\in I$.

Definitions of Some Ideals

1. If an ideal $I$ is proper, then $1\notin I$.

2. If a proper ideal $I$ is maximal if it is not strictly contained in any other proper ideal of the ring.

3. Ideal generated by a strict subset $S\subset A$ is

   $$⟨S⟩=\{\sum _{i=1}^n{a}_i\cdot s_i\mid n\in \mathbb{N},a_i\in A,s_i\in S\},$$

   the elements of $S$ are generators of ideal $I=⟨S⟩$. Since cardinality $|S|=n\in \mathbb{N}$ is a finite number, the ideal $I$ is finitely generated. Let $S=\{s_1,...,s_n\}$, then $I=⟨s_1,...,s_n⟩$.

4. If the cardinality of $S$ is 1, i.e., $S=\{s\}$, then the ideal $I$ generated by $S$ is principal, i.e., $I=⟨s⟩$.

5. A ring $A$ always contains two special ideals, one is the bottom ideal $⟨0⟩=\{0\}$ (denoted as $\mathrm{\perp }$ lean), and the other is the top ideal $⟨1⟩=A$ (denoted as $\mathrm{\top }$ lean).

Special Ring

1. A ring $A$ is called Principal Ideal Ring (PIR) if every ideal of $A$ is principal, i.e., can be generated by a single element. Moreover, if $A$ is also an integral domain, it is called a Principal Ideal Domain (PID).

Facts on Ideals

1. $1\notin I⟺A^{\ast }\cap I=\mathrm{\varnothing }$, i.e. No unit exists in a proper ideal of a ring.

   Proof

   (a) Regarding the forward direction, in a contrapositive way, we assume $a\in A^{\ast },a\in I$.

   • Since $a\in A^{\ast }$, there exists $b\in A$ such that $a\cdot b=1$.

   • Since $a\in I$, we have $\mathrm{\forall }c\in A,a\cdot c\in I$.

   Putting these two hypotheses together. we obtain $a\cdot b=1\in I$, which contradicts the assumption that $I$ is proper.

   (b) Regarding the backward direction, assume $A^{\ast }\cap I=\mathrm{\varnothing }$, which implies that:

   $$\begin{gathered} \mathrm{\forall }a\in I\to ⌝(\mathrm{\exists }b\in A,a\cdot b=1) \\ \Updownarrow \\ \mathrm{\forall }a\in I\to \mathrm{\forall }b\in A,a\cdot b\ne 1 \end{gathered}$$

   By definition of ideal, $\mathrm{\forall }b\in A,a\cdot b\in I$, therefore, $1\notin I$.

   Lean 4 proof

   /- Fact 1: an ideal is proper iff it contains no unit. -/
   theorem one_not_mem_iff (I : Ideal A) : (1 : A) ∉ I ↔ ∀ a ∈ I, ¬ IsUnit a := by
     constructor
     · -- if a unit `a` with `a * b = 1` lies in `I`, then `1 = a * b ∈ I`
       intro h1 a ha hu
       obtain ⟨b, hb⟩ := hu.exists_right_inv
       apply h1
       rw [← hb]
       exact I.mul_mem_right b ha
     · -- `1` is itself a unit
       intro h h1
       exact h 1 h1 isUnit_one
   
   example (I : Ideal A) {a : A} (ha : a ∈ I) (hu : IsUnit a) : I = ⊤ :=
     Ideal.eq_top_of_isUnit_mem I ha hu

2. If $A$ is a field, then it has only has two ideals: the zero ideal $⟨0⟩$ and the field itself $⟨1⟩=A$.

   Proof

   (a) Firstly, considering the special case of $A=\{0\}$, then the only ideal is $⟨0⟩=\{0\}$.

   (b) Secondly, consider the case when $A$ is a non-zero field. Let $I$ be a non-zero ideal of $A$. By the definition of field $A$ :

   $$\mathrm{\forall }a\ne 0\in A,\mathrm{\exists }b\in A,a\cdot b=1.$$

   Take any non-zero element $a\in I\subseteq A$, by definition of ideal, we have :

   $$\mathrm{\forall }b\in A,a\cdot b\in I$$

   Putting these two hypotheses together, we obtain $a\cdot b=1\in I$. Since $1\in I$, thus $I=⟨1⟩=A$.

   Completing the proof.

   Lean 4 proof

   /- Fact 2: a field has only the ideals `⟨0⟩` and `⟨1⟩`. -/
   theorem eq_bot_or_top_of_field {K : Type*} [Field K] (I : Ideal K) : I = ⊥ ∨ I = ⊤ := by
     by_cases h : I = ⊥
     · exact Or.inl h
     · -- take a nonzero `a ∈ I`; then `1 = a⁻¹ * a ∈ I`
       right
       obtain ⟨a, ha, ha0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h
       rw [Ideal.eq_top_iff_one, ← inv_mul_cancel₀ ha0]
       exact I.mul_mem_left a⁻¹ ha
   
   example {K : Type*} [Field K] (I : Ideal K) : I = ⊥ ∨ I = ⊤ := Ideal.eq_bot_or_top I

Ideal Operations

1. Intersection. For any family of ideals $\{I_h{\}}_{h\in H}$ of $A$, their intersection $\bigcap _{h\in H}{I}_h$ is also an ideal of $A$.

2. Sum. For any family of ideals $\{I_h{\}}_{h\in H}$ of $A$, the ideal generated by their union $\bigcup _{h\in H}{I}_h$ is also an ideal of $A$. It is denoted by $\sum _{h\in H}{I}_h$. That is exists a function :$$f:\bigcup _{h\in H}{I}_h\to \sum _{h\in H}{I}_h=\{\sum _{i=1}^n{a}_i\mid a_i\in I_{h_i},h_i\in H,n\in \mathbb{N}\}$$which is inclusion map. $\sum _{h\in H}{I}_h$ is smallest ideal containing $\bigcup _{h\in H}{I}_h$.

3. Product. For any finite family of ideals $\{I_h{\}}_{h\in H}$ of $A$, their product ideal $\prod _{h\in H}{I}_h$ is generated by

   $$\{\prod _{h\in H}{x}_h\mid x_h\in I_h\text{ for all }h\in H\}.$$

   Observations

   Fact : $I^k\subseteq I^{k-1}\subseteq \cdots \subseteq I\subseteq I^0=A$ for all $k\in \mathbb{N}$.

   Two cases considered, (a) if $1\in I⟺I=A$, then $I^k=I^{k-1}=\cdots =I^0=A$. (b) if $1\notin I$, then we must have $I^k\subseteq I^{k-1}\subseteq \cdots \subseteq I\subseteq I^0=A$. For example, for $A=\mathbb{Z}/(6)$, it is possible that $(⟨2⟩{)}^2=⟨2⟩$.

4. Quotient and Annihilator. For any two ideals $I,J$ of $A$, we define the quotient of $I$ by $J$ as the set

   $$I:J=\{a\in A\mid a\cdot J\subseteq I\}.$$

   In particular, when $I=⟨0⟩$, then the quotient $I:J$ is called the annihilator of $J$ and is denoted by $\mathrm{Ann}(J)$. When $J$ is principal $J=⟨a⟩$, we simply denote it by $\mathrm{Ann}(a)$.

   Observations

   As $J$ is an ideal, so $\mathrm{\forall }a\in A,aJ=J$. So

   1. if $J\subseteq I$, then $I:J=A$.

   2. if $I⊊J$, then $I:J⊊A$.

   3. if $I\cap J=\mathrm{\varnothing }$, then $I:J=\mathrm{\varnothing }$.

5. Radical. For any ideal $I$ of $A$, the radical of $I$ is defined as the set$$\sqrt{I}=\{a\in A\mid \mathrm{\exists }n\in \mathbb{N},a^n\in I\}.$$

Facts on Ideal Operations

1. Intersection of a family of ideals is also an ideal.

   Proof

   Since $\bigcap _{h\in H}{I}_h\subseteq I_k$ for all $k\in H$, then :

   • for any $a,b\in \bigcap _{h\in H}{I}_h$, we have $a+b\in I_h$ for all $h\in H$. That implies that $a+b\in \bigcap _{h\in H}{I}_h$.
   • for any $a\in A$ and $x\in \bigcap _{h\in H}{I}_h$, we have $x\in I_h$ for all $h\in H$. Since each $I_h$ is an ideal, $a\cdot x\in I_h$ for all $h\in H$. That implies that $a\cdot x\in \bigcap _{h\in H}{I}_h$.
   Lean 4 proof

   /- Fact 1: the intersection of a family of ideals is an ideal. -/
   def iInter {ι : Type*} (I : ι → Ideal A) : Ideal A where
     carrier := {x | ∀ h, x ∈ I h}
     zero_mem' := by
       intro h
       exact (I h).zero_mem
     add_mem' := by
       intro a b ha hb h
       exact (I h).add_mem (ha h) (hb h)
     smul_mem' := by
       intro a x hx h
       exact (I h).mul_mem_left a (hx h)
   
   example {ι : Type*} (I : ι → Ideal A) : iInter I = ⨅ h, I h := by
     ext x
     exact (Submodule.mem_iInf I).symm

   
   

2. Quotient is also an ideal.

   Proof that quotient is also an ideal

   For addition closure, let $a,b\in I:J$, we need to show that $a-b\in I:J$. Since

   • $a\cdot J\subseteq I⟺\mathrm{\forall }x\in J,a\cdot x\in I$
   • $b\cdot J\subseteq I⟺\mathrm{\forall }x\in J,b\cdot x\in I$

   By addition closure property of ideal, we have $\mathrm{\forall }x\in J,(a-b)\cdot x\in I$, which implies that $a-b\in I:J$.

   For multiplicity closure, let $a\in I:J$ and for any $r\in A$, we need to show that $r\cdot a\in I:J$.

   • if $r=0$, it trivially holds that $r\cdot a=0\in I:J$.

   • if $r\ne 0$. Since $a\cdot J\subseteq I⟺\mathrm{\forall }x\in J,a\cdot x\in I$, then $\mathrm{\forall }x\in J,(r\cdot a)\cdot x=r\cdot (a\cdot x)\in I$ always holds, which implies that $r\cdot a\in I:J$.

   Lean 4 proof

   /- Fact 2: the quotient `I : J = {a | a * J ⊆ I}` is an ideal. -/
   def colon (I J : Ideal A) : Ideal A where
     carrier := {a | ∀ x ∈ J, a * x ∈ I}
     zero_mem' := by
       intro x _
       rw [zero_mul]
       exact I.zero_mem
     add_mem' := by
       intro a b ha hb x hx
       rw [add_mul]
       exact I.add_mem (ha x hx) (hb x hx)
     smul_mem' := by
       -- `(r * a) * x = r * (a * x) ∈ I`
       intro r a ha x hx
       rw [smul_eq_mul, mul_assoc]
       exact I.mul_mem_left r (ha x hx)
   
   example (I J : Ideal A) (a : A) : a ∈ colon I J ↔ a ∈ I.colon J := by
     rw [Submodule.mem_colon]
     rfl

   
   

3. Radical is also an ideal.

   Proof that radical is also an ideal

   For the addition closure, let $a,b\in \sqrt{I}$, we need to show that $a-b\in \sqrt{I}$.

   • $\mathrm{\exists }m\in \mathbb{N},a^m\in I$
   • $\mathrm{\exists }n\in \mathbb{N},b^n\in I$

   Consider $(a-b{)}^{m+n}$. By the binomial theorem,

   $$(a-b{)}^{m+n}=\sum _{k=0}^{m+n}(\genfrac{}{}{0ex}{}{m+n}{k})a^k(-b{)}^{m+n-k}.$$

   Each term in this sum is in $I$ because either $k\ge m$ or $m+n-k\ge n$, so $a^k\in I$ or $b^{m+n-k}\in I$:

   $$(a-b{)}^{m+n}=(-b{)}^n\cdot \sum _{k=0}^m(\genfrac{}{}{0ex}{}{m}{k})a^k(-b{)}^{m-k}+a^m\cdot \sum _{k=m+1}^{m+n}(\genfrac{}{}{0ex}{}{m+n}{k})a^{k-m}(-b{)}^{m+n-k}$$

   Since $I$ is an ideal and closed under addition, $(a-b{)}^{m+n}\in I$, which implies that $a-b\in \sqrt{I}$.

   For the multiplicity closure, let $a\in \sqrt{I}$ and $r\in A$, we need to show that $r\cdot a\in \sqrt{I}$.

   • $\mathrm{\exists }n\in \mathbb{N},a^n\in I$ Consider $(r\cdot a{)}^n=r^n\cdot a^n$. Since $a^n\in I$ and $I$ is an ideal, $r^n\cdot a^n\in I$, which implies that $(r\cdot a{)}^n\in I$. Therefore, $r\cdot a\in \sqrt{I}$.
   Lean 4 proof

   /- Fact 3: the radical `√I = {a | ∃ n, a ^ n ∈ I}` is an ideal. -/
   def radical (I : Ideal A) : Ideal A where
     carrier := {a | ∃ n : ℕ, a ^ n ∈ I}
     zero_mem' := by
       refine ⟨1, ?_⟩
       rw [pow_one]
       exact I.zero_mem
     add_mem' := by
       -- binomial theorem: each term of `(a + b) ^ (m + n)` has `a ^ k` with `k ≥ m`
       -- or `b ^ (m + n - k)` with `m + n - k ≥ n`
       rintro a b ⟨m, hm⟩ ⟨n, hn⟩
       refine ⟨m + n, ?_⟩
       rw [add_pow]
       refine I.sum_mem fun k _ => ?_
       by_cases h : m ≤ k
       · have e : a ^ k = a ^ m * a ^ (k - m) := by rw [← pow_add, Nat.add_sub_cancel' h]
         rw [e]
         exact I.mul_mem_right _ (I.mul_mem_right _ (I.mul_mem_right _ hm))
       · have hk : n ≤ m + n - k := by omega
         have e : b ^ (m + n - k) = b ^ n * b ^ (m + n - k - n) := by
           rw [← pow_add, Nat.add_sub_cancel' hk]
         rw [e]
         exact I.mul_mem_right _ (I.mul_mem_left _ (I.mul_mem_right _ hn))
     smul_mem' := by
       -- `(r * a) ^ n = r ^ n * a ^ n ∈ I`
       rintro r a ⟨n, hn⟩
       refine ⟨n, ?_⟩
       rw [smul_eq_mul, mul_pow]
       exact I.mul_mem_left _ hn
   
   example (I : Ideal A) (a : A) : a ∈ radical I ↔ a ∈ I.radical := Iff.rfl

   
   

4. The set of nipotent elements $\mathcal{N}(A)$ is also an ideal.

   Proof

   In particular, the set of nilpotent elements is a special case of the radical: $\mathcal{N}(A)=\sqrt{⟨0⟩}$. Indeed, $a^n\in ⟨0⟩$ if and only if $a^n=0$. Since the radical is an ideal, the nilpotent elements form an ideal too.

   Lean 4 proof

   /- Fact 4: the nilpotent elements form the ideal `√⟨0⟩`. -/
   theorem isNilpotent_iff_mem_radical_bot (a : A) : IsNilpotent a ↔ a ∈ radical ⊥ := by
     show (∃ n : ℕ, a ^ n = 0) ↔ ∃ n : ℕ, a ^ n ∈ (⊥ : Ideal A)
     simp only [Ideal.mem_bot]
   
   example (a : A) : a ∈ nilradical A ↔ IsNilpotent a := mem_nilradical

5. The set of zero-divisors $\mathcal{D}(A)$ is not an ideal in general.

   Proof

   Not an ideal means either addition or multiplicity closure fails, we choose the former one. That is

   $$\mathrm{\exists }a,b\in \mathcal{D}(A)\text{ such that }a+b\notin \mathcal{D}(A).$$

   Take $A=\mathbb{Z}/(6)$, $a=2$ and $b=3$. Since $2\cdot 3=0$ with $3\ne 0$ and $2\ne 0$, both $a$ and $b$ are zero-divisors.

   However, $a+b=5$ and $5\cdot 5=25=1$, so $a+b$ is a unit. By fact (2) on special elements, no unit is a zero divisor, so $a+b\notin \mathcal{D}(A)$.

   Lean 4 proof

   /- Fact 5: the zero divisors need not form an ideal.
   In `ℤ/6ℤ`, `2` and `3` are zero divisors (`2 * 3 = 0`), but `2 + 3 = 5` is a unit. -/
   theorem zeroDivisors_not_ideal :
       ¬ ∃ I : Ideal (ZMod 6), ∀ a, a ∈ I ↔ IsZeroDivisor a := by
     rintro ⟨I, hI⟩
     have h2 : (2 : ZMod 6) ∈ I := (hI 2).mpr ⟨3, by decide, by decide⟩
     have h3 : (3 : ZMod 6) ∈ I := (hI 3).mpr ⟨2, by decide, by decide⟩
     have h5 : IsUnit (2 + 3 : ZMod 6) := IsUnit.of_mul_eq_one 5 (by decide)
     exact not_isZeroDivisor_of_isUnit h5 ((hI _).mp (I.add_mem h2 h3))

   
   

6. If $I,J$ are two ideals of a ring $A$, then $IJ\subseteq I\cap J$.

   Proof

   Firstly we decompose the argument :

   $$IJ\subseteq I\cap J⟺\mathrm{\forall }x\in IJ,x\in I\cap J⟺\mathrm{\forall }a\in I,\mathrm{\forall }b\in J,a\cdot b\in I\cap J$$

   Since $a\in I$, so we have $a\cdot b\in I$. Similarly, since $b\in J$, we have $a\cdot b\in J$. Therefore, $a\cdot b\in I\cap J$. Completing the proof.

   Lean 4 proof

   /- Fact 6: `I J ⊆ I ∩ J`. -/
   theorem mul_le_inf' (I J : Ideal A) : I * J ≤ I ⊓ J := by
     -- it suffices to check the generators `a * b` with `a ∈ I`, `b ∈ J`
     rw [Ideal.mul_le]
     intro a ha b hb
     exact Submodule.mem_inf.mpr ⟨I.mul_mem_right b ha, J.mul_mem_left a hb⟩
   
   example (I J : Ideal A) : I * J ≤ I ⊓ J := Ideal.mul_le_inf

   
   

7. If $I,J$ are two ideals of a ring $A$, and $I+J=⟨1⟩$, then $I\cap J=IJ$. $I$ and $J$ are comaximal.

   Proof

   By (6), we only need to show the converse inclusion: $I\cap J\subseteq IJ$ when $I+J=⟨1⟩$.

   By $I+J=⟨1⟩⟺A\subseteq I+J⟺\mathrm{\forall }x\in A,\mathrm{\exists }y\in I,\mathrm{\exists }z\in J,x=y+z$, thus for any $x\in I\cap J$, we can write $x=y+z$ with existence of $y\in I$ and $z\in J$.

   So for any $x\in I\cap J$, we can write it as $x=x\cdot 1=x\cdot (y+z)\in I\cap J$ with the existence of $y\in I$ and $z\in J$. After some expanding, and $x\in J$ and $x\in I$, we have :

   $$x=x\cdot (y+z)=x\cdot y+x\cdot z\in IJ$$

   which proves $\mathrm{\forall }x\in I\cap J,x\in IJ$. Therefore, $I\cap J\subseteq IJ$. Completing the proof.

   Lean 4 proof

   /- Fact 7: if `I + J = ⟨1⟩`, then `I ∩ J = I J`. -/
   theorem inf_eq_mul_of_sup_eq_top (I J : Ideal A) (h : I ⊔ J = ⊤) : I ⊓ J = I * J := by
     refine le_antisymm ?_ (mul_le_inf' I J)
     intro x hx
     obtain ⟨hxI, hxJ⟩ := Submodule.mem_inf.mp hx
     -- write `1 = y + z` with `y ∈ I`, `z ∈ J`
     have h1 : (1 : A) ∈ I ⊔ J := by
       rw [h]
       exact Submodule.mem_top
     obtain ⟨y, hy, z, hz, hyz⟩ := Submodule.mem_sup.mp h1
     -- `x = x * (y + z) = y * x + x * z ∈ I J`
     have e : x = y * x + x * z := by
       calc x = x * (y + z) := by rw [hyz, mul_one]
         _ = y * x + x * z := by ring
     rw [e]
     exact Ideal.add_mem _ (Ideal.mul_mem_mul hy hxJ) (Ideal.mul_mem_mul hxI hz)
   
   example (I J : Ideal A) (h : I ⊔ J = ⊤) : I * J = I ⊓ J := Ideal.mul_eq_inf_of_coprime h

   
   

8. Let $I_1,...,I_n$ are pairwise comaximal ideals of a ring $A$. Then

   $$I_1\cap ...\cap I_n=I_1\cdot ...\cdot I_n.$$

   This is a general form of the result in (7) for two comaximal ideals. We omit the proof here.

9. Let $I,J,H$ be ideals of a ring $A$. Then$$\begin{array}{rl}\text{(a) }& (I+J)H=IH+JH\\ \text{(b) }& (I+J)(I\cap J)\subseteq IJ\\ \text{(c) }& (I\cap J)+(I\cap H)\subseteq I\cap (J+H)\\ \text{(d) }& J\subset I\text{ or }I\subset H\to I\cap (J+H)=(I\cap J)+(I\cap H)\\ \text{(e) }& I+JH\subseteq (I+J)\cap (I+H)\end{array}$$

Properties of the Radical

Let $A$ be a ring, and let $I,J,H$ be ideals of $A$. Then :

1. if $I\subseteq J$, then $\sqrt{I}\subseteq \sqrt{J}$.

   Proof

   In order to show $\sqrt{I}\subseteq \sqrt{J}$, it is suffices to show :

   $$\mathrm{\forall }x\in \sqrt{I}⟹x\in \sqrt{J}⟺\mathrm{\forall }x\in \sqrt{I},\mathrm{\exists }n\in \mathbb{N},x^n\in I⟹\mathrm{\exists }m\in \mathbb{N},x^m\in J$$

   Since $x^n\in I\subseteq J$, use $m=n$, we have $x^m\in J$. Completing the proof.

   Lean 4 proof

   theorem radical_mono' (I J : Ideal A) (h : I ≤ J) : I.radical ≤ J.radical := by
     rintro x ⟨n, hn⟩
     exact ⟨n, h hn⟩

   
   

2. $I\subseteq \sqrt{I}$ and $\sqrt{\sqrt{I}}=\sqrt{I}$

   Proof

   For any $x\in I$, we have $x^1=x\in I$, hence $x\in \sqrt{I}$. This shows $I\subseteq \sqrt{I}$.

   In order to show $\sqrt{\sqrt{I}}=\sqrt{I}$, since $\sqrt{I}\subseteq \sqrt{\sqrt{I}}$ follows from the fact that $I\subseteq \sqrt{I}$, it suffices to show the forward inclusion is true, i.e., $\sqrt{\sqrt{I}}\subseteq \sqrt{I}$. That is,

   $$\begin{gathered} \sqrt{\sqrt{I}}\subseteq \sqrt{I}⟺\mathrm{\forall }x\in \sqrt{\sqrt{I}}⟹x\in \sqrt{I} \\ ⟺\mathrm{\forall }x\in \sqrt{\sqrt{I}},\mathrm{\exists }n\in \mathbb{N},x^n\in \sqrt{I}⟹\mathrm{\exists }m\in \mathbb{N},x^m\in I \end{gathered}$$

   Since $x^n\in \sqrt{I}$ for some $n\in \mathbb{N}$, by definition of $\sqrt{I}$, there exists $p\in \mathbb{N}$ such that $(x^n{)}^p=x^{np}\in I$. So use $m=np$, we have $x^m\in I$. Completing the proof.

   Lean 4 proof

   theorem le_radical_and_idem (I : Ideal A) :
       I ≤ I.radical ∧ I.radical.radical = I.radical := by
     have hle : I ≤ I.radical := fun x hx => ⟨1, by simpa using hx⟩
     refine ⟨hle, le_antisymm ?_ Ideal.le_radical⟩
     rintro x ⟨n, m, h⟩
     exact ⟨n * m, by simpa only [pow_mul] using h⟩

   
   

3. $\sqrt{IJ}=\sqrt{I\cap J}=\sqrt{I}\cap \sqrt{J}$

   Proof

   (a) First, we show $\sqrt{IJ}=\sqrt{I\cap J}$. Since $IJ\subseteq I\cap J$, by property (1) above, we have $\sqrt{IJ}\subseteq \sqrt{I\cap J}$. So it suffices to show the backward direction inclusion $\sqrt{I\cap J}\subseteq \sqrt{IJ}$. That is,

   $$\begin{gathered} \sqrt{I\cap J}\subseteq \sqrt{IJ}⟺\mathrm{\forall }x\in \sqrt{I\cap J}⟹x\in \sqrt{IJ} \\ ⟺\mathrm{\forall }x\in \sqrt{I\cap J},\mathrm{\exists }n\in \mathbb{N},x^n\in I\cap J⟹\mathrm{\exists }m\in \mathbb{N},x^m\in IJ \end{gathered}$$

   $x^n\in I\cap J$ for some $n\in \mathbb{N}$ implies $x^n\in I$ and $x^n\in J$, hence by definition we have $x^{2n}=(x^n{)}^2\in IJ$. So use $m=2n$, we have $x^m\in IJ$. Completing the proof of (a).

   
   

   (b) Next, in order to show the equality $\sqrt{I\cap J}=\sqrt{I}\cap \sqrt{J}$, we first show the forward inclusion direction $\sqrt{I\cap J}\subseteq \sqrt{I}\cap \sqrt{J}$. That is,

   $$\begin{gathered} \sqrt{I\cap J}\subseteq \sqrt{I}\cap \sqrt{J}⟺\mathrm{\forall }x\in \sqrt{I\cap J}⟹x\in \sqrt{I}\cap \sqrt{J} \\ ⟺\mathrm{\forall }x\in \sqrt{I\cap J},\mathrm{\exists }n\in \mathbb{N},x^n\in I\cap J⟹\mathrm{\exists }{m}_1,m_2\in \mathbb{N},x^{m_1}\in I\text{ and }{x}^{m_2}\in J \end{gathered}$$

   $x^n\in I\cap J$ for some $n\in \mathbb{N}$ implies $x^n\in I$ and $x^n\in J$, hence use $m_1=n,m_2=n$, we have $x^{m_1}\in I$ and $x^{m_2}\in J$. Completing the proof of the forward inclusion.

   
   

   Then we show the backward inclusion direction $\sqrt{I}\cap \sqrt{J}\subseteq \sqrt{I\cap J}$. That is,

   $$\begin{gathered} \sqrt{I}\cap \sqrt{J}\subseteq \sqrt{I\cap J}⟺\mathrm{\forall }x\in \sqrt{I}\cap \sqrt{J}⟹x\in \sqrt{I\cap J} \\ ⟺\mathrm{\forall }x\in \sqrt{I}\cap \sqrt{J},\mathrm{\exists }{m}_1,m_2\in \mathbb{N},x^{m_1}\in I\text{ and }{x}^{m_2}\in J⟹\mathrm{\exists }n\in \mathbb{N},x^n\in I\cap J \end{gathered}$$

   Since $x^{m_1}\in I,x^{m_2}\in J$, by definition, we have $x^{m_1}\cdot x^{m_2}=x^{m_1+m_2}\in IJ$. Hence, using $n=m_1+m_2$, we have $x^n\in IJ$. Again by $IJ\subseteq I\cap J$, we have $x^n\in I\cap J$. Completing the proof of the backward inclusion.

   Lean 4 proof

   theorem radical_mul_inf (I J : Ideal A) :
       (I * J).radical = (I ⊓ J).radical ∧
         (I ⊓ J).radical = I.radical ⊓ J.radical := by
     have hi : (I ⊓ J).radical = I.radical ⊓ J.radical := by
       apply le_antisymm
       · exact le_inf (radical_mono' _ _ inf_le_left) (radical_mono' _ _ inf_le_right)
       · rintro x ⟨⟨m, hm⟩, ⟨n, hn⟩⟩
         refine ⟨m + n, ?_⟩
         rw [pow_add]
         exact ⟨I.mul_mem_right _ hm, J.mul_mem_left _ hn⟩
     refine ⟨le_antisymm (radical_mono' _ _ Ideal.mul_le_inf) ?_, hi⟩
     rintro x ⟨n, hn⟩
     refine ⟨n + n, ?_⟩
     rw [pow_add]
     exact Ideal.mul_mem_mul hn.1 hn.2

4. $\sqrt{I^n}=\sqrt{I}$ for any integer $n\ge 1$.

   Proof

   Induct on $n\ge 1$. The case $n=1$ is immediate. For the induction step, property (3) gives $\sqrt{I^{n+1}}=\sqrt{I^{n}I}=\sqrt{I^n}\cap \sqrt{I}=\sqrt{I}$. The restriction is necessary: $I^0=A$, whose radical is $A$.

   Lean 4 proof

   theorem radical_pow_positive (I : Ideal A) (n : ℕ) (hn : n ≠ 0) :
       (I ^ n).radical = I.radical := by
     obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
     induction k with
     | zero => simp
     | succ k ih =>
       rw [pow_succ, (radical_mul_inf _ _).1, (radical_mul_inf _ _).2,
         ih (Nat.succ_ne_zero k), inf_idem]

   
   

5. $\sqrt{I}=⟨1⟩$ if and only if $I=⟨1⟩$.

6. $\sqrt{I+J}=\sqrt{\sqrt{I}+\sqrt{J}}$

   Proof

   In order to show the equality $\sqrt{I+J}=\sqrt{\sqrt{I}+\sqrt{J}}$, we first show the forward inclusion directions. That is,

   $$\begin{gathered} \sqrt{I+J}\subseteq \sqrt{\sqrt{I}+\sqrt{J}}⟺\mathrm{\forall }x\in \sqrt{I+J}⟹x\in \sqrt{\sqrt{I}+\sqrt{J}} \\ ⟺\mathrm{\forall }x\in \sqrt{I+J},\mathrm{\exists }n\in \mathbb{N},x^n\in I+J⟹\mathrm{\exists }m\in \mathbb{N},x^m\in \sqrt{I}+\sqrt{J} \end{gathered}$$

   As $x^n\in I+J$ implies $\mathrm{\exists }{x}_1\in I,x_2\in J$ such that $x^n=x_1+x_2$. We use $m=n$, then by the property (2) above, we have $x_1\in \sqrt{I},x_2\in \sqrt{J}$, thus $x^m=x_1+x_2\in \sqrt{I}+\sqrt{J}$. Completing the proof of the forward inclusion.

   
   

   Next, we show the backward inclusion direction $\sqrt{\sqrt{I}+\sqrt{J}}\subseteq \sqrt{I+J}$. That is,

   $$\begin{gathered} \sqrt{\sqrt{I}+\sqrt{J}}\subseteq \sqrt{I+J}⟺\mathrm{\forall }x\in \sqrt{\sqrt{I}+\sqrt{J}}⟹x\in \sqrt{I+J} \\ ⟺\mathrm{\forall }x\in \sqrt{\sqrt{I}+\sqrt{J}},\mathrm{\exists }m\in \mathbb{N},x^m\in \sqrt{I}+\sqrt{J}⟹\mathrm{\exists }n\in \mathbb{N},x^n\in I+J \end{gathered}$$

   Since $x^m\in \sqrt{I}+\sqrt{J}$, write $x^m=x_1+x_2$ with $x_1^{k_1}\in I$ and $x_2^{k_2}\in J$. In the binomial expansion of $(x_1+x_2{)}^{k_1+k_2}$, every term has either at least $k_1$ factors of $x_1$ or at least $k_2$ factors of $x_2$, so every term belongs to $I+J$. Thus $x^{m(k_1+k_2)}\in I+J$, completing the backward inclusion.

   Lean 4 proof

   theorem radical_sup' (I J : Ideal A) :
       (I ⊔ J).radical = (I.radical ⊔ J.radical).radical := by
     apply le_antisymm
     · exact radical_mono' _ _ (sup_le_sup Ideal.le_radical Ideal.le_radical)
     · have h : I.radical ⊔ J.radical ≤ (I ⊔ J).radical :=
         sup_le (radical_mono' _ _ le_sup_left) (radical_mono' _ _ le_sup_right)
       exact (radical_mono' _ _ h).trans_eq (le_radical_and_idem _).2

   
   

7. $\sqrt{I+JH}=\sqrt{I+J}\cap \sqrt{I+H}$

   Proof

   In order to prove the equality $\sqrt{I+JH}=\sqrt{I+J}\cap \sqrt{I+H}$, we need to show both inclusions.

   Forward inclusion: $\sqrt{I+JH}\subseteq \sqrt{I+J}\cap \sqrt{I+H}$, that is,

   $$\begin{gathered} \sqrt{I+JH}\subseteq \sqrt{I+J}\cap \sqrt{I+H}⟺\mathrm{\forall }x\in \sqrt{I+JH}⟹x\in \sqrt{I+J}\cap \sqrt{I+H} \\ ⟺\mathrm{\forall }x\in \sqrt{I+JH},\mathrm{\exists }n\in \mathbb{N},x^n\in I+JH⟹\mathrm{\exists }{m}_1,m_2\in \mathbb{N},x^{m_1}\in I+J\text{ and }{x}^{m_2}\in I+H \end{gathered}$$

   As $x^n\in I+JH$ implies $\mathrm{\exists }{x}_1\in I,x_2\in JH$ such that $x^n=x_1+x_2$. We use $m_1=m_2=n$, as $H\subseteq A$ thus we have $JH\subseteq J$, then $x^{m_1}=x_1+x_2\in I+JH\subseteq I+J$, similarly we have $x^{m_2}=x_1+x_2\in I+JH\subseteq I+H$. Completing the proof of the forward inclusion.

   
   

   Backward inclusion: $\sqrt{I+J}\cap \sqrt{I+H}\subseteq \sqrt{I+JH}$, that is,

   $$\begin{gathered} \sqrt{I+J}\cap \sqrt{I+H}\subseteq \sqrt{I+JH}⟺\mathrm{\forall }x\in \sqrt{I+J}\cap \sqrt{I+H}⟹x\in \sqrt{I+JH} \\ ⟺\mathrm{\forall }x\in \sqrt{I+J}\cap \sqrt{I+H},\mathrm{\exists }{m}_1,m_2\in \mathbb{N},x^{m_1}\in I+J\text{ and }{x}^{m_2}\in I+H⟹\mathrm{\exists }n\in \mathbb{N},x^n\in I+JH \end{gathered}$$

   Since $x^{m_1}\in I+J$ and $x^{m_2}\in I+H$, thus we have $x^{m_1}\cdot x^{m_2}=x^{m_1+m_2}\in (I+J)(I+H)\subseteq I+JH$. Let $n=m_1+m_2$, then $x^n\in I+JH$. Completing the proof of the backward inclusion.

   Lean 4 proof

   theorem radical_sup_mul (I J H : Ideal A) :
       (I ⊔ J * H).radical = (I ⊔ J).radical ⊓ (I ⊔ H).radical := by
     apply le_antisymm
     · exact le_inf
         (radical_mono' _ _ (sup_le_sup_left ((mul_le_inf' J H).trans inf_le_left) I))
         (radical_mono' _ _ (sup_le_sup_left ((mul_le_inf' J H).trans inf_le_right) I))
     · rintro x ⟨⟨m, hm⟩, ⟨n, hn⟩⟩
       refine ⟨m + n, ?_⟩
       rw [pow_add]
       obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hm
       obtain ⟨c, hc, d, hd, hcd⟩ := Submodule.mem_sup.mp hn
       rw [← hab, ← hcd]
       have hi : a * c + a * d + b * c ∈ I :=
         I.add_mem (I.add_mem (I.mul_mem_right _ ha) (I.mul_mem_right _ ha))
           (I.mul_mem_left _ hc)
       have hj : b * d ∈ J * H := Ideal.mul_mem_mul hb hd
       have he : (a + b) * (c + d) = (a * c + a * d + b * c) + b * d := by ring
       rw [he]
       exact (I ⊔ J * H).add_mem
         ((show I ≤ I ⊔ J * H from le_sup_left) hi)
         ((show J * H ≤ I ⊔ J * H from le_sup_right) hj)

   
   

Maximal Ideal

As we know, maximal ideal is derived from the concept of proper ideal. A few important facts upon maximal ideal are derived from Zorn's Lemma.

Zorn's Lemma

Poset Definition : A poset $(\mathrm{\Sigma },\le )$ is a set $\mathrm{\Sigma }$ equipped with a partial order $\le$ which is reflexive, antisymmetric, and transitive. Every chain in a poset is a totally ordered subset of $\mathrm{\Sigma }$.

Zorn's Lemma : Let $(\mathrm{\Sigma },\le )$ be a partially ordered set in which every chain has an upper bound in $\mathrm{\Sigma }$. Then $\mathrm{\Sigma }$ contains maximal elements with respect to the partial order $\le$.

Facts on Maximal Ideal

Let $A$ be a non-zero ring. Then

1. $A$ has at least one maximal ideal $\mathfrak{m}$.

2. For any proper ideal $I$ of $A$, there exists a maximal ideal $\mathfrak{m}$ such that $I\subseteq \mathfrak{m}$.

3. Every non-invertible element of $A$ is contained in some maximal ideal of $A$.

Proof

Regarding (1), we can treat $A$ as a poset whose elements are the proper ideals of $A$, ordered by inclusion $\subseteq$.

$$\mathrm{\Sigma }=\{I⊊A\mid I\text{ is a ideal of }A\}$$

For example, $⟨a⟩\subseteq ⟨a,b⟩\subseteq ⟨a,b,c⟩\subseteq \cdots$.

By Zorn's Lemma, in order to show $A$ contains maximal ideals with respect to order relation $\subseteq$, it suffices to show that for any chain of proper ideals $\mathcal{C}=\{I_h:h\in H\}$ in $A$, there exists an upper bound in $A$.

For any chain of proper ideals $\mathcal{C}=\{I_h:h\in H\}$ in $A$, the upper bound of this chain is the minimal set containing all the proper ideals, it can defined by

$$I=\bigcup _{h\in H}{I}_h.$$

Then we need to show that :

1. $I$ is an ideal of $A$.
   • Addition closure, i.e. for any $x,y\in I$, we have $x+y\in I$.
   • Multiplication closure, i.e. for any $a\in A$ and $x\in I$, we have $a\cdot x\in I$.
2. $I$ is a proper ideal of $A$, i.e. $I⊊A$.
   • $1\notin I$ proof details are ignored here.

Regarding (2), it is trivially holds for any chain of proper ideals in $A$.

Regarding (3), if $a\in A$ is not invertible, implying that

$$⌝(\mathrm{\exists }b\in A,a\cdot b=1)⟺\mathrm{\forall }b\in A,a\cdot b\ne 1$$

Then the principal ideal $⟨a⟩$ do not contains $1$, which means $⟨a⟩$ is a proper ideal of $A$. By (2), there exists a maximal ideal $\mathfrak{m}$ such that $⟨a⟩\subseteq \mathfrak{m}$.

Lean 4 proof

/- Fact 2: every proper ideal is contained in a maximal ideal (Zorn's lemma). -/
theorem exists_le_maximal' (I : Ideal A) (hI : I ≠ ⊤) :
    ∃ M : Ideal A, M.IsMaximal ∧ I ≤ M := by
  -- every nonempty chain of proper ideals has a proper upper bound: its union
  have ih : ∀ c ⊆ {J : Ideal A | J ≠ ⊤}, IsChain (· ≤ ·) c →
      ∀ J ∈ c, ∃ ub ∈ {J : Ideal A | J ≠ ⊤}, ∀ K ∈ c, K ≤ ub := by
    intro c hcs hchain J hJ
    refine ⟨sSup c, ?_, fun K hK => le_sSup hK⟩
    -- `1 ∉ ⋃ c`, since `1` would lie in some proper ideal of the chain
    show sSup c ≠ ⊤
    rw [Ne, Ideal.eq_top_iff_one]
    intro h1
    obtain ⟨K, hKc, h1K⟩ := (Submodule.mem_sSup_of_directed ⟨J, hJ⟩ hchain.directedOn).mp h1
    exact hcs hKc ((Ideal.eq_top_iff_one K).mpr h1K)
  obtain ⟨M, hIM, hM⟩ := zorn_le_nonempty₀ {J : Ideal A | J ≠ ⊤} ih I hI
  -- a maximal element of the proper ideals is a maximal ideal
  refine ⟨M, ⟨⟨hM.prop, fun J hMJ => ?_⟩⟩, hIM⟩
  by_contra hJ
  exact hMJ.ne' (le_antisymm (hM.2 hJ hMJ.le) hMJ.le)

example (I : Ideal A) (hI : I ≠ ⊤) : ∃ M : Ideal A, M.IsMaximal ∧ I ≤ M :=
  Ideal.exists_le_maximal I hI

/- Fact 1: a nonzero ring has at least one maximal ideal. -/
theorem exists_maximal' [Nontrivial A] : ∃ M : Ideal A, M.IsMaximal := by
  obtain ⟨M, hM, -⟩ := exists_le_maximal' (⊥ : Ideal A) bot_ne_top
  exact ⟨M, hM⟩

example [Nontrivial A] : ∃ M : Ideal A, M.IsMaximal := Ideal.exists_maximal A

/- Fact 3: every non-invertible element lies in some maximal ideal. -/
theorem exists_maximal_of_not_isUnit {a : A} (ha : ¬ IsUnit a) :
    ∃ M : Ideal A, M.IsMaximal ∧ a ∈ M := by
  -- `⟨a⟩` is proper, so apply Fact 2
  have hprop : Ideal.span {a} ≠ ⊤ := fun h => ha (Ideal.span_singleton_eq_top.mp h)
  obtain ⟨M, hM, haM⟩ := exists_le_maximal' _ hprop
  exact ⟨M, hM, haM (Ideal.mem_span_singleton_self a)⟩

example {a : A} (ha : a ∈ nonunits A) : ∃ M : Ideal A, M.IsMaximal ∧ a ∈ M :=
  exists_max_ideal_of_mem_nonunits ha

Other Special Ideals

Let $A$ be a ring, and let $I,I_1,I_2\subset A$ be proper ideals. Then, $I$ is :

1. prime, if $ab\in I$ implies $a\in I$ or $b\in I$ for all $a,b\in A$;

   Prime ideal means any element of the ideal can be decomposed into a product of elements, at least one of which lies in the ideal. We give out an couter-example, suppose $A=\mathbb{Z}$ and $I=⟨6⟩$, then :

   $$6=2\cdot 3$$

   where $2,3\notin I$

2. radical, if $I=\sqrt{I}$;

   Note the difference between radical of an ideal and radical ideal, by the property (2) of radical, $I\subseteq \sqrt{I}$, we see that radical ideal is a special case where the ideal coincides with its radical.

3. primary, if $ab\in I$ implies $a\in I$ or $b\in \sqrt{I}$;

   Note the difference between primary ideal and prime ideal, a prime ideal is always primary, but a primary ideal need not be prime. This is reflected by the fact that $I\subseteq \sqrt{I}$, and the inclusion can be strict.

4. irreducible, if $I=I_1\cap I_2$ implies $I=I_1$ or $I=I_2$.

   Irreducible ideal only exists when $I_1\subseteq I_2$ or $I_2\subseteq I_1$.

Facts on Special Ideals

Let $I$ be a proper ideal of $A$. Then we have the following facts:

1. If $I$ is primary, then $\sqrt{I}$ is prime.

   Proof

   Since $I$ is proper, $\sqrt{I}$ is proper: $1\in \sqrt{I}$ would imply $1^n=1\in I$. If $ab\in \sqrt{I}$, choose $n$ with $a^n{b}^n=(ab{)}^n\in I$. Primaryness gives either $a^n\in I$, hence $a\in \sqrt{I}$, or $b^n\in \sqrt{I}$. In the latter case choose $m$ with $b^{nm}\in I$, so $b\in \sqrt{I}$. This proves that $\sqrt{I}$ is prime.

   Lean 4 proof

   theorem primary_radical_prime (I : Ideal A) (hI : I.IsPrimary) : I.radical.IsPrime := by
     refine ⟨?_, ?_⟩
     · exact fun h => (Ideal.isPrimary_iff.mp hI).1 (Ideal.radical_eq_top.mp h)
     · intro a b hab
       obtain ⟨n, hn⟩ := hab
       rw [mul_pow] at hn
       rcases (Ideal.isPrimary_iff.mp hI).2 hn with ha | hb
       · exact Or.inl ⟨n, ha⟩
       · exact Or.inr (Ideal.mem_radical_of_pow_mem hb)

   
   

2. If $I$ is a maximal ideal, then $A/I$ is a field.

   Proof

   By the definition of field, it is suffices to show :

   $$\mathrm{\forall }x+I\in A/I,x\notin I⟹\mathrm{\exists }m+I\in A/I,(x+I)(m+I)=1$$

   ---

   If $x\notin I$, $I$ is maximal, then we must have :

   $$I\subseteq ⟨x⟩+I=A$$

   because $⟨x⟩+I$ strictly contains $I$, and maximality forces it to equal $A$.

   ---

   So any element $a\in A$ can be represented as $a=mx+i$ for $i\in I$, we take $a=1$. Then modulo $I$ on both sides, we get

   $$1+I=mx+I=(m+I)(x+I)$$

   Completing the proof.

   Lean 4 proof

   theorem maximal_quotient_field (I : Ideal A) (hI : I.IsMaximal) : IsField (A ⧸ I) := by
     letI := hI
     letI := Ideal.Quotient.field I
     exact Field.toIsField _

   
   

3. If $\sqrt{I}=\mathfrak{m}$ is a maximal ideal, then $I$ is primary.

   Proof

   By the definition of primary ideal, it is suffices to show that for any $ab\in I$ when $a\notin I$, we must have $b\in \sqrt{I}$. By contradiction, we assume $b\notin \sqrt{I}$.

   ---

   Since $\sqrt{I}$ is maximal, by fact (2) above, we know that the quotient ring $A/\sqrt{I}$ is a field, which implies every nonzero element in $A/\sqrt{I}$ is invertible. More specially,

   $$b+\sqrt{I}\in A/\sqrt{I},b\notin \sqrt{I},\mathrm{\exists }c+\sqrt{I}\in A/\sqrt{I},(b+\sqrt{I})(c+\sqrt{I})=1$$

   Thus we have :

   $$\begin{gathered} (b+\sqrt{I})(c+\sqrt{I})=bc+\sqrt{I}=1+\sqrt{I}⟹bc-1\in \sqrt{I}⟺\mathrm{\exists }n\in \mathbb{N},(bc-1{)}^n\in I \\ ⟹\mathrm{\exists }n\in \mathbb{N},a(bc-1{)}^n\in I \end{gathered}$$

   ---

   After expanding :

   $$a(bc-1{)}^n=(-1{)}^{n}a+\sum _{k=1}^n(\genfrac{}{}{0ex}{}{n}{k})a(bc{)}^k(-1{)}^{n-k}\in I$$

   We have assumed that $ab\in I$, thus $\sum _{k=1}^n(\genfrac{}{}{0ex}{}{n}{k})a(bc{)}^k(-1{)}^{n-k}\in I$ as well, which implies $(-1{)}^{n}a\in I$, and hence $a\in I$. Contradiction happens, which completes the proof.

   Lean 4 proof

   theorem primary_of_maximal_radical (I : Ideal A) (h : I.radical.IsMaximal) :
       I.IsPrimary := by
     -- Mathlib packages the maximal-ideal argument, avoiding a binomial expansion.
     exact Ideal.isPrimary_of_isMaximal_radical h

Krull Dimension

Let $A$ be a ring. The Krull Dimension of $A$, denoted by $\dim (A)$, is defined as the supremum of the lengths $n$ of all chains of prime ideals:

$${\mathfrak{p}}_0⊊{\mathfrak{p}}_1⊊\cdots ⊊{\mathfrak{p}}_n$$

in $A$.

For example,

• if $A$ is a field, there are only two ideals $⟨0⟩$ and $A$, but only $⟨0⟩$ is prime, $⟨0⟩$ forms the longest chain of prime ideals,

  $$⟨0⟩$$

  so the Krull dimension is $0$.

• if $A=\mathbb{Z}$, there are two prime ideals $⟨0⟩$ and $⟨p⟩$ for any prime number $p$, and a strict inclusion exists between them

  $$⟨0⟩⊊⟨p⟩$$

  so the Krull dimension is $1$ for the longest chain of prime ideals.

• if $A=k[X]$, similar with $A=\mathbb{Z}$, there are two prime ideals $⟨0⟩$ and $⟨f⟩$ for any irreducible polynomial $f\in k[X]$, and a strict inclusion exists between them

  $$⟨0⟩⊊⟨f⟩$$

  so the Krull dimension is $1$ for the longest chain of prime ideals.

Homomorphisms and Quotient Rings

Definition of Quotient Ring

Let $A$ be a (commutative with identity) ring,

1. Every ideal $I$ of $A$ is a normal subgroup of $A$, thus $A/I$ forms a quotient group. The reasons behind this are as follows:

   • $A$ itself is a commutative additive group.
   • Additive closure of ideal ensures $I$ is a subgroup of $A$.
   • Commutative property ensure this subgroup is normal.
   • That $I$ is normal ensure that $A/I$ is a quotient group.

2. The element of $A/I$ is denoted as $\bar{x}=x+I$ where $x\in A$ is a representative of the coset $\bar{x}$.

3. The addition and multiplication in the quotient ring $A/I$ are defined as follows:

   $$\bar{x}+\bar{y}=\overline{x+y},\bar{x}\cdot \bar{y}=\overline{xy},\mathrm{\forall }x,y\in A.$$

---

We need to show that the addition and multiplication in the quotient ring $A/I$ are well-defined, i.e., if $\bar{x}=\overline{x^{\prime }}$ and $\bar{y}=\overline{y^{\prime }}$, then

$$\bar{x}+\bar{y}=\overline{x^{\prime }}+\overline{y^{\prime }},\bar{x}\cdot \bar{y}=\overline{x^{\prime }}\cdot \overline{y^{\prime }}.$$

Proof

For addition, by definition, we have :

• $\bar{x}+\bar{y}=\overline{x+y}$
• $\overline{x^{\prime }}+\overline{y^{\prime }}=\overline{x^{\prime }+y^{\prime }}$

So, we need to show that $\overline{x+y}=\overline{x^{\prime }+y^{\prime }}$. This is equivalent to showing that $(x+y)-(x^{\prime }+y^{\prime })\in I$. Since $\bar{x}=\overline{x^{\prime }}$ and $\bar{y}=\overline{y^{\prime }}$, we have $x-x^{\prime }\in I$ and $y-y^{\prime }\in I$. Therefore,

$$(x+y)-(x^{\prime }+y^{\prime })=(x-x^{\prime })+(y-y^{\prime })\in I,$$

which proves that addition is well-defined.

For multiplication, $xy-x^{\prime }{y}^{\prime }=(x-x^{\prime })y+x^{\prime }(y-y^{\prime })\in I$ by absorption and additive closure of the ideal. Thus multiplication is well-defined too.

Lean 4 proof

theorem quotient_operations_well_defined (I : Ideal A) (x x' y y' : A)
    (hx : Ideal.Quotient.mk I x = Ideal.Quotient.mk I x')
    (hy : Ideal.Quotient.mk I y = Ideal.Quotient.mk I y') :
    Ideal.Quotient.mk I (x + y) = Ideal.Quotient.mk I (x' + y') ∧
      Ideal.Quotient.mk I (x * y) = Ideal.Quotient.mk I (x' * y') := by
  have hxi := Ideal.Quotient.eq.mp hx
  have hyi := Ideal.Quotient.eq.mp hy
  constructor
  · apply Ideal.Quotient.eq.mpr
    have he : (x + y) - (x' + y') = (x - x') + (y - y') := by ring
    rw [he]
    exact I.add_mem hxi hyi
  · apply Ideal.Quotient.eq.mpr
    have he : x * y - x' * y' = (x - x') * y + x' * (y - y') := by ring
    rw [he]
    exact I.add_mem (I.mul_mem_right _ hxi) (I.mul_mem_left _ hyi)

Ring Homomorphism

Let $A$ and $B$ be two rings. A function $\varphi :A\to B$ is called a ring homomorphism if for all $a,b\in A$, the following conditions hold:

1. $\varphi (a+b)=\varphi (a)+\varphi (b)$
2. $\varphi (a\cdot b)=\varphi (a)\cdot \varphi (b)$
3. $\varphi (1_A)=1_B$ (if $A$ and $B$ have multiplicative identities)

which implies :

1. $\ker (\varphi )$ is an ideal of $A$.
2. $\varphi$ is injective iff $\ker (\varphi )=\{0\}$.
3. $\text{range}(\varphi )$ is a subring of $B$.

If $\varphi$ is bijective (i.e., both injective and surjective), then $\varphi$ is called a ring isomorphism, and $A$ and $B$ are said to be isomorphic rings.

Ring Homomorphism Theorems

If $I\subseteq \ker (\varphi )$, then $\varphi$ induces a well-defined ring homomorphism $\bar{\varphi }:A/I\to B$ such that $\varphi =\bar{\varphi }\circ \pi$, where $\pi :A\to A/I$ is the canonical projection which sends $a\in A$ to $\bar{a}=a+I\in A/I$. The following diagram commutes:

$$\begin{array}{ccc}A& \stackrel{\varphi }{\to }& B\\ \downarrow \pi & & \Vert \\ A/I& \stackrel{\bar{\varphi }}{\to }& B\end{array}$$

Explanation

Why the commutative diagram holds? Because by definition, the equivalence of two functions $\varphi =\bar{\varphi }\circ \pi$ implies :

$$\mathrm{\forall }a\in A,\varphi (a)=\bar{\varphi }(\pi (a))=\bar{\varphi }(\bar{a})$$

This defines $\bar{\varphi }(\bar{a})=\varphi (a)$, and we need to check that it is well-defined. If $\bar{a}=\overline{a^{\prime }}$, then $a-a^{\prime }\in I\subseteq \ker (\varphi )$, so $\varphi (a)-\varphi (a^{\prime })=\varphi (a-a^{\prime })=0$. Hence the definition is independent of the representative. Preservation of addition, multiplication, and one follows from the corresponding properties of $\varphi$.

Lean 4 proof

def inducedHom {B : Type*} [CommRing B] (I : Ideal A) (f : A →+* B)
    (h : I ≤ RingHom.ker f) : A ⧸ I →+* B :=
  Ideal.Quotient.lift I f (fun _ ha => h ha)

theorem inducedHom_factorization {B : Type*} [CommRing B] (I : Ideal A)
    (f : A →+* B) (h : I ≤ RingHom.ker f) :
    (inducedHom I f h).comp (Ideal.Quotient.mk I) = f := by
  ext a
  exact Ideal.Quotient.lift_mk I f (fun _ ha => h ha)

Three theorems are particularly important in the study of ring homomorphisms:

1. First Isomorphism Theorem: If $\varphi :A\to B$ is a ring homomorphism, then $A/\ker (\varphi )\cong \text{range}(\varphi )$.

2. Second Isomorphism Theorem: If $A$ is a ring, $I$ and $J$ are ideals of $A$ with $I\subseteq J$, then $(A/I)/(J/I)\cong A/J$.

3. Third Isomorphism Theorem: If $I\subset A$ be an ideal, and let $B\subset A$ be a subring. Then :

   (a) $B+I\subset A$ is a subring containing $I$. (b) $I$ is an ideal of $B+I$. (c) $B\cap I$ is an ideal of $B$. Moreover,

   $$(B+I)/I\cong B/(B\cap I)$$

Proof

For the first isomorphism theorem, let $\bar{\varphi }:A/\ker (\varphi )\to \text{range}(\varphi )$ be defined by $\bar{\varphi }(a+\ker (\varphi ))=\varphi (a)$. In order to show the isomorphism, we need to prove :

• (a) $\bar{\varphi }$ is well-defined.
• (b) $\bar{\varphi }$ is a ring homomorphism.
• (c) $\bar{\varphi }$ is injective.
• (d) $\bar{\varphi }$ is surjective.

The factorization argument verifies (a) and (b). For (c), equality of the images of $a+\ker (\varphi )$ and $a^{\prime }+\ker (\varphi )$ means $\varphi (a-a^{\prime })=0$, hence the cosets are equal. For (d), every element of the range has the form $\varphi (a)$ and is the image of $a+\ker (\varphi )$.

---

For the second isomorphism theorem, let $\varphi :A/I\to A/J$ be a projection map defined by $\varphi (a+I)=a+J$. By the first isomorphism theorem, we need to show :

1. $\varphi$ is well-defined since $I\subseteq J$, and it is surjective because $b+J=\varphi (b+I)$ for every $b\in A$.
2. $\varphi (a+I)=0$ if and only if $a\in J$, so $\ker (\varphi )=J/I$.

Therefore, by the first isomorphism theorem, we have $(A/I)/(J/I)\cong A/J$, as required.

---

For the third isomorphism theorem, consider a composition map :

$$\varphi :B\to B+I\to (B+I)/I$$

Here $B+I=\{b+i\mid b\in B,i\in I\}$ is a subring: addition and negation preserve this form, $1=1+0$, and $(b+i)(b^{\prime }+i^{\prime })=b{b}^{\prime }+(b{i}^{\prime }+i{b}^{\prime }+i{i}^{\prime })$ with the parenthesized term in $I$. Restricting $I$ to $B+I$ gives an ideal, and restricting it to $B$ gives $B\cap I$.

The map is composed of the inclusion and the natural projection. It is surjective because each $(b+i)+I$ equals $b+I$, and its kernel is precisely $B\cap I$. By the first isomorphism theorem, we have :

$$B/(B\cap I)\cong (B+I)/I$$

Lean 4 proof

The numbering follows these notes; Mathlib calls the double-quotient result the third isomorphism theorem. Ideal.map represents $J/I$, and Ideal.comap restricts $I$ to a subring. Below, subringAddIdeal defines $B+I$ as the preimage of the image of $B$ in $A/I$; mem_subringAddIdeal verifies its usual description.

noncomputable def firstIsomorphism {B : Type*} [CommRing B] (f : A →+* B) :
    A ⧸ RingHom.ker f ≃+* f.range :=
  RingHom.quotientKerEquivRange f

def secondIsomorphism (I J : Ideal A) (h : I ≤ J) :
    (A ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* A ⧸ J :=
  DoubleQuot.quotQuotEquivQuotOfLE h

noncomputable def subringQuotientImage (I : Ideal A) (B : Subring A) :
    B ⧸ I.comap B.subtype ≃+* ((Ideal.Quotient.mk I).comp B.subtype).range := by
  let f := (Ideal.Quotient.mk I).comp B.subtype
  have hk : RingHom.ker f = I.comap B.subtype := by
    ext b
    exact Ideal.Quotient.eq_zero_iff_mem
  exact (Ideal.quotEquivOfEq hk.symm).trans (RingHom.quotientKerEquivRange f)

-- The preimage of the image of B under A → A/I is precisely B + I.
def subringAddIdeal (I : Ideal A) (B : Subring A) : Subring A :=
  ((Ideal.Quotient.mk I).comp B.subtype).range.comap (Ideal.Quotient.mk I)

theorem mem_subringAddIdeal (I : Ideal A) (B : Subring A) (a : A) :
    a ∈ subringAddIdeal I B ↔ ∃ b ∈ B, ∃ i ∈ I, a = b + i := by
  change (∃ b : B, Ideal.Quotient.mk I (b : A) = Ideal.Quotient.mk I a) ↔ _
  constructor
  · rintro ⟨b, hb⟩
    refine ⟨b, b.property, a - b, Ideal.Quotient.eq.mp hb.symm, ?_⟩
    ring
  · rintro ⟨b, hb, i, hi, rfl⟩
    refine ⟨⟨b, hb⟩, ?_⟩
    rw [map_add, Ideal.Quotient.eq_zero_iff_mem.mpr hi, add_zero]

def subringAddIdealProjection (I : Ideal A) (B : Subring A) :
    subringAddIdeal I B →+* ((Ideal.Quotient.mk I).comp B.subtype).range where
  toFun a := ⟨Ideal.Quotient.mk I a, a.property⟩
  map_zero' := Subtype.ext (map_zero _)
  map_one' := Subtype.ext (map_one _)
  map_add' a b := Subtype.ext (map_add (Ideal.Quotient.mk I) (a : A) (b : A))
  map_mul' a b := Subtype.ext (map_mul (Ideal.Quotient.mk I) (a : A) (b : A))

noncomputable def thirdIsomorphism (I : Ideal A) (B : Subring A) :
    B ⧸ I.comap B.subtype ≃+*
      (subringAddIdeal I B) ⧸ I.comap (subringAddIdeal I B).subtype := by
  let g := subringAddIdealProjection I B
  have hg : Function.Surjective g := by
    rintro ⟨x, b, rfl⟩
    refine ⟨⟨b, ?_⟩, rfl⟩
    exact ⟨b, rfl⟩
  have hk : RingHom.ker g = I.comap (subringAddIdeal I B).subtype := by
    ext a
    change (⟨Ideal.Quotient.mk I a, a.property⟩ :
      ((Ideal.Quotient.mk I).comp B.subtype).range) = 0 ↔ (a : A) ∈ I
    rw [Subtype.ext_iff]
    exact Ideal.Quotient.eq_zero_iff_mem
  let e := (Ideal.quotEquivOfEq hk.symm).trans
    (RingHom.quotientKerEquivOfSurjective hg)
  exact (subringQuotientImage I B).trans e.symm

Special Ideals

Let $I$ be an ideal of a ring $A$. Then :

1. $I$ is proper iff $A/I\ne 0$;
2. $I$ is maximal iff $A/I$ is a field.
3. $I$ is prime iff $A/I$ is an (integral) domain.
4. $I$ is radical iff $A/I$ is reduced.
5. If $I$ is proper, then $I$ is primary iff $\mathcal{N}(A/I)=\mathcal{D}(A/I)$.
6. If $I$ is maximal, then $I$ is prime.
7. If $I$ is prime, then $I$ is radical.
8. If $I$ is prime, then $I$ is primary.

Proof

For (1), $I$ is proper means $1\notin I$, equivalently $I\ne A$. This is equivalent to $1+I\ne 0+I$, hence to $A/I\ne 0$.

For (2), if $I$ is maximal and $a\notin I$, then $I+⟨a⟩=A$. Write $1=i+ba$ with $i\in I$; modulo $I$, this gives $(b+I)(a+I)=1+I$. Thus $A/I$ is a field; $a$ need not be invertible in $A$ itself. Conversely, if $A/I$ is a field and an ideal $J$ strictly contains $I$, choose $a\in J\setminus I$ and an inverse $b+I$ of $a+I$. Then $1-ab\in I\subseteq J$ and $ab\in J$, so $1\in J$ and $J=A$. Therefore $I$ is maximal.

For (3), by definition, $A/I$ is a domain means, for any non-zero element $a+I\in A/I$, there is not any non-zero $b+I\in A/I$ such that $(a+I)\cdot (b+I)=0$. In other words,

$$\begin{gathered} 0\ne a+I,0\ne b+I\to (a+I)\cdot (b+I)=ab+I\ne 0 \\ ⟺ab\in I\to a\in I\text{ or }b\in I. \end{gathered}$$

For (4), by definition, $A/I$ is reduced means it has no non-zero nilpotent elements. That is, for any $a+I\in A/I$, if $(a+I{)}^n=a^n+I=0$ for some $n\in {\mathbb{Z}}^{+}$, then $a+I=0$. Furthermore,

$$\begin{array}{rl}& a^n+I=0\to a+I=0\\ & ⟺a\in \sqrt{I}\to a\in I\\ & ⟺\sqrt{I}\subseteq I\end{array}$$

In previous sections, we have already concluded that $I\subseteq \sqrt{I}$, and hence $I=\sqrt{I}$. Therefore, $I$ is radical if and only if $A/I$ is reduced.

---

For (5), by definition of primary ideal :

$$I\text{ is primary }⟺ab\in I\to a\in I\text{ or }b\in \sqrt{I}$$

, the definition of $\mathcal{N}(A/I)$, we have:

$$\mathcal{N}(A/I)=\{\bar{a}\in A/I\mid \mathrm{\exists }n\in {\mathbb{Z}}^{+},{\bar{a}}^n=0\}$$

and the definition of $\mathcal{D}(A/I)$, we have:

$$\mathcal{D}(A/I)=\{\bar{a}\in A/I\mid \mathrm{\exists }\bar{b}\ne 0\in A/I,\bar{a}\cdot \bar{b}=0\}$$

Since $I$ is proper, $A/I$ is nonzero, and the earlier nilpotent-element argument gives $\mathcal{N}(A/I)\subseteq \mathcal{D}(A/I)$. Properness is essential: in the zero ring the only element is nilpotent, but there is no nonzero annihilator. So, we only need to show :

$$ab\in I\to a\in I\text{ or }b\in \sqrt{I}⟺\mathcal{D}(A/I)\subseteq \mathcal{N}(A/I)$$

For the backward direction, we need to show :

$$\mathcal{D}(A/I)\subseteq \mathcal{N}(A/I)⟹ab\in I\to a\in I\text{ or }b\in \sqrt{I}$$

Expanding the left-hand side, we have :

$$\mathcal{D}(A/I)\subseteq \mathcal{N}(A/I)⟺\mathrm{\forall }\bar{a}\in A/I,(\mathrm{\exists }\bar{b}\ne 0\in A/I,\bar{a}\cdot \bar{b}=0)\to (\mathrm{\exists }n\in {\mathbb{Z}}^{+},{\bar{a}}^n=0)$$

that is, for any $\bar{a}\in A/I$, if there exists $\bar{b}\in A/I$ such that $\bar{a}\cdot \bar{b}=0$, then there exists $n\in {\mathbb{Z}}^{+}$ such that ${\bar{a}}^n=0$. Two cases involved :

• case $\bar{a}=0⟺a\in I$, our goal always holds when we choose the left argument $\bar{a}=0$.

• case $\bar{a}\ne 0⟺a\notin I$, then proposition $\bar{a}\cdot \bar{b}=0$ implies that $\bar{b}\in \mathcal{D}(A/I)$, since $\mathcal{D}(A/I)\subseteq \mathcal{N}(A/I)$, we have $\bar{b}\in \mathcal{N}(A/I)$, i.e., $\mathrm{\exists }n\in {\mathbb{Z}}^{+},{\bar{b}}^n=\overline{b^n}=0⟺b^n\in I$. The right arugment $b\in \sqrt{I}$ always holds.

Proof complete for $\mathcal{D}(A/I)\subseteq \mathcal{N}(A/I)⟹ab\in I\to a\in I\text{ or }b\in \sqrt{I}$.

For the forward direction, if $\bar{b}$ is a zero divisor, choose $\bar{a}\ne 0$ with $\bar{a}\bar{b}=0$. Then $ab\in I$ and $a\notin I$, so primaryness implies $b\in \sqrt{I}$, equivalently $\bar{b}$ is nilpotent.

---

For (6), by (2), if $I$ is maximal, then $A/I$ is a field, thus $A/I$ must be a (integral) domain. By (3), it follows that $I$ is prime. Completing the proof.

For (7), by (3), $A/I$ is a (integral) domain, which implies $\mathcal{D}(A/I)=\{0\}$, and since $\mathcal{N}(A/I)\subseteq \mathcal{D}(A/I)$, we have $\mathcal{N}(A/I)=\{0\}$ ($A/I$ is reduced) as well. By (4), it follows that $I$ is radical.

For (8), by definition of prime ideal:

$$\begin{gathered} I\text{ is prime }⟺ab\in I\to a\in I\text{ or }b\in I \\ ⟺\bar{a}\cdot \bar{b}=0\to \bar{a}=0\text{ or }\bar{b}=0 \end{gathered}$$

, by definition of primary ideal :

$$\begin{gathered} I\text{ is primary }⟺ab\in I\to a\in I\text{ or }{b}^n\in I \\ ⟺\bar{a}\cdot \bar{b}=0\to \bar{a}=0\text{ or }{\bar{b}}^n=0 \end{gathered}$$

So, we need to show that :

$$\bar{a}\cdot \bar{b}=0\to \bar{a}=0\text{ or }\bar{b}=0⟹\bar{a}\cdot \bar{b}=0\to \bar{a}=0\text{ or }{\bar{b}}^n=0$$

Two cases involved :

$$\begin{gathered} \text{ (a) }\bar{a}=0⟹\bar{a}\cdot \bar{b}=0\to \bar{a}=0\text{ or }{\bar{b}}^n=0 \\ \text{ (b) }\bar{b}=0⟹\bar{a}\cdot \bar{b}=0\to \bar{a}=0\text{ or }{\bar{b}}^n=0 \end{gathered}$$

For case (a), it trivially holds when we choose the left argument $\bar{a}=0$.

For case (b), it trivially holds when we choose the right argument $\bar{b}=0$ for $n=1$.

Lean 4 proof

theorem proper_iff_nontrivial_quotient (I : Ideal A) :
    I ≠ ⊤ ↔ Nontrivial (A ⧸ I) :=
  Ideal.Quotient.nontrivial_iff.symm

theorem maximal_iff_field_quotient (I : Ideal A) :
    I.IsMaximal ↔ IsField (A ⧸ I) :=
  Ideal.Quotient.maximal_ideal_iff_isField_quotient I

theorem prime_iff_domain_quotient (I : Ideal A) :
    I.IsPrime ↔ IsDomain (A ⧸ I) :=
  (Ideal.Quotient.isDomain_iff_prime I).symm

theorem radical_iff_reduced_quotient (I : Ideal A) :
    I.IsRadical ↔ IsReduced (A ⧸ I) :=
  Ideal.isRadical_iff_quotient_reduced I

theorem nilpotent_mk_iff (I : Ideal A) (a : A) :
    IsNilpotent (Ideal.Quotient.mk I a) ↔ a ∈ I.radical := by
  simp only [IsNilpotent, Ideal.mem_radical_iff, ← map_pow,
    Ideal.Quotient.eq_zero_iff_mem]

theorem primary_iff_quotient_zeroDivisors (I : Ideal A) (hI : I ≠ ⊤) :
    I.IsPrimary ↔ ∀ x : A ⧸ I, IsNilpotent x ↔ IsZeroDivisor x := by
  letI : Nontrivial (A ⧸ I) := Ideal.Quotient.nontrivial_iff.mpr hI
  constructor
  · intro hp x
    constructor
    · exact isZeroDivisor_of_isNilpotent
    · rintro ⟨y, hy, hxy⟩
      obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
      obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective y
      have hba : b * a ∈ I := Ideal.Quotient.eq_zero_iff_mem.mp (by
        rw [map_mul, mul_comm]
        exact hxy)
      rcases (Ideal.isPrimary_iff.mp hp).2 hba with hb | ha
      · exact False.elim (hy (Ideal.Quotient.eq_zero_iff_mem.mpr hb))
      · exact (nilpotent_mk_iff I a).mpr ha
  · intro h
    refine Ideal.isPrimary_iff.mpr ⟨hI, ?_⟩
    intro a b hab
    by_cases ha : a ∈ I
    · exact Or.inl ha
    · right
      apply (nilpotent_mk_iff I b).mp
      apply (h _).mpr
      refine ⟨Ideal.Quotient.mk I a, ?_, ?_⟩
      · exact fun hz => ha (Ideal.Quotient.eq_zero_iff_mem.mp hz)
      · rw [← map_mul, mul_comm]
        exact Ideal.Quotient.eq_zero_iff_mem.mpr hab

theorem maximal_prime (I : Ideal A) (h : I.IsMaximal) : I.IsPrime :=
  h.isPrime

theorem prime_radical (I : Ideal A) (h : I.IsPrime) : I.IsRadical := by
  rintro x ⟨n, hn⟩
  exact h.mem_of_pow_mem n hn

theorem prime_primary (I : Ideal A) (h : I.IsPrime) : I.IsPrimary := by
  refine Ideal.isPrimary_iff.mpr ⟨h.ne_top, ?_⟩
  intro a b hab
  exact (h.mem_or_mem hab).imp id (fun hb => Ideal.le_radical hb)

Prime Avoidance Lemma

1. Let ${\mathfrak{p}}_1,\dots ,{\mathfrak{p}}_n$ be prime ideals of a commutative ring $A$. If an ideal $I$ of $A$ is contained in the union of these prime ideals, then $I$ is contained in one of them. This is known as the Prime Avoidance Lemma. That is,

$$I\subseteq \bigcup _{i=1}^n{\mathfrak{p}}_i⟹I\subseteq {\mathfrak{p}}_j\text{ for some }j\in \{1,\dots ,n\}.$$

2. Let $I_1,...,I_n$ be ideals, and let $\mathfrak{p}$ be a prime such that$$\bigcap _{i=1}^n{I}_i\subseteq \mathfrak{p}.$$Then $I_i\subseteq \mathfrak{p}$ for some $i\in \{1,\dots ,n\}$. Furthermore, if $\bigcap _{i=1}^n{I}_i=\mathfrak{p}$, then $I_i=\mathfrak{p}$ for some $i\in \{1,\dots ,n\}$.

3. Every prime ideal is irreducible.

Explanation

We use contrapositive way to prove these theorems, i,e. $p⟹Q⟺\mathrm{\neg }Q⟹\mathrm{\neg }p$.

Regarding (1), let's first consider a more simpler case when $n=2$. Let $b=a_1+a_2$, where $a_1\in {\mathfrak{p}}_1\setminus {\mathfrak{p}}_2$, and $a_2\in {\mathfrak{p}}_2\setminus {\mathfrak{p}}_1$. Then we have below proposition :

$$b\notin {\mathfrak{p}}_1,b\notin {\mathfrak{p}}_2⟹b\notin {\mathfrak{p}}_1\cup {\mathfrak{p}}_2$$

The argument (1) holds for any general ideals ${\mathfrak{p}}_i$, the primality is not a necessary condition for the case of $n=2$. So why do we need the primality?

Now, let's consider the general case when $n\ge 2$. A natural question arises: how to choose a proper $b$ such that $b\notin {\mathfrak{p}}_i$ for all $i\in \{1,\dots ,n\}$? There is a simple fact :

$$a\in {\mathfrak{p}}_i,b\notin {\mathfrak{p}}_i⟹a+b\notin {\mathfrak{p}}_i$$

Let $b=\sum _{i=1}^n\prod _{j\ne i}^n{a}_j$, where $a_j\in {\mathfrak{p}}_j$ and $a_j\notin {\mathfrak{p}}_i$ for all $i\ne j$. Then for the $i$-th term of $b$ ,

$$\prod _{j\ne i}^n{a}_j\notin {\mathfrak{p}}_i$$

it does not belong to ${\mathfrak{p}}_i$ since ${\mathfrak{p}}_i$ are prime and all factors of the product are not in ${\mathfrak{p}}_i$. And for other terms except the $i$-th one are belong to ${\mathfrak{p}}_i$ since one factor of each of these terms is in ${\mathfrak{p}}_i$. Therefore, $b\notin {\mathfrak{p}}_i$ for all $i\in \{1,\dots ,n\}$, moreover $b\notin \bigcup _{i=1}^n{\mathfrak{p}}_i$.

As shown in the above figure, the $i$-th term of $b$, $a_1\cdot a_2$, is not in ${\mathfrak{p}}_i$. This mainly owe to the primality of ${\mathfrak{p}}_i$ which ensures that the product of elements not in ${\mathfrak{p}}_i$ is also not in ${\mathfrak{p}}_i$.

---

Regarding (2), let $J={\cap }_i{I}_i$, the contrapositive way to show the statement is to prove

$$\begin{array}{rl}& \mathrm{\neg }(\mathrm{\exists }i\le n,I_i\subseteq \mathfrak{p})⟹\mathrm{\neg }(J\subseteq \mathfrak{p})\\ & ⟺(\mathrm{\forall }i\le n,\mathrm{\exists }{a}_i\in I_i,a_i\notin \mathfrak{p})⟹\mathrm{\exists }x\in J,x\notin \mathfrak{p}\end{array}$$

We use $x=\prod _{i=1}^n{a}_i$ where $a_i\in I_i$ and $a_i\notin \mathfrak{p}$. By the definition of ideal, $x\in {\cap }_i{I}_i=J$. And since $\mathfrak{p}$ is prime and none of the $a_i$ are in $\mathfrak{p}$, it follows that $x\notin \mathfrak{p}$. This completes the proof of the contrapositive.

As shown in the above figure, $x=a_1\cdot a_2\cdot a_3\in {\cap }_i{I}_i$ but $x\notin \mathfrak{p}$, this mainly owe to the primality of $\mathfrak{p}$ which ensures that the product of elements not in $\mathfrak{p}$ is also not in $\mathfrak{p}$.

---

For (3), we wan to show :

$$\begin{array}{rl}& \mathfrak{p}\text{ is prime}⟹\mathfrak{p}\text{ is irreducible}\\ & ⟺\mathfrak{p}\text{ is prime}⟹I=I_1\cap I_2,I_1\subseteq I\text{ or }{I}_2\subseteq I\end{array}$$

Since $I=I_1\cap I_2$, then $\mathrm{\forall }x\in I$, we have $\mathrm{\exists }a\in I_1,b\in I_2$ such that $x=a\cdot b$. By $I$ is prime, we have $a\in I$ or $b\in I$, which implies $I_1\subseteq I$ or $I_2\subseteq I$. This completes the proof.