Prove2Me

Maximal ideals of K[X1,…,Xn]K[X_1,\dots,X_n]

Proved
Nullstellensatz.isMaximal_iff_eq_pointIdeal

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

algebraic-geometrycommutative-algebra

Let KK be algebraically closed. An ideal m\mathfrak m of K[X1,…,Xn]K[X_1,\dots,X_n] is maximal if and only if

m=(X1−a1,…,Xn−an)for some a=(a1,…,an)∈Kn.\mathfrak m = (X_1 - a_1, \dots, X_n - a_n) \quad \text{for some } a = (a_1,\dots,a_n) \in K^n.

This characterisation of maximal ideals is another common formulation of the weak Nullstellensatz.

Preamble
import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial
Formal statement
namespace Nullstellensatz

theorem isMaximal_iff_eq_pointIdeal {K : Type*} [Field K] [IsAlgClosed K] {n : ℕ}
    (m : Ideal (MvPolynomial (Fin n) K)) :
    m.IsMaximal ↔ ∃ a : Fin n → K, m = 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", paragraph 6 (every maximal ideal is of the form (X_1 - a_1, ..., X_n - a_n)); also section "Proofs / Using Zariski's lemma".
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 KK be algebraically closed, n∈Nn \in \mathbb N, and m\mathfrak m an ideal of K[X1,…,Xn]K[X_1,\dots,X_n]. Then m\mathfrak m is maximal if and only if there exists a∈Kna \in K^n with m\mathfrak m equal to the ideal generated by X1−a1,…,Xn−anX_1 - a_1,\dots,X_n - a_n.

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