Alon's Combinatorial Nullstellensatz

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

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.

• MvPolynomial.eq_zero_of_eval_zero_at_prod_finset : if f vanishes at any such point and f.degreeOf s < #(S s) for all s, then f = 0.

• combinatorial_nullstellensatz_exists_linearCombination If f vanishes at every such point, 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.

• combinatorial_nullstellensatz_exists_eval_nonzero 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.

TODO

• Applications
• relation with Schwartz–Zippel lemma, as in [Rote_2023]

References

• [Alon, Combinatorial Nullstellensatz][Alon_1999]

• [Rote, The Generalized Combinatorial Lason-Alon-Zippel-Schwartz Nullstellensatz Lemma][Rote_2023]

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 : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧ f = (Finsupp.linearCombination (MvPolynomial σ R) fun (i : σ) => ∏ r ∈ S 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.

[Alon_1999], 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.

[Alon_1999], theorem 2