English
There is a canonical star-homomorphism embedding the center of CentroidHom α into CentroidHom α.
Русский
Существует канонический *-одомох, внедряющий центр CentroidHom α в CentroidHom α.
LaTeX
$$$\\text{centerStarEmbedding}: \\mathrm{Subsemiring.center}(\\mathrm{CentroidHom}(\\alpha)) \\to_{*} \\mathrm{CentroidHom}(\\alpha)$ with star-preservation: $\\big(\\text{centerStarEmbedding}(z)\\big)^{\\ast}=\\text{centerStarEmbedding}(z^{\\ast})$$$
Lean4
/-- The canonical *-homomorphism embedding the center of `CentroidHom α` into `CentroidHom α`. -/
def centerStarEmbedding : Subsemiring.center (CentroidHom α) →⋆ₙ+* CentroidHom α
where
toNonUnitalRingHom := (SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom
map_star'
f :=
by
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe,
SubsemiringClass.coe_subtype]
exact rfl
