English
If I is a maximal ideal of MvPolynomial σ k, then there exists x: σ → K with I = vanishingIdeal k {x}.
Русский
Если I — максимальный идеал MvPolynomial σ k, то существует x: σ → K such that I = vanishingIdeal k {x}.
LaTeX
$$∃ x : σ → K, I = vanishingIdeal k { x }$$
Lean4
theorem eq_vanishingIdeal_singleton_of_isMaximal {I : Ideal (MvPolynomial σ k)} (hI : I.IsMaximal) :
∃ x : σ → K, I = vanishingIdeal k { x } :=
by
let : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
have : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I) :=
by
rw [Algebra.isAlgebraic_iff_isIntegral, ← algebraMap_isIntegral_iff]
exact
MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
let φ : (MvPolynomial σ k ⧸ I) →ₐ[k] K := IsAlgClosed.lift
let x : σ → K := fun s => φ (Ideal.Quotient.mk I (X s))
have : aeval x = φ.comp (Quotient.mkₐ k I) := by ext; simp [x]
use x
simp [Ideal.ext_iff, this, Ideal.Quotient.eq_zero_iff_mem]
