Prove2Me

Vanishing ideals of sets of complex points agree in C[X,Y]\mathbb C[X,Y] and in Spec⁡C[X,Y]\operatorname{Spec}\mathbb C[X,Y]

Proved
CurveSymmetry.spectrum_vanishingIdeal_image

by carlok · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycurve-symmetry-leaneuclidean-geometry

For v=(v0,v1)∈C2v=(v_0,v_1)\in\mathbb C^2 let mv={Q∈C[X,Y]:Q(v)=0}\mathfrak m_v=\{Q\in\mathbb C[X,Y]:Q(v)=0\} be the kernel of evaluation at vv, that is, the maximal ideal (X−v0, Y−v1)(X-v_0,\,Y-v_1), regarded as a point of the prime spectrum Spec⁡C[X,Y]\operatorname{Spec}\mathbb C[X,Y]. The vanishing ideal of a set of prime ideals is their intersection, the whole ring for the empty set.

Then for every subset S⊆C2S\subseteq\mathbb C^2

⋂v∈Smv={Q∈C[X,Y]: Q(v)=0 for all v∈S}.\bigcap_{v\in S}\mathfrak m_v=\{Q\in\mathbb C[X,Y]:\ Q(v)=0\ \text{for all}\ v\in S\}.

It translates between the classical vanishing ideal of a set of complex points and the vanishing ideal, in Spec⁡C[X,Y]\operatorname{Spec}\mathbb C[X,Y], of the corresponding closed points. The formalization uses it to compute Zariski closures in the prime spectrum from classical vanishing ideals, for instance the closure of the real points of the curve (6).

Formalization Note: the left side is PrimeSpectrum.vanishingIdeal of the image of SS under v↦mvv\mapsto\mathfrak m_v, and the right side is MvPolynomial.vanishingIdeal ℂ S.

Preamble
import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Definitions.Def_CurveSymmetry_03_IsometriesAndCharts
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.RingTheory.MvPolynomial.Homogeneous
import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
import Mathlib.RingTheory.Nullstellensatz
import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.RingTheory.RootsOfUnity.Complex
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
import Mathlib.RingTheory.Spectrum.Prime.Topology
import Mathlib.Tactic

open CurveSymmetry
set_option autoImplicit false
open MvPolynomial
Formal statement
theorem CurveSymmetry.spectrum_vanishingIdeal_image (S : Set (Fin 2 → ℂ)) :
    PrimeSpectrum.vanishingIdeal (affineSpectrumPoint '' S) = vanishingIdeal ℂ S := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for Section 3, closure of equation (6), p. 3, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/AffineClosure.lean (C. Perassi)

View graph