Module

MvPolynomial_exists_ne_zero_common_zero_of_card_lt.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_ne_zero_common_zero_of_card_lt

1 declaration indexed from sourceView source ↗

Module documentation

A nontrivial common zero with fewer equations than variables

This is the dimension-theoretic input to the Riemann--Roch proof of Tsen's theorem. It strengthens the homogeneous case in Stacks Project, Tag 03RB: the equations need only vanish at the origin. https://stacks.math.columbia.edu/tag/03RB

The proof reuses the existing maximal-ideal dimension theorem, together with the Nullstellensatz and Krull's height theorem.

Imports5

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_add_ringKrullDim_quotient_eq_ringKrullDim_of_finiteType
Mathlib.RingTheory.Nullstellensatz
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Mathlib.Tactic.NormNum

Imported by2

theorem

exists_ne_zero_common_zero_of_card_lt

L36 ↗

MvPolynomial.exists_ne_zero_common_zero_of_card_lt

Documentation

Fewer equations than variables cannot cut out only the origin over an algebraically closed field, if all equations vanish at the origin.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
open Ideal_height_add_ringKrullDim_quotient_eq_ringKrullDim_of_finiteType
namespace MvPolynomial

Lean source · statement

theorem exists_ne_zero_common_zero_of_card_lt
    {K : Type u} [Field K] [IsAlgClosed K]
    {s n : ℕ} (f : Fin s → MvPolynomial (Fin n) K)
    (hf : ∀ i : Fin s, aeval (0 : Fin n → K) (f i) = 0)
    (hsn : s < n) :
    ∃ x : Fin n → K, x ≠ 0 ∧ ∀ i : Fin s, aeval x (f i) = 0

Module documentation

A nontrivial common zero with fewer equations than variables

Declarations

exists_ne_zero_common_zero_of_card_lt