English
A general construction MkDerivation defines a derivation from a family f : σ → A by specifying its action on X_i and extending to all polynomials.
Русский
Общая конструкция MkDerivation задаёт производную по данному семейству f: σ → A и затем распространяет onto все полиномы.
LaTeX
$$$\\\\text{MkDerivation}(f):\\\\ Derivation \\\\text{on } MvPolynomial(\\\\sigma, R) \\\\text{with } X_i \\mapsto f(i)$$$
Lean4
/-- The derivation on `MvPolynomial σ R` that takes value `f i` on `X i`. -/
def mkDerivation (f : σ → A) : Derivation R (MvPolynomial σ R) A
where
toLinearMap := mkDerivationₗ R f
map_one_eq_zero' := mkDerivationₗ_C _ 1
leibniz' :=
(leibniz_iff_X (mkDerivationₗ R f) (mkDerivationₗ_C _ 1)).2 fun s i =>
by
simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]
rw [Finsupp.sum_add_index'] <;> [skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul])]
rw [Finsupp.sum_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]
rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm, Finsupp.smul_sum]
refine congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => ?_); dsimp only
rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]
rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]
