English
The mapCoeffs map from a derivation d to a polynomial-coefficient derivation satisfies that its value on p is given coefficientwise by applying d to each coefficient of p.
Русский
MapCoeffs отображает производную d к полиномиальному выводу так, что значение на p задаётся по коэффициентам: каждое коэффициент p$i$ отображается через d.
LaTeX
$$$\text{mapCoeffs}(p) \text{ has coefficients } (\text{coeff }(\text{mapCoeffs}(p),i) = d(\text{coeff }(p,i))).$$$
Lean4
/-- The `R`-derivation from `A[X]` to `M[X]` which applies the derivative to each
of the coefficients.
-/
def mapCoeffs : Derivation R A[X] (PolynomialModule A M)
where
__ := (PolynomialModule.map A d.toLinearMap).comp PolynomialModule.equivPolynomial.symm.toLinearMap
map_one_eq_zero' := show (Finsupp.single 0 1).mapRange (d : A → M) d.map_zero = 0 by simp
leibniz' p
q := by
dsimp
induction p using Polynomial.induction_on' with
| add => simp only [add_mul, map_add, add_smul, smul_add, add_add_add_comm, *]
| monomial n a =>
induction q using Polynomial.induction_on' with
| add => simp only [mul_add, map_add, add_smul, smul_add, add_add_add_comm, *]
| monomial m b =>
refine Finsupp.ext fun i ↦ ?_
dsimp [PolynomialModule.equivPolynomial, PolynomialModule.map]
simp only [toFinsupp_mul, toFinsupp_monomial, AddMonoidAlgebra.single_mul_single]
change
d _ =
_ +
_
-- TODO: copy more `Finsupp` API to `PolynomialModule`.
-- We have to do a bit of work to go through the identification
-- `PolynomialModule A M = ℕ →₀ M`...
dsimp only [PolynomialModule, Finsupp.mapRange.linearMap_apply, coeFn_coe]
rw [Finsupp.mapRange_single, Finsupp.mapRange_single]
-- ... and here we go back through the identification.
change _ = (_ • PolynomialModule.single A _ _) _ + (_ • PolynomialModule.single A _ _) i
simp only [PolynomialModule.monomial_smul_single, AddMonoidAlgebra.single_apply, apply_ite d, leibniz, map_zero,
PolynomialModule.single_apply, ite_add_zero, add_comm m n]
