Documentation

Mathlib.Analysis.CStarAlgebra.Hom

Properties of C⋆-algebra homomorphisms #

Here we collect properties of C⋆-algebra homomorphisms.

Main declarations #

theorem IsSelfAdjoint.map_spectrum_real {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [CompleteSpace A] [StarRing A] [CStarRing A] [NormedAlgebra A] [StarModule A] [NormedRing B] [CompleteSpace B] [StarRing B] [CStarRing B] [NormedAlgebra B] [StarModule B] [FunLike F A B] [AlgHomClass F A B] [StarHomClass F A B] {a : A} (ha : IsSelfAdjoint a) (φ : F) (hφ : Function.Injective φ) :

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

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