The continuous functional calculus of a closed star subalgebra

Let B be a Banach ⋆-algebra over 𝕜 = ℝ or ℂ carrying a continuous functional calculus for the elements satisfying a predicate q, and let S be a closed star subalgebra of B. Mathlib's cfc_mem says that cfc f x lies in S whenever x does. This file draws the two consequences of that fact.

• Spectral permanence. For x ∈ S with q x, the spectrum of x in S equals its spectrum in B (StarSubalgebra.spectrum_eq_of_predicate): if r - x is invertible in B, its inverse is cfc (fun t ↦ (r - t)⁻¹) x, which lies in S. This needs no norm on B.
• The calculus restricts. S carries a continuous functional calculus for the elements satisfying q in B (StarSubalgebra.continuousFunctionalCalculus), computed by the calculus of B (StarSubalgebra.coe_cfc).

Transferring the second statement along a star algebra isomorphism onto the range gives the form used in practice: a unital ⋆-homomorphism φ : A →⋆ₐ[𝕜] B that is a closed embedding pulls the continuous functional calculus of B back to A (StarAlgHom.continuousFunctionalCalculus_of_isClosedEmbedding), and then commutes with it (StarAlgHom.map_cfc). The motivating instance is a real C⋆-algebra embedded isometrically in a complex one, such as the bounded operators on a real Hilbert space inside the bounded operators on its complexification: the self-adjoint elements of the real algebra acquire a real continuous functional calculus, which Mathlib constructs only for complex C⋆-algebras.

Mathlib's StarSubalgebra.spectrum_eq is the analogous spectral permanence statement for closed complex star subalgebras of a complex C⋆-algebra, where it holds for every element. Here only the calculus of B is used, so the statement covers real subalgebras, but it is restricted to the elements on which that calculus is defined.

Main declarations

• StarSubalgebra.spectrum_eq_of_predicate: spectral permanence for the elements of a closed star subalgebra satisfying the predicate of the calculus.
• StarSubalgebra.continuousFunctionalCalculus: a closed star subalgebra inherits the continuous functional calculus.
• StarSubalgebra.coe_cfc: the inherited calculus is computed in the ambient algebra.
• StarAlgHom.spectrum_apply_eq_of_isClosedEmbedding: spectral permanence along a closed embedding of ⋆-algebras.
• StarAlgHom.continuousFunctionalCalculus_of_isClosedEmbedding: a closed embedding of ⋆-algebras pulls the continuous functional calculus back.

theorem StarSubalgebra.spectrum_eq_of_predicate {𝕜 : Type u_1} {B : Type u_2} {q : B → Prop} [RCLike 𝕜] [Ring B] [StarRing B] [Algebra 𝕜 B] [TopologicalSpace B] [IsTopologicalRing B] [StarModule 𝕜 B] [ContinuousStar B] [ContinuousFunctionalCalculus 𝕜 B q] (S : StarSubalgebra 𝕜 B) [IsClosed ↑S] {x : ↥S} (hx : q ↑x) : spectrum 𝕜 x = spectrum 𝕜 ↑x

Spectral permanence for a closed star subalgebra S: an element x ∈ S on which the continuous functional calculus of the ambient algebra is defined has the same spectrum in S as in the ambient algebra.

theorem StarAlgHom.spectrum_apply_eq_of_isClosedEmbedding {𝕜 : Type u_1} {B : Type u_2} {q : B → Prop} [RCLike 𝕜] [Ring B] [StarRing B] [Algebra 𝕜 B] [TopologicalSpace B] [IsTopologicalRing B] [StarModule 𝕜 B] [ContinuousStar B] [ContinuousFunctionalCalculus 𝕜 B q] {A : Type u_3} [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] (φ : A →⋆ₐ[𝕜] B) (hφ : Topology.IsClosedEmbedding ⇑φ) {a : A} (ha : q (φ a)) : spectrum 𝕜 (φ a) = spectrum 𝕜 a

Spectral permanence along a unital ⋆-homomorphism φ which is a closed embedding: if the continuous functional calculus of B is defined at φ a, then φ a has the same spectrum as a.

theorem StarSubalgebra.continuousFunctionalCalculus {𝕜 : Type u_1} {B : Type u_3} {q : B → Prop} [RCLike 𝕜] [NormedRing B] [StarRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] [StarModule 𝕜 B] [ContinuousStar B] [ContinuousFunctionalCalculus 𝕜 B q] (S : StarSubalgebra 𝕜 B) [hS : IsClosed ↑S] : ContinuousFunctionalCalculus 𝕜 ↥S fun (x : ↥S) => q ↑x

A closed star subalgebra S inherits the continuous functional calculus of the ambient algebra, for the elements satisfying the same predicate there: the calculus of x ∈ S is the ambient calculus of x, which takes values in S by cfc_mem.

@[simp]

theorem StarSubalgebra.coe_cfc {𝕜 : Type u_1} {B : Type u_3} {q : B → Prop} [RCLike 𝕜] [NormedRing B] [StarRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] [StarModule 𝕜 B] [ContinuousStar B] [ContinuousFunctionalCalculus 𝕜 B q] (S : StarSubalgebra 𝕜 B) [hS : IsClosed ↑S] [ContinuousMap.UniqueHom 𝕜 B] (f : 𝕜 → 𝕜) (x : ↥S) : ↑(cfc f x) = cfc f ↑x

The continuous functional calculus that a closed star subalgebra inherits is computed in the ambient algebra.

theorem StarAlgHom.continuousFunctionalCalculus_of_isClosedEmbedding {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} {p : A → Prop} {q : B → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [NormedRing B] [StarRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] [StarModule 𝕜 B] [ContinuousStar B] [ContinuousFunctionalCalculus 𝕜 B q] (φ : A →⋆ₐ[𝕜] B) (hφ : Topology.IsClosedEmbedding ⇑φ) (hpq : ∀ (a : A), p a ↔ q (φ a)) : ContinuousFunctionalCalculus 𝕜 A p

A unital ⋆-homomorphism φ : A →⋆ₐ[𝕜] B which is a closed embedding pulls the continuous functional calculus of B back to A, for elements a such that φ a satisfies the predicate of the calculus of B. The calculus of A is then intertwined with that of B by StarAlgHom.map_cfc.