Spectral properties in C⋆-algebras

In this file, we establish various properties related to the spectrum of elements in C⋆-algebras.

theorem unitary.spectrum_subset_circle {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra 𝕜 E] [CompleteSpace E] (u : ↥(unitary E)) : spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1

theorem spectrum.subset_circle_of_unitary {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra 𝕜 E] [CompleteSpace E] {u : E} (h : u ∈ unitary E) : spectrum 𝕜 u ⊆ Metric.sphere 0 1

theorem IsSelfAdjoint.spectralRadius_eq_nnnorm {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] {a : A} (ha : IsSelfAdjoint a) : spectralRadius ℂ a = ↑‖a‖₊

theorem IsStarNormal.spectralRadius_eq_nnnorm {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] (a : A) [IsStarNormal a] : spectralRadius ℂ a = ↑‖a‖₊

theorem IsSelfAdjoint.mem_spectrum_eq_re {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] {a : A} (ha : IsSelfAdjoint a) {z : ℂ} (hz : z ∈ spectrum ℂ a) : z = ↑z.re

Any element of the spectrum of a selfadjoint is real.

theorem selfAdjoint.mem_spectrum_eq_re {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] (a : ↥(selfAdjoint A)) {z : ℂ} (hz : z ∈ spectrum ℂ ↑a) : z = ↑z.re

Any element of the spectrum of a selfadjoint is real.

theorem IsSelfAdjoint.val_re_map_spectrum {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] {a : A} (ha : IsSelfAdjoint a) : spectrum ℂ a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ a

The spectrum of a selfadjoint is real

theorem selfAdjoint.val_re_map_spectrum {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] (a : ↥(selfAdjoint A)) : spectrum ℂ ↑a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ ↑a

The spectrum of a selfadjoint is real

theorem StarAlgHom.nnnorm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [FunLike F A B] [AlgHomClass F ℂ A B] [StarAlgHomClass F ℂ A B] (φ : F) (a : A) : ‖φ a‖₊ ≤ ‖a‖₊

A star algebra homomorphism of complex C⋆-algebras is norm contractive.

theorem StarAlgHom.norm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [FunLike F A B] [AlgHomClass F ℂ A B] [StarAlgHomClass F ℂ A B] (φ : F) (a : A) : ‖φ a‖ ≤ ‖a‖

A star algebra homomorphism of complex C⋆-algebras is norm contractive.

noncomputable instance StarAlgHom.instContinuousLinearMapClassComplexInstSemiringComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToModuleInstNormedFieldComplexToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace' {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [FunLike F A B] [AlgHomClass F ℂ A B] [StarAlgHomClass F ℂ A B] : ContinuousLinearMapClass F ℂ A B

Star algebra homomorphisms between C⋆-algebras are continuous linear maps. See note [lower instance priority]

Equations

• ⋯ = ⋯

theorem StarAlgEquiv.nnnorm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarAlgEquivClass F ℂ A B] (φ : F) (a : A) : ‖φ a‖₊ = ‖a‖₊

theorem StarAlgEquiv.norm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarAlgEquivClass F ℂ A B] (φ : F) (a : A) : ‖φ a‖ = ‖a‖

theorem StarAlgEquiv.isometry {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarAlgEquivClass F ℂ A B] (φ : F) : Isometry ⇑φ

noncomputable instance WeakDual.Complex.instStarHomClass {F : Type u_1} {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] [FunLike F A ℂ] [hF : AlgHomClass F ℂ A ℂ] : StarHomClass F A ℂ

This instance is provided instead of StarAlgHomClass to avoid type class inference loops. See note [lower instance priority]

Equations

• ⋯ = ⋯

theorem AlgHomClass.instStarAlgHomClass {F : Type u_1} {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] [FunLike F A ℂ] [hF : AlgHomClass F ℂ A ℂ] : StarAlgHomClass F ℂ A ℂ

This is not an instance to avoid type class inference loops. See WeakDual.Complex.instStarHomClass.

noncomputable instance WeakDual.CharacterSpace.instStarAlgHomClass {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ℂ A] : StarAlgHomClass ↑(WeakDual.characterSpace ℂ A) ℂ A ℂ

Equations

• ⋯ = ⋯