toTrivSqZeroExt — Mathlib

English

There is a canonical algebra homomorphism from TensorAlgebra R M to TrivSqZeroExt R M which sends ι_R x to the right component (inr x).

Русский

Существует канонический алгебра-гомоморфизм из TensorAlgebra_R M в TrivSqZeroExt_R M, отправляющий ι_R x в правый компонент (inr x).

LaTeX

$$$\\text{toTrivSqZeroExt} : \\mathrm{TensorAlgebra}_R M \\to_A \\mathrm{TrivSqZeroExt}_R M,\\quad \\text{toTrivSqZeroExt}(\\iota_R x) = \\mathrm{TrivSqZeroExt.inr} x$$$

Lean4

/-- The canonical map from `TensorAlgebra R M` into `TrivSqZeroExt R M` that sends
`TensorAlgebra.ι` to `TrivSqZeroExt.inr`. -/
def toTrivSqZeroExt [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : TensorAlgebra R M →ₐ[R] TrivSqZeroExt R M :=
  lift R (TrivSqZeroExt.inrHom R M)

Похожие утверждения