English
The inverse embedding ιInv interacts with the map construction compatibly: ιInv.comp (map f).toLinearMap = f.comp ιInv for a linear map f: M → N.
Русский
Обратное вложение ιInv взаимодествует с построением отображения: ιInv ∘ map f = f ∘ ιInv.
LaTeX
$$$ ιInv \\circ (map\\ f) = f \\circ ιInv. $$$
Lean4
theorem ιInv_comp_map (f : M →ₗ[R] N) : ιInv.comp (map f).toLinearMap = f.comp ιInv :=
by
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
letI : Module Rᵐᵒᵖ N := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
haveI : IsCentralScalar R N := ⟨fun r m => rfl⟩
unfold ιInv
conv_lhs =>
rw [LinearMap.comp_assoc, ← AlgHom.comp_toLinearMap, toTrivSqZeroExt_comp_map, AlgHom.comp_toLinearMap, ←
LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map]
rfl
