English
Pushing a derivation forward along a linear equivalence e: M ≃ L, gives a derivation on N corresponding to the image of D under e, and this operation is itself an equivalence of derivation spaces.
Русский
Перенос деривации через линейное эквивалентное отображение e задаёт деривацию на образе, и это образует эквивалентность пространств дериваций.
LaTeX
$$$\text{LinearEquiv}_{R,A,M,N}(e)\;:\; \mathrm{Derivation}(R,A,M) \simeq \mathrm{Derivation}(R,A,N).$$$
Lean4
/-- We can push forward derivations using linear maps, i.e., the composition of a derivation with a
linear map is a derivation. Furthermore, this operation is linear on the spaces of derivations. -/
def _root_.LinearMap.compDer : Derivation R A M →ₗ[R] Derivation R A N
where
toFun
D :=
{ toLinearMap := (f : M →ₗ[R] N).comp (D : A →ₗ[R] M)
map_one_eq_zero' := by simp only [LinearMap.comp_apply, coeFn_coe, map_one_eq_zero, map_zero]
leibniz' := fun a b => by
simp only [coeFn_coe, LinearMap.comp_apply, LinearMap.map_add, leibniz, LinearMap.coe_restrictScalars,
LinearMap.map_smul] }
map_add' D₁ D₂ := by ext; exact LinearMap.map_add _ _ _
map_smul' r D := by dsimp; ext; exact LinearMap.map_smul (f : M →ₗ[R] N) _ _
