English
The ι-inverse ιInv is a linear map from ExteriorAlgebra R M to M that serves as the left inverse to ι_R; i.e., ιInv ∘ ι_R = id_M.
Русский
Обратное к ι — линейное отображение ιInv: ExteriorAlgebra R M → M, являющееся левым обратным для ι_R; то есть ιInv ∘ ι_R = id_M.
LaTeX
$$$\iota_R \colon M \to \mathrm{ExteriorAlgebra} R M$, \ ιInv : \mathrm{ExteriorAlgebra} R M \to \!_R M, \ ιInv \circ ι_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 : ExteriorAlgebra 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
