feat(Combinatorics/Nullstellensatz): formalize Alon's Combinatorial Nullstellensatz

Mathlib.lean

@@ -2421,6 +2421,7 @@ import Mathlib.Combinatorics.HalesJewett
 import Mathlib.Combinatorics.Hall.Basic
 import Mathlib.Combinatorics.Hall.Finite
 import Mathlib.Combinatorics.Hindman
+import Mathlib.Combinatorics.Nullstellensatz
 import Mathlib.Combinatorics.Optimization.ValuedCSP
 import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Combinatorics.Quiver.Arborescence

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -319,6 +319,58 @@ lemma optionEquivLeft_X_none : optionEquivLeft R S₁ (X none) = Polynomial.X :=
 lemma optionEquivLeft_C (r : R) : optionEquivLeft R S₁ (C r) = Polynomial.C (C r) := by
   simp only [optionEquivLeft_apply, aeval_C, Polynomial.algebraMap_apply, algebraMap_eq]
 
+theorem optionEquivLeft_monomial (m : Option S₁ →₀ ℕ) (r : R) :
+    optionEquivLeft R S₁ (monomial m r) = .monomial (m none) (monomial m.some r) := by
+  rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
+  · rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]
+    simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
+      map_mul, mul_assoc]
+    apply congr_arg₂ _ rfl
+    simp only [mul_comm, map_finsupp_prod, map_pow]
+  · intros; simp
+  · intros; rw [pow_add]
+
+/-- The coefficient of `n.some` in the `n none`-th coefficient of `optionEquivLeft R S₁ f`
+equals the coefficient of `n` in `f` -/
+theorem optionEquivLeft_coeff_coeff (n : Option S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R) :
+    coeff n.some (Polynomial.coeff (optionEquivLeft R S₁ f) (n none)) =
+      coeff n f := by
+  induction' f using MvPolynomial.induction_on' with j r p q hp hq generalizing n
+  swap
+  · simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
+  · rw [optionEquivLeft_monomial]
+    classical
+    simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
+    simp only [coeff_zero]
+    by_cases hj : j = n
+    · simp [hj]
+    · rw [if_neg hj]
+      simp only [ite_eq_right_iff]
+      intro hj_none hj_some
+      apply False.elim (hj _)
+      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
+      simpa only [Finsupp.ext_iff] using hj_some
+
+theorem optionEquivLeft_elim_eval (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R) :
+    eval (fun x ↦ Option.elim x y s) f =
+      Polynomial.eval y (Polynomial.map (eval s) (optionEquivLeft R S₁ f)) := by
+  -- turn this into a def `Polynomial.mapAlgHom`
+  let φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
+    { Polynomial.mapRingHom (eval s) with
+      commutes' := fun r => by
+        convert Polynomial.map_C (eval s)
+        exact (eval_C _).symm }
+  show
+    aeval (fun x ↦ Option.elim x y s) f =
+      (Polynomial.aeval y).comp (φ.comp (optionEquivLeft _ _).toAlgHom) f
+  congr 2
+  apply MvPolynomial.algHom_ext
+  rw [Option.forall]
+  simp only [aeval_X, Option.elim_none, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp,
+    Polynomial.coe_aeval_eq_eval, AlgHom.coe_mk, coe_mapRingHom, AlgHom.coe_coe, comp_apply,
+    optionEquivLeft_apply, Polynomial.map_X, Polynomial.eval_X, Option.elim_some, Polynomial.map_C,
+    eval_X, Polynomial.eval_C, implies_true, and_self, φ]
+
 end
 
 /-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
@@ -437,7 +489,7 @@ theorem eval_eq_eval_mv_eval' (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (
     RingHom.coe_mk, MonoidHom.coe_coe, AlgHom.coe_coe, implies_true, and_self,
     RingHom.toMonoidHom_eq_coe]
 
-theorem coeff_eval_eq_eval_coeff (s' : Fin n → R) (f : Polynomial (MvPolynomial (Fin n) R))
+theorem coeff_eval_eq_eval_coeff (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R))
     (i : ℕ) : Polynomial.coeff (Polynomial.map (eval s') f) i = eval s' (Polynomial.coeff f i) := by
   simp only [Polynomial.coeff_map]
 

Mathlib/Combinatorics/Nullstellensatz.lean

@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2024 Antoine Chambert-Loir. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Loir
+-/
+import Mathlib.Algebra.MvPolynomial.Equiv
+import Mathlib.Algebra.Polynomial.Degree.Definitions
+import Mathlib.Data.Finsupp.MonomialOrder.DegLex
+import Mathlib.RingTheory.Ideal.Maps
+import Mathlib.RingTheory.MvPolynomial.Groebner
+import Mathlib.RingTheory.MvPolynomial.Homogeneous
+import Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
+
+/-! # 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]
+
+-/
+
+open Finsupp
+
+open scoped Finset
+
+variable {R : Type*} [CommRing R]
+
+namespace MvPolynomial
+
+open Finsupp Function
+
+/-- A multivariate polynomial that vanishes on a large product finset is the zero polynomial. -/
+theorem eq_zero_of_eval_zero_at_prod_finset {σ : Type*} [Finite σ] [IsDomain R]
+    (P : MvPolynomial σ R) (S : σ → Finset R)
+    (Hdeg : ∀ i, P.degreeOf i < #(S i))
+    (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x P = 0) :
+    P = 0 := by
+  induction σ using Finite.induction_empty_option with
+  | @of_equiv σ τ e h =>
+    suffices MvPolynomial.rename e.symm P = 0 by
+      have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)
+      rw [RingHom.injective_iff_ker_eq_bot] at that
+      rwa [← RingHom.mem_ker, that] at this
+    apply h _ (fun i ↦ S (e i))
+    · intro i
+      classical
+      convert Hdeg (e i)
+      conv_lhs => rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]
+    · intro x hx
+      simp only [MvPolynomial.eval_rename]
+      apply Heval
+      intro s
+      simp only [Function.comp_apply]
+      convert hx (e.symm s)
+      simp only [Equiv.apply_symm_apply]
+  | h_empty =>
+    suffices P = C (constantCoeff P) by
+      specialize Heval default (fun i ↦ PEmpty.elim i)
+      rw [this, eval_C] at Heval
+      rw [this, Heval, C_0]
+    ext m
+    suffices m = 0 by simp [this, ← constantCoeff_eq]
+    ext d; exact PEmpty.elim d
+  | @h_option σ _ h =>
+    set Q := optionEquivLeft R σ P with hQ
+    suffices Q = 0 by
+      rw [← AlgEquiv.symm_apply_apply (optionEquivLeft R σ) P, ← hQ, this, map_zero]
+    have Heval' (x : σ → R) (hx : ∀ i, x i ∈ S (some i)) : Polynomial.map (eval x) Q = 0 := by
+      apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ (S none)
+      · intro y hy
+        rw [← optionEquivLeft_elim_eval]
+        apply Heval
+        simp only [Option.forall, Option.elim_none, hy, Option.elim_some, hx, implies_true,
+          and_self]
+      · apply lt_of_le_of_lt _ (Hdeg none)
+        rw [Polynomial.natDegree_le_iff_coeff_eq_zero]
+        intro d hd
+        simp only [hQ]
+        rw [MvPolynomial.coeff_eval_eq_eval_coeff]
+        convert map_zero (MvPolynomial.eval x)
+        ext m
+        simp only [coeff_zero, optionEquivLeft_coeff_coeff]
+        set n := embDomain Function.Embedding.some m + Finsupp.single none d with hn
+        rw [option_embedding_add_single] at hn
+        rw [← hn.1, ← hn.2, optionEquivLeft_coeff_coeff]
+        by_contra hm
+        apply not_le.mpr hd
+        rw [MvPolynomial.degreeOf_eq_sup]
+        rw [← ne_eq, ← MvPolynomial.mem_support_iff] at hm
+        convert Finset.le_sup hm
+        exact hn.1.symm
+    ext m d
+    simp only [Polynomial.coeff_zero, coeff_zero]
+    suffices Q.coeff m = 0 by simp only [this, coeff_zero]
+    apply h _ (fun i ↦ S (some i))
+    · intro i
+      apply lt_of_le_of_lt _ (Hdeg (some i))
+      simp only [degreeOf_eq_sup, Finset.sup_le_iff, mem_support_iff, ne_eq]
+      intro e he
+      set n : Option σ →₀ ℕ := embDomain Function.Embedding.some e + Finsupp.single none m with hn
+      rw [option_embedding_add_single] at hn
+      rw [hQ, ← hn.1, ← hn.2, optionEquivLeft_coeff_coeff, ← ne_eq,
+        ← MvPolynomial.mem_support_iff] at he
+      convert Finset.le_sup he
+      rw [← hn.2, some_apply]
+    · intro x hx
+      specialize Heval' x hx
+      rw [Polynomial.ext_iff] at Heval'
+      simpa only [Polynomial.coeff_map, Polynomial.coeff_zero] using Heval' m
+
+open MonomialOrder
+
+/- Here starts the actual proof of the combinatorial Nullstellensatz -/
+
+variable {σ : Type*}
+
+/-- The polynomial in `X i` that vanishes at all elements of `S`. -/
+private noncomputable def Alon.P (S : Finset R) (i : σ) : MvPolynomial σ R :=
+  ∏ r ∈ S, (X i - C r)
+
+/-- The degree of `Alon.P S i` with respect to `X i` is the cardinality of `S`,
+  and `0` otherwise. -/
+private theorem Alon.degree_P [Nontrivial R] (m : MonomialOrder σ) (S : Finset R) (i : σ) :
+    m.degree (Alon.P S i) = single i #S := by
+  simp only [P]
+  rw [degree_prod_of_regular]
+  · simp [Finset.sum_congr rfl (fun r _ ↦ m.degree_X_sub_C i r)]
+  · intro r _
+    rw [m.monic_X_sub_C]
+    exact isRegular_one
+
+/-- The leading coefficient of `Alon.P S i` is `1`. -/
+private theorem Alon.monic_P [Nontrivial R] (m : MonomialOrder σ) (S : Finset R) (i : σ) :
+    m.Monic (P S i) :=
+  Monic.prod (fun r _ ↦ m.monic_X_sub_C i r)
+
+/-- The support of `Alon.P S i` is the set of exponents of the form `single i e`,
+  for `e ≤ S.card`. -/
+private lemma Alon.of_mem_P_support {ι : Type*} (i : ι) (S : Finset R) (m : ι →₀ ℕ)
+    (hm : m ∈ (Alon.P S i).support) :
+    ∃ e ≤ S.card, m = single i e := by
+  classical
+  have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P, map_prod]
+  rw [hP, support_rename_of_injective (Function.injective_of_subsingleton _)] at hm
+  simp only [Finset.mem_image, mem_support_iff, ne_eq] at hm
+  obtain ⟨e, he, hm⟩ := hm
+  haveI : Nontrivial R := nontrivial_of_ne _ _ he
+  refine ⟨e (), ?_, ?_⟩
+  · suffices e ≼[lex] single () #S by
+      simpa [MonomialOrder.lex_le_iff_of_unique] using this
+    rw [← Alon.degree_P]
+    apply MonomialOrder.le_degree
+    rw [mem_support_iff]
+    convert he
+  · rw [← hm]
+    ext j
+    by_cases hj : j = i
+    · rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
+    · rw [mapDomain_notin_range, single_eq_of_ne (Ne.symm hj)]
+      simp [Set.range_const, Set.mem_singleton_iff, hj]
+
+variable [Fintype σ]
+
+open scoped BigOperators
+
+/-- 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_finsupp_sum, 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
+
+/-- 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
+  -- one could simplify this by proving `totalDegree_mul_eq` (at least in a domain)
+  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
+  change (h i).totalDegree < p.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]
+
+end MvPolynomial

Mathlib/Data/Finsupp/Basic.lean

@@ -753,6 +753,22 @@ theorem sum_option_index_smul [Semiring R] [AddCommMonoid M] [Module R M] (f : O
     (f.sum fun o r => r • b o) = f none • b none + f.some.sum fun a r => r • b (Option.some a) :=
   f.sum_option_index _ (fun _ => zero_smul _ _) fun _ _ _ => add_smul _ _ _
 
+theorem option_embedding_add_single [AddCommMonoid M] {n : Option α →₀ M} {m : α →₀ M} {i : M} :
+    (n = embDomain Embedding.some m + single none i) ↔
+      n none = i ∧ n.some = m := by
+  rw [Finsupp.ext_iff, Option.forall]
+  apply and_congr
+  · simp only [coe_add, Pi.add_apply, single_eq_same]
+    rw [embDomain_notin_range _ _ _ ?_, zero_add]
+    rintro ⟨s, hs⟩
+    exact Option.some_ne_none s hs
+  · rw [Finsupp.ext_iff]
+    apply forall_congr'
+    intro s
+    simp only [coe_add, Pi.add_apply, ne_eq, reduceCtorEq, not_false_eq_true, single_eq_of_ne,
+      add_zero, some_apply]
+    rw [← Embedding.some_apply, embDomain_apply, Embedding.some_apply]
+
 end Option
 
 /-! ### Declarations about `Finsupp.filter` -/