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}
[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 ⇑φ)
:
theorem
NonUnitalStarAlgHom.norm_map
{F : Type u_1}
{A : Type u_2}
{B : Type u_3}
[NonUnitalNormedRing A]
[CompleteSpace A]
[StarRing A]
[CStarRing A]
[NormedSpace ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[StarModule ℂ A]
[NonUnitalNormedRing B]
[CompleteSpace B]
[StarRing B]
[CStarRing B]
[NormedSpace ℂ B]
[IsScalarTower ℂ B B]
[SMulCommClass ℂ B B]
[StarModule ℂ B]
[FunLike F A B]
[NonUnitalAlgHomClass F ℂ A B]
[StarHomClass F A B]
(φ : F)
(hφ : Function.Injective ⇑φ)
(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}
[NonUnitalNormedRing A]
[CompleteSpace A]
[StarRing A]
[CStarRing A]
[NormedSpace ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[StarModule ℂ A]
[NonUnitalNormedRing B]
[CompleteSpace B]
[StarRing B]
[CStarRing B]
[NormedSpace ℂ B]
[IsScalarTower ℂ B B]
[SMulCommClass ℂ B B]
[StarModule ℂ B]
[FunLike F A B]
[NonUnitalAlgHomClass F ℂ A B]
[StarHomClass F A B]
(φ : F)
(hφ : Function.Injective ⇑φ)
(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}
[NonUnitalNormedRing A]
[CompleteSpace A]
[StarRing A]
[CStarRing A]
[NormedSpace ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[StarModule ℂ A]
[NonUnitalNormedRing B]
[CompleteSpace B]
[StarRing B]
[CStarRing B]
[NormedSpace ℂ B]
[IsScalarTower ℂ B B]
[SMulCommClass ℂ B B]
[StarModule ℂ B]
[FunLike F A B]
[NonUnitalAlgHomClass F ℂ A B]
[StarHomClass F A B]
(φ : F)
(hφ : Function.Injective ⇑φ)
:
Isometry ⇑φ