English
There exists a linear equivalence between derivation spaces induced by a linear equivalence on the underlying modules, with explicit inverse given by the inverse equivalence.
Русский
Существует линейное эквивалентное отображение между пространствами дериваций, индуцируемое линейным эквивалентом между модулями, с явной обратной стороной.
LaTeX
$$$\text{LinearEquiv.compDer} : \mathrm{Derivation}(R,A,M) \simeq \mathrm{Derivation}(R,A,N)$ for a linear equivalence $e: M \simeq N$.$$
Lean4
/-- Pushing a derivation forward through a linear equivalence is an equivalence. -/
def _root_.LinearEquiv.compDer : Derivation R A M ≃ₗ[R] Derivation R A N :=
{ e.toLinearMap.compDer with
invFun := e.symm.toLinearMap.compDer
left_inv := fun D => by ext a; exact e.symm_apply_apply (D a)
right_inv := fun D => by ext a; exact e.apply_symm_apply (D a) }
