toTop — Mathlib

English

There is a canonical nonunital algebra hom from A to ⊤ given by restricting the identity map to ⊤.

Русский

Существует канонический неединичный гомоморфизм из A в ⊤, получаемый ограничением тождественного отображения на ⊤.

LaTeX

$$$toTop : A \toₙₐ[R] (\top : NonUnitalSubalgebra R A) = \mathrm{codRestrict}(\mathrm{id}_{R,A}, \top, \lambda x.\ mem_top)$$$

Lean4

/-- `NonUnitalAlgHom` to `⊤ : NonUnitalSubalgebra R A`. -/
def toTop : A →ₙₐ[R] (⊤ : NonUnitalSubalgebra R A) :=
  NonUnitalAlgHom.codRestrict (NonUnitalAlgHom.id R A) ⊤ fun _ => mem_top

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