Spectral properties in C⋆-algebras

In this file, we establish various properties related to the spectrum of elements in C⋆-algebras. In particular, we show that the spectrum of a unitary element is contained in the unit circle in ℂ, the spectrum of a selfadjoint element is real, the spectral radius of a selfadjoint element or normal element is its norm, among others.

An essential feature of C⋆-algebras is spectral permanence. This is the property that the spectrum of an element in a closed subalgebra is the same as the spectrum of the element in the whole algebra. For Banach algebras more generally, and even for Banach ⋆-algebras, this fails.

A consequence of spectral permanence is that one may always enlarge the C⋆-algebra (via a unital embedding) while preserving the spectrum of any element. In addition, it allows us to make sense of the spectrum of elements in non-unital C⋆-algebras by considering them as elements in the Unitization of the C⋆-algebra, or indeed any unital C⋆-algebra. Of course, one may do this (that is, consider the spectrum of an element in a non-unital by embedding it in a unital algebra) for any Banach algebra, but the downside in that setting is that embedding in different unital algebras results in varying spectra.

In Mathlib, we don't define the spectrum of an element in a non-unital C⋆-algebra, and instead simply consider the quasispectrum so as to avoid depending on a choice of unital algebra. However, we can still establish a form of spectral permanence.

Main statements

• unitary.spectrum_subset_circle: The spectrum of a unitary element is contained in the unit sphere in ℂ.
• IsSelfAdjoint.spectralRadius_eq_nnnorm: The spectral radius of a selfadjoint element is equal to its norm.
• IsStarNormal.spectralRadius_eq_nnnorm: The spectral radius of a normal element is equal to its norm.
• IsSelfAdjoint.mem_spectrum_eq_re: Any element of the spectrum of a selfadjoint element is real.

• StarSubalgebra.coe_isUnit: for x : S in a C⋆-Subalgebra S of A, then ↑x : A is a Unit if and only if x is a unit.
• StarSubalgebra.spectrum_eq: spectral_permanence for x : S, where S is a C⋆-Subalgebra of A, spectrum ℂ x = spectrum ℂ (x : A).

TODO

• prove a variation of spectral permanence using StarAlgHom instead of StarSubalgebra.
• prove a variation of spectral permanence for quasispectrum.

theorem unitary.spectrum_subset_circle {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [NormedAlgebra 𝕜 E] [CompleteSpace E] (u : { x : E // x ∈ 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 IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CStarRing A] {a : A} (ha : IsSelfAdjoint a) : (spectralRadius ℂ a).toReal = ‖a‖

In a C⋆-algebra, the spectral radius of a self-adjoint element is equal to its norm. See IsSelfAdjoint.toReal_spectralRadius_eq_norm for a version involving spectralRadius ℝ 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 : { x : A // x ∈ selfAdjoint A }) {z : ℂ} (hz : z ∈ spectrum ℂ ↑a) : z = ↑z.re

Any element of the spectrum of a selfadjoint is real.

theorem IsSelfAdjoint.im_eq_zero_of_mem_spectrum {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.im = 0

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 : { x : A // x ∈ selfAdjoint A }) : spectrum ℂ ↑a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ ↑a

The spectrum of a selfadjoint is real

theorem IsSelfAdjoint.isConnected_spectrum_compl {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] {a : A} (ha : IsSelfAdjoint a) : IsConnected (spectrum ℂ a)ᶜ

The complement of the spectrum of a selfadjoint element in a C⋆-algebra is connected.

theorem StarSubalgebra.coe_isUnit {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : { x : A // x ∈ S }} : IsUnit ↑a ↔ IsUnit a

For a unital C⋆-subalgebra S of A and x : S, if ↑x : A is invertible in A, then x is invertible in S.

theorem StarSubalgebra.mem_spectrum_iff {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : { x : A // x ∈ S }} {z : ℂ} : z ∈ spectrum ℂ a ↔ z ∈ spectrum ℂ ↑a

theorem StarSubalgebra.spectrum_eq {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : { x : A // x ∈ S }} : spectrum ℂ a = spectrum ℂ ↑a

Spectral permanence. The spectrum of an element is invariant of the (closed) StarSubalgebra in which it is contained.

theorem NonUnitalStarAlgHom.nnnorm_apply_le {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) (a : A) : ‖φ a‖₊ ≤ ‖a‖₊

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

theorem NonUnitalStarAlgHom.norm_apply_le {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) (a : A) : ‖φ a‖ ≤ ‖a‖

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

theorem NonUnitalStarAlgHom.instContinuousLinearMapClassComplex {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] : ContinuousLinearMapClass F ℂ A B

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

theorem StarAlgEquiv.nnnorm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedSpace ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] [NormedRing B] [NormedSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [CompleteSpace B] [StarRing B] [CStarRing B] [StarModule ℂ B] [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass 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] [NormedSpace ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] [NormedRing B] [NormedSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [CompleteSpace B] [StarRing B] [CStarRing B] [StarModule ℂ B] [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass 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] [NormedSpace ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] [NormedRing B] [NormedSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [CompleteSpace B] [StarRing B] [CStarRing B] [StarModule ℂ B] [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass F A B] (φ : F) : Isometry ⇑φ

@[instance 100]

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 StarHomClass to avoid type class inference loops. See note [lower instance priority]

Equations

• ⋯ = ⋯

theorem AlgHomClass.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 is not an instance to avoid type class inference loops. See WeakDual.Complex.instStarHomClass.

noncomputable instance WeakDual.CharacterSpace.instStarHomClass {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A] : StarHomClass (↑(WeakDual.characterSpace ℂ A)) A ℂ

Equations

• ⋯ = ⋯