Documentation

Mathlib.Combinatorics.Nullstellensatz

Alon's Combinatorial Nullstellensatz #

This is a formalization of Noga Alon's Combinatorial Nullstellensatz. It follows [Alo99].

We consider a family S : σ → Finset R of finite subsets of a domain R and a multivariate polynomial f in MvPolynomial σ R. The combinatorial Nullstellensatz gives combinatorial constraints for the vanishing of f at any x : σ → R such that x s ∈ S s for all s.

TODO #

References #

theorem MvPolynomial.eq_zero_of_eval_zero_at_prod_finset {R : Type u_1} [CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (P : MvPolynomial σ R) (S : σFinset R) (Hdeg : ∀ (i : σ), degreeOf i P < (S i).card) (Heval : ∀ (x : σR), (∀ (i : σ), x i S i)(eval x) P = 0) :
P = 0

A multivariate polynomial that vanishes on a large product finset is the zero polynomial.

theorem MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination {R : Type u_1} [CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (S : σFinset R) (Sne : ∀ (i : σ), (S i).Nonempty) (f : MvPolynomial σ R) (Heval : ∀ (x : σR), (∀ (i : σ), x i S i)(eval x) f = 0) :
∃ (h : σ →₀ MvPolynomial σ R), (∀ (i : σ), ((∏ sS i, (X i - C s)) * h i).totalDegree f.totalDegree) f = (Finsupp.linearCombination (MvPolynomial σ R) fun (i : σ) => rS i, (X i - C r)) h

The Combinatorial Nullstellensatz.

If f vanishes at every point x : σ → R such that x s ∈ S s for all s, then it can be written as a linear combination f = linearCombination (MvPolynomial σ R) (fun i ↦ (∏ r ∈ S i, (X i - C r))) h, for some h : σ →₀ MvPolynomial σ R such that ((∏ r ∈ S s, (X i - C r)) * h i).totalDegree ≤ f.totalDegree for all s.

[Alo99], theorem 1.

theorem MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero {R : Type u_1} [CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (f : MvPolynomial σ R) (t : σ →₀ ) (ht : coeff t f 0) (ht' : f.totalDegree = t.degree) (S : σFinset R) (htS : ∀ (i : σ), t i < (S i).card) :
∃ (s : σR), (∀ (i : σ), s i S i) (eval s) f 0

The Combinatorial Nullstellensatz.

Given a multi-index t : σ →₀ ℕ such that t s < (S s).card for all s, f.totalDegree = t.degree and f.coeff t ≠ 0, there exists a point x : σ → R such that x s ∈ S s for all s and f.eval s ≠ 0.

[Alo99], theorem 2