English
Let f ∈ R[σ] be a polynomial with a distinguished multi-index t ∈ σ → Fin ℕ such that the coefficient f_t ≠ 0 and total degree deg f equals deg t. If |S(i)| > t(i) for each i, then there exists a point s ∈ ∏_i S(i) with f(s) ≠ 0.
Русский
Пусть f принадлежит R[σ], и дан многомерный индекс t ∈ σ → Fin ℕ such that коэффициент f_t ≠ 0 и deg f = deg t. Если для каждого i выполняется |S(i)| > t(i), то существует точка s ∈ ∏_i S(i), такая что f(s) ≠ 0.
LaTeX
$$$\\forall f ∈ MvPolynomial\\, σ \\, R\\, \\forall t ∈ σ \\to_{0} \\mathbb{N},\\; f.coeff t \\ne 0 \\land f.totalDegree = t.degree \\Rightarrow \\forall S : σ → Finset R, (\\forall i, t i < #(S i))\\Rightarrow ∃ s: σ → R, (∀ i, s i ∈ S i) ∧ eval s f ≠ 0$$$
Lean4
/-- 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 -/
theorem combinatorial_nullstellensatz_exists_eval_nonzero [IsDomain R] (f : MvPolynomial σ R) (t : σ →₀ ℕ)
(ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree) (S : σ → Finset R) (htS : ∀ i, t i < #(S i)) :
∃ s : σ → R, (∀ i, s i ∈ S i) ∧ eval s f ≠ 0 :=
by
let _ : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
classical
by_contra Heval
apply ht
push_neg at Heval
obtain ⟨h, hh, hf⟩ :=
combinatorial_nullstellensatz_exists_linearCombination S
(fun i ↦ by rw [← Finset.card_pos]; exact Nat.zero_lt_of_lt (htS i)) f Heval
rw [hf]
rw [linearCombination_apply, Finsupp.sum, coeff_sum]
apply Finset.sum_eq_zero
intro i _
set g := h i * Alon.P (S i) i with hg
by_cases hi : h i = 0
· simp [hi]
have : g.totalDegree ≤ f.totalDegree := by
rw [hg, mul_comm]
exact hh i
rw [hg, ← degree_degLexDegree,
degree_mul_of_isRegular_right hi (by simp only [(Alon.monic_P ..).leadingCoeff_eq_one, isRegular_one]),
Alon.degree_P, degree_add, degree_degLexDegree, degree_single, ht'] at this
rw [smul_eq_mul, coeff_mul, Finset.sum_eq_zero]
rintro ⟨p, q⟩ hpq
simp only [Finset.mem_antidiagonal] at hpq
simp only [mul_eq_zero, Classical.or_iff_not_imp_right]
rw [← ne_eq, ← mem_support_iff]
intro hq
obtain ⟨e, hq', hq⟩ := Alon.of_mem_P_support _ _ _ hq
apply coeff_eq_zero_of_totalDegree_lt
rw [← Finsupp.degree]
apply lt_of_add_lt_add_right (lt_of_le_of_lt this _)
rw [← hpq, degree_add, add_lt_add_iff_left, hq, degree_single]
apply lt_of_le_of_lt _ (htS i)
simp [← hpq, hq]
