English
If for all monomials d with φ.coeff d ≠ 0 there exists i in d.support with g(i) = 0, then eval₂Hom f g φ = 0.
Русский
Если для каждого монома d с φ.coeff d ≠ 0 существует i в поддержке d такое, что g(i) = 0, то eval₂Hom f g φ = 0.
LaTeX
$$$$ \forall d, \; \phi.coeff(d) \neq 0 \to \exists i \in d.support, g(i) = 0 \Rightarrow \mathrm{eval_2Hom}(f,g)(\phi) = 0 $$$$
Lean4
theorem eval₂Hom_eq_zero (f : R →+* S₂) (g : σ → S₂) (φ : MvPolynomial σ R)
(h : ∀ d, φ.coeff d ≠ 0 → ∃ i ∈ d.support, g i = 0) : eval₂Hom f g φ = 0 :=
by
rw [φ.as_sum, map_sum]
refine Finset.sum_eq_zero fun d hd => ?_
obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (Finsupp.mem_support_iff.mp hd)
rw [eval₂Hom_monomial, Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
rw [hgi, zero_pow]
rwa [← Finsupp.mem_support_iff]
