English
The map A → AlgebraEnd(B,M) given by left action is an ℝ-algebra homomorphism.
Русский
Отображение A в End_B(M), задаваемое левой операцией, является ℝ-алгебраическим гомоморфизмом.
LaTeX
$$$\mathrm{lsmul} : A \to_{\mathbb{R}} \mathrm{End}_B(M)$$$
Lean4
/-- If a `NonUnitalStarSubalgebra` over a field does not contain `1`, then its unitization is
isomorphic to its `StarAlgebra.adjoin`. -/
@[simps! apply_coe]
noncomputable def unitizationStarAlgEquiv (h1 : (1 : A) ∉ s) :
Unitization R s ≃⋆ₐ[R] StarAlgebra.adjoin R (s : Set A) :=
let starAlgHom : Unitization R s →⋆ₐ[R] StarAlgebra.adjoin R (s : Set A) :=
((unitization s).codRestrict _ fun x ↦ (unitization_range s).le <| Set.mem_range_self x)
StarAlgEquiv.ofBijective starAlgHom <| by
refine ⟨?_, fun x ↦ ?_⟩
· have :=
AlgHomClass.unitization_injective s h1 ((StarSubalgebra.subtype _).comp starAlgHom) fun _ ↦ by simp [starAlgHom]
rw [StarAlgHom.coe_comp] at this
exact this.of_comp
· obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) := (unitization_range s).ge x.property
exact ⟨a, Subtype.ext ha⟩
