English
There is a natural linear equivalence between the space of R-linear maps from σ to A and the space of R-derivations from MvPolynomial σ R to A, given by the mkDerivation construction; its inverse sends a derivation D to the map i ↦ D(X_i).
Русский
Существует естественное линейное эквалентное отображение между пространством линейных отображений R-модуля σ → A и пространством производных по MvPolynomial σ R в A, задаваемое конструктором mkDerivation; обратное отображение отправляет деривцию D в отображение i ↦ D(X_i).
LaTeX
$$$\mkDerivationEquiv : (\\sigma \\to A) \\simeq_l[R] \\operatorname{Derivation} R (MvPolynomial\\ \\sigma\\ R) A$$$
Lean4
/-- `MvPolynomial.mkDerivation` as a linear equivalence. -/
def mkDerivationEquiv : (σ → A) ≃ₗ[R] Derivation R (MvPolynomial σ R) A :=
LinearEquiv.symm <|
{ invFun := mkDerivation R
toFun := fun D i => D (X i)
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl
left_inv := fun _ => derivation_ext <| mkDerivation_X _ _
right_inv := fun _ => funext <| mkDerivation_X _ _ }
