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} {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [RCLike 𝕜] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [Algebra 𝕜 A] [Ring B] [StarRing B] [TopologicalSpace B] [Algebra ℝ B] [Algebra 𝕜 B] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [IsScalarTower ℝ 𝕜 A] [IsScalarTower ℝ 𝕜 B] [ContinuousMap.UniqueHom ℝ B] [FunLike F A B] [AlgHomClass F 𝕜 A B] [StarHomClass F A B] {a : A} (ha : IsSelfAdjoint a) (φ : F) (hφ : Function.Injective ⇑φ) (hφ' : Continuous ⇑φ := by fun_prop) : spectrum ℝ (φ a) = spectrum ℝ a

theorem IsSelfAdjoint.map_quasispectrum_real {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] {a : A} (ha : IsSelfAdjoint a) (φ : F) (hφ : Function.Injective ⇑φ) : quasispectrum ℝ (φ a) = quasispectrum ℝ a

def NonUnitalStarAlgHom.toOrderEmbedding {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] (φ : A →⋆ₙₐ[ℂ] B) (hφ : Function.Injective ⇑φ) : A ↪o B

A non-unital star monomorphism between C⋆-algebras is an order embedding.

Equations

• φ.toOrderEmbedding hφ = { toFun := ⇑φ, inj' := hφ, map_rel_iff' := ⋯ }

theorem NonUnitalStarAlgHom.map_le_map_iff {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) {x y : A} : f x ≤ f y ↔ x ≤ y

A non-unital star monomorphism between C⋆-algebras is an order embedding.

theorem NonUnitalStarAlgHom.map_lt_map_iff {F : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) (hf : Function.Injective ⇑f) {x y : A} : f x < f y ↔ x < y

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 ⇑φ