toNonUnitalAlgHom — Mathlib

English

A unital algebra homomorphism can be regarded as a nonunital algebra homomorphism by forgetting the unit, with the same action on elements and the same multiplicative structure.

Русский

Угомоморфизм алгебр с единицей можно рассматривать как неединичный гомоморфизм, забывая единицу, сохраняя действии на элементы и умножение.

LaTeX

$$$f:A\\to_{R}B\\Rightarrow f\\text{ как }A\\to_{\\mathrm{NonUnital}}B$$$

Lean4

/-- A unital morphism of algebras is a `NonUnitalAlgHom`. -/
@[coe]
def toNonUnitalAlgHom (f : A →ₐ[R] B) : A →ₙₐ[R] B :=
  { f with map_smul' := map_smul f }

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