Properties of C⋆-algebra homomorphisms

Here we collect properties of C⋆-algebra homomorphisms.

Main declarations

• NonUnitalStarAlgHom.norm_map: A non-unital star algebra monomorphism of complex C⋆-algebras is isometric.

theorem IsSelfAdjoint.map_spectrum_real {F : Type u_1} {A : Type u_2} {B : Type u_3} [CStarAlgebra A] [CStarAlgebra B] [FunLike F A B] [AlgHomClass F ℂ A B] [StarHomClass F A B] {a : A} (ha : IsSelfAdjoint a) (φ : F) (hφ : Function.Injective ⇑φ) : spectrum ℝ (φ a) = spectrum ℝ a

theorem NonUnitalStarAlgHom.norm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (hφ : Function.Injective ⇑φ) (a : A) : ‖φ a‖ = ‖a‖

A non-unital star algebra monomorphism of complex C⋆-algebras is isometric.

theorem NonUnitalStarAlgHom.nnnorm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (hφ : Function.Injective ⇑φ) (a : A) : ‖φ a‖₊ = ‖a‖₊

A non-unital star algebra monomorphism of complex C⋆-algebras is isometric.

theorem NonUnitalStarAlgHom.isometry {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F) (hφ : Function.Injective ⇑φ) : Isometry ⇑φ