English
A multivariate polynomial that vanishes on a large product finite set is identically zero.
Русский
Мультивариантный многочлен, который обращается в ноль на большом произведении конечных множеств, должен быть нулевым.
LaTeX
$$$$ \text{eq_zero_of_eval_zero_at_prod_finset} \ ; \ P = 0. $$$$
Lean4
/-- 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]
set n := (embDomain Function.Embedding.some m).update none d with hn
rw [eq_option_embedding_update_none_iff] 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 := (embDomain Function.Embedding.some e).update none m with hn
rw [eq_option_embedding_update_none_iff] 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
