$\sqrt J$ as an intersection of maximal ideals

Proved

Nullstellensatz.radical_eq_sInf_maximal_eq_iInf_pointIdeal

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycommutative-algebra

Let $K$ be algebraically closed and $J$ an ideal of $K[X_1,\dots,X_n]$ . Then

\sqrt J = \bigcap_{\mathfrak m \supseteq J} \mathfrak m = \bigcap_{(a_1,\dots,a_n) \in \mathrm V(J)} (X_1 - a_1, \dots, X_n - a_n),

where the first intersection is over the maximal ideals $\mathfrak m$ containing $J$ .

Formalization Note. An empty intersection is the whole ring, which is the correct value when $J$ is the whole ring.

Preamble

import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial

Formal statement

namespace Nullstellensatz

theorem radical_eq_sInf_maximal_eq_iInf_pointIdeal {K : Type*} [Field K] [IsAlgClosed K]
    {n : ℕ} (J : Ideal (MvPolynomial (Fin n) K)) :
    J.radical = sInf {m | J ≤ m ∧ m.IsMaximal} ∧
      J.radical = ⨅ a ∈ zeroSet J, pointIdeal a := by sorry

end Nullstellensatz

Source

Wikipedia, article "Hilbert's Nullstellensatz" (snapshot supplied as Hilbert's_Nullstellensatz.pdf, printed 2026-09-27), https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz, section "Formulations", last display (sqrt J as intersections over maximal ideals and over points of V(J)).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence that the statement is faithful.

Let $K$ be algebraically closed, $n \in \mathbb N$ , $J$ an ideal of $K[X_1,\dots,X_n]$ . Two equalities of ideals:

$\sqrt J$ equals the intersection of all maximal ideals $\mathfrak m$ with $J \subseteq \mathfrak m$ ;
$\sqrt J$ equals the intersection, over all points $a \in \mathrm V(J)$ , of the ideals generated by $X_1 - a_1,\dots,X_n - a_n$ .

An intersection over an empty family is the whole ring.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

J\sqrt JJ​ as an intersection of maximal ideals

$\sqrt J$ as an intersection of maximal ideals