inlAlgHom — Mathlib

English

The lift construction builds an algebra hom from the data of a map on R and a linear map on M, subject to compatibility conditions.

Русский

Конструкция lift восстанавливает алгебраическое отображение по данным отображения на R и линейного отображения на M с условием совместимости.

LaTeX

$$$ lift(f,g,hg,hfg,hgf) : tsze R M \\toₐ[S] A $$$

Lean4

/-- The canonical `S`-algebra inclusion `R → TrivSqZeroExt R M`. -/
@[simps]
def inlAlgHom : R →ₐ[S] tsze R M where
  toFun := inl
  map_one' := inl_one _
  map_mul' := inl_mul _
  map_zero' := inl_zero (M := M)
  map_add' := inl_add _
  commutes' _r := (algebraMap_eq_inl' _ _ _ _).symm

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