English
Let R be a domain and σ a finite index set. Suppose S : σ → Finset R are nonempty, and f is a multivariate polynomial in the σ-variables with coefficients in R. If f vanishes at every point x ∈ σ → R with x(i) ∈ S(i) for all i, then f can be written as a linear combination f = sum_i [ (∏_{s ∈ S(i)} (X_i − C s)) · h_i ] where each h_i is a polynomial in the σ-variables with coefficients in R, and for every i the total degree of (∏_{s ∈ S(i)} (X_i − C s)) h_i does not exceed deg(f).
Русский
Пусть R – интегральный домен, σ – конечное множество индексов. Пусть S : σ → Finset R непусты, и f ∈ R[X_i : i ∈ σ] – многочлен. Если f обращается в нуль при любом x ∈ ∏_{i} S(i) (то есть x(i) ∈ S(i) для всех i), то f можно записать в виде f = ∑_i (∏_{s ∈ S(i)} (X_i − C(s))) · h_i, где h_i ∈ R[ X_j : j ∈ σ ], причем для каждого i выполнено равенство deg((∏_{s ∈ S(i)} (X_i − C(s)) · h_i)) ≤ deg(f).
LaTeX
$$$\\exists h : σ \\to_{0} \\text{MvPolynomial } σ R,\\; (\\forall i, ((\\prod_{s \\in S(i)} (X_i - C s)) * h i).totalDegree \\le f.totalDegree) \\; \\wedge\\; f = \\text{linearCombination } (MvPolynomial \\ σ R) (fun i \\mapsto \\prod_{r \\in S i} (X i - C r)) h$$$
Lean4
/-- 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 combinatorial_nullstellensatz_exists_linearCombination [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 = linearCombination (MvPolynomial σ R) (fun i ↦ ∏ r ∈ S i, (X i - C r)) h :=
by
letI : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
obtain ⟨h, r, hf, hh, hr⟩ :=
degLex.div (b := fun i ↦ Alon.P (S i) i) (fun i ↦ by simp only [(Alon.monic_P ..).leadingCoeff_eq_one, isUnit_one])
f
use h
suffices r = 0 by
rw [this, add_zero] at hf
exact ⟨fun i ↦ degLex_totalDegree_monotone (hh i), hf⟩
apply eq_zero_of_eval_zero_at_prod_finset r S
· intro i
rw [degreeOf_eq_sup, Finset.sup_lt_iff (by simp [Sne i])]
intro c hc
rw [← not_le]
intro h'
apply hr c hc i
intro j
rw [Alon.degree_P, single_apply]
split_ifs with hj
· rw [← hj]
exact h'
· exact zero_le _
· intro x hx
rw [Iff.symm sub_eq_iff_eq_add'] at hf
rw [← hf, map_sub, Heval x hx, zero_sub, neg_eq_zero, linearCombination_apply, map_finsuppSum, Finsupp.sum,
Finset.sum_eq_zero]
intro i _
rw [smul_eq_mul, map_mul]
convert mul_zero _
rw [Alon.P, map_prod]
apply Finset.prod_eq_zero (hx i)
simp
