English
There is a canonical algebra map from ExteriorAlgebra R M to TrivSqZeroExt R M sending ι x to inr x; this map is defined via lift with the appropriate primitive inr.
Русский
Существует канонический алгебра-хомоморфизм от ExteriorAlgebra R M в TrivSqZeroExt R M, отправляющий ι x в inr x; этот отображение задаётся через lift со соответствующим inr.
LaTeX
$$$\mathrm{toTrivSqZeroExt} : \mathrm{ExteriorAlgebra} R M \to_{\!a[R]} \mathrm{TrivSqZeroExt} R M$$$
Lean4
/-- The canonical map from `ExteriorAlgebra R M` into `TrivSqZeroExt R M` that sends
`ExteriorAlgebra.ι` to `TrivSqZeroExt.inr`. -/
def toTrivSqZeroExt [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : ExteriorAlgebra R M →ₐ[R] TrivSqZeroExt R M :=
lift R ⟨TrivSqZeroExt.inrHom R M, fun m => TrivSqZeroExt.inr_mul_inr R m m⟩
