English
There exists a natural linear equivalence between the module A and the module of R-derivations Derivation R R[X] A, given by a ↦ mkDerivation R a, with inverse given by evaluating a derivation at X.
Русский
Существует естественная линейная эк Dual-эквивалентность между модулем A и модулем R-дериваций Derivation R R[X] A, задаваемая a ↦ mkDerivation R a, а обратное отображение задаётся восприятием деривации на X.
LaTeX
$$$A \\cong_R \\mathrm{Derivation}_R\\bigl(R[X],A\\b\bigr).$$$$
Lean4
/-- `Polynomial.mkDerivation` as a linear equivalence. -/
def mkDerivationEquiv : A ≃ₗ[R] Derivation R R[X] A :=
LinearEquiv.symm <|
{ invFun := mkDerivation R
toFun := fun D => D X
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl
left_inv := fun _ => derivation_ext <| mkDerivation_X _ _
right_inv := fun _ => mkDerivation_X _ _ }
