English
The left inverse ιInv is a linear map from TensorAlgebra R M to M which, together with the canonical embedding ι_R, recovers the original element of M.
Русский
Левополная обратная ιInv — линейное отображение из TensorAlgebra_R M в M, которое вместе с каноническим внедрением ι_R восстанавливает исходный элемент M.
LaTeX
$$$\\iotaInv : \\mathrm{TensorAlgebra}_R M \\to_L_R M$,\\quad \\iotaInv \\circ \\iota_R = \\mathrm{id}_M$$$
Lean4
/-- The left-inverse of `ι`.
As an implementation detail, we implement this using `TrivSqZeroExt` which has a suitable
algebra structure. -/
def ιInv : TensorAlgebra R M →ₗ[R] M :=
by
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap
