From cc5a7230aa37dba826c9f86298401754bc2bd2cf Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 12 Dec 2023 19:59:15 +0000 Subject: [PATCH] feat: add `StarAlgHom.ofId` (#8993) --- Mathlib/Algebra/Star/StarAlgHom.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean index 8a9b7b3362da8..d7c8a3c477c70 100644 --- a/Mathlib/Algebra/Star/StarAlgHom.lean +++ b/Mathlib/Algebra/Star/StarAlgHom.lean @@ -450,6 +450,14 @@ theorem coe_id : ⇑(StarAlgHom.id R A) = id := rfl #align star_alg_hom.coe_id StarAlgHom.coe_id +/-- `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] } + end instance : Inhabited (A →⋆ₐ[R] A) :=