Algebraic sets correspond to radical ideals

Proved

Nullstellensatz.algebraicSet_radicalIdeal_correspondence

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

algebraic-geometrycommutative-algebra

Let $K$ be algebraically closed. The map $J \mapsto \mathrm V(J)$ is an order-reversing bijection from the radical ideals of $K[X_1,\dots,X_n]$ onto the algebraic sets in $K^n$ , with inverse $W \mapsto \mathrm I(W)$ . Precisely:

$\mathrm V$ maps radical ideals to algebraic sets, injectively and surjectively;
$J_1 \subseteq J_2 \implies \mathrm V(J_2) \subseteq \mathrm V(J_1)$ ;
$\mathrm I(\mathrm V(J)) = J$ for every radical ideal $J$ ;
$\mathrm V(\mathrm I(W)) = W$ for every algebraic set $W$ .

This is the dictionary between affine geometry over $K$ and radical ideals.

Preamble

import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial

Formal statement

namespace Nullstellensatz

theorem algebraicSet_radicalIdeal_correspondence {K : Type*} [Field K] [IsAlgClosed K] {n : ℕ} :
    Set.BijOn (zeroSet (K := K) (n := n)) {J | J.IsRadical} {W | IsAlgebraicSet W} ∧
    (∀ J₁ J₂ : Ideal (MvPolynomial (Fin n) K), J₁ ≤ J₂ → zeroSet J₂ ⊆ zeroSet J₁) ∧
    (∀ J : Ideal (MvPolynomial (Fin n) K), J.IsRadical → vanishingIdeal (zeroSet J) = J) ∧
    (∀ W : Set (Fin n → K), IsAlgebraicSet W → zeroSet (vanishingIdeal W) = W) := 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", paragraph 5 (order-reversing bijective correspondence between algebraic sets and radical ideals).

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 and $n \in \mathbb N$ . Four claims are asserted together.

The map $J \mapsto \mathrm V(J)$ , restricted to the set of radical ideals $J$ of $K[X_1,\dots,X_n]$ (ideals with $p^r \in J \Rightarrow p \in J$ ), sends each radical ideal to an algebraic subset of $K^n$ , is injective on radical ideals, and every algebraic subset of $K^n$ is $\mathrm V(J)$ for some radical $J$ .
For all ideals $J_1 \subseteq J_2$ : $\mathrm V(J_2) \subseteq \mathrm V(J_1)$ .
For every radical ideal $J$ : $\mathrm I(\mathrm V(J)) = J$ .
For every algebraic set $W$ (i.e. $W = \mathrm V(J')$ for some ideal $J'$ ): $\mathrm V(\mathrm I(W)) = W$ .

The whole ring counts as a radical ideal and corresponds to $\emptyset$ .

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