English
The underlying function of a StarAlgHom, when viewed as a non-unital star-algebra homomorphism, coincides with the original underlying function.
Русский
Базовая функция StarAlgHom, рассматриваемая как ненаправленный звездной алгебной гомоморфизм, совпадает с исходной функцией.
LaTeX
$$$f.toNonUnitalStarAlgHom : A \to⋆ₙₐ[R] B$ induces same underlying map as $f$$$
Lean4
/-- `algebraMap R A` as a `StarAlgHom` when `A` is a star algebra over `R`. -/
@[simps]
def ofId (R A : Type*) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] :
R →⋆ₐ[R] A :=
{ Algebra.ofId R A with
toFun := algebraMap R A
map_star' := by simp [Algebra.algebraMap_eq_smul_one] }
