mathlib3 documentation

analysis.normed_space.star.continuous_functional_calculus

Continuous functional calculus #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we construct the continuous_functional_calculus for a normal element a of a (unital) C⋆-algebra over ℂ. This is a star algebra equivalence C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elemental_star_algebra ℂ a which sends the (restriction of) the identity map continuous_map.id ℂ to the (unique) preimage of a under the coercion of elemental_star_algebra ℂ a to A.

Being a star algebra equivalence between C⋆-algebras, this map is continuous (even an isometry), and by the Stone-Weierstrass theorem it is the unique star algebra equivalence which extends the polynomial functional calculus (i.e., polynomial.aeval).

For any continuous function f : spectrum ℂ a → ℂ, this makes it possible to define an element f a (not valid notation) in the original algebra, which heuristically has the same eigenspaces as a and acts on eigenvector of a for an eigenvalue λ as multiplication by f λ. This description is perfectly accurate in finite dimension, but only heuristic in infinite dimension as there might be no genuine eigenvector. In particular, when f is a polynomial ∑ cᵢ Xⁱ, then f a is ∑ cᵢ aⁱ. Also, id a = a.

This file also includes a proof of the spectral permanence theorem for (unital) C⋆-algebras (see star_subalgebra.spectrum_eq)

Main definitions #

continuous_functional_calculus : C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elemental_star_algebra ℂ a: this is the composition of the inverse of the gelfand_star_transform with the natural isomorphism induced by the homeomorphism elemental_star_algebra.character_space_homeo.
elemental_star_algebra.character_space_homeo :character_space ℂ (elemental_star_algebra ℂ a) ≃ₜ spectrum ℂ a: this homeomorphism is defined by evaluating a characterφata, and noting thatφ a ∈ spectrum ℂ asinceφ` is an algebra homomorphism. Moreover, this map is continuous and bijective and since the spaces involved are compact Hausdorff, it is a homeomorphism.

Main statements #

star_subalgebra.coe_is_unit: for x : S in a C⋆-subalgebra S of A, then ↑x : A is a unit if and only if x is a unit.
star_subalgebra.spectrum_eq: spectral_permanence for x : S, where S is a C⋆-subalgebra of A, spectrum ℂ x = spectrum ℂ (x : A).

Notes #

The result we have established here is the strongest possible, but it is likely not the version which will be most useful in practice. Future work will include developing an appropriate API for the continuous functional calculus (including one for real-valued functions with real argument that applies to self-adjoint elements of the algebra).

@[protected, instance]

def elemental_star_algebra.normed_comm_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [star_ring R] [normed_ring A] [algebra R A] [star_ring A] [has_continuous_star A] [star_module R A] (a : A) [is_star_normal a] :

normed_comm_ring ↥(elemental_star_algebra R a)

Equations

@[protected, instance]

def elemental_star_algebra.normed_algebra {R : Type u_1} {A : Type u_2} [normed_field R] [star_ring R] [normed_ring A] [normed_algebra R A] [star_ring A] [has_continuous_star A] [star_module R A] (a : A) :

normed_algebra R ↥(elemental_star_algebra R a)

Equations

elemental_star_algebra.normed_algebra a = (elemental_star_algebra R a).to_normed_algebra

@[protected, instance]

def elemental_star_algebra.normed_space {R : Type u_1} {A : Type u_2} [normed_field R] [star_ring R] [normed_ring A] [normed_algebra R A] [star_ring A] [has_continuous_star A] [star_module R A] (a : A) :

normed_space R ↥(elemental_star_algebra R a)

Equations

elemental_star_algebra.normed_space a = normed_algebra.to_normed_space ↥(elemental_star_algebra R a)

@[protected, instance]

noncomputable def elemental_star_algebra.complex.normed_algebra {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] (a : A) :

normed_algebra ℂ ↥(elemental_star_algebra ℂ a)

Equations

elemental_star_algebra.complex.normed_algebra a = infer_instance

theorem spectrum_star_mul_self_of_is_star_normal {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (a : A) [is_star_normal a] :

spectrum ℂ (has_star.star a * a) ⊆ set.Icc 0 ↑‖has_star.star a * a‖

This lemma is used in the proof of star_subalgebra.is_unit_of_is_unit_of_is_star_normal, which in turn is the key to spectral permanence star_subalgebra.spectrum_eq, which is itself necessary for the continuous functional calculus. Using the continuous functional calculus, this lemma can be superseded by one that omits the is_star_normal hypothesis.

theorem elemental_star_algebra.is_unit_of_is_unit_of_is_star_normal {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] {a : A} [is_star_normal a] (h : is_unit a) :

is_unit ⟨a, _⟩

This is the key lemma on the way to establishing spectral permanence for C⋆-algebras, which is established in star_subalgebra.spectrum_eq. This lemma is superseded by star_subalgebra.coe_is_unit, which does not require an is_star_normal hypothesis and holds for any closed star subalgebra.

theorem star_subalgebra.is_unit_coe_inv_mem {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] {S : star_subalgebra ℂ A} (hS : is_closed ↑S) {x : A} (h : is_unit x) (hxS : x ∈ S) :

↑(h.unit)⁻¹ ∈ S

For x : A which is invertible in A, the inverse lies in any unital C⋆-subalgebra S containing x.

theorem star_subalgebra.coe_is_unit {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] {S : star_subalgebra ℂ A} (hS : is_closed ↑S) {x : ↥S} :

is_unit ↑x ↔ is_unit x

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 star_subalgebra.mem_spectrum_iff {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] {S : star_subalgebra ℂ A} (hS : is_closed ↑S) {x : ↥S} {z : ℂ} :

z ∈ spectrum ℂ x ↔ z ∈ spectrum ℂ ↑x

theorem star_subalgebra.spectrum_eq {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] {S : star_subalgebra ℂ A} (hS : is_closed ↑S) (x : ↥S) :

spectrum ℂ x = spectrum ℂ ↑x

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

noncomputable def elemental_star_algebra.character_space_to_spectrum {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (x : A) (φ : ↥(weak_dual.character_space ℂ ↥(elemental_star_algebra ℂ x))) :

↥(spectrum ℂ x)

The natural map from character_space ℂ (elemental_star_algebra ℂ x) to spectrum ℂ x given by evaluating φ at x. This is essentially just evaluation of the gelfand_transform of x, but because we want something in spectrum ℂ x, as opposed to spectrum ℂ ⟨x, elemental_star_algebra.self_mem ℂ x⟩ there is slightly more work to do.

Equations

elemental_star_algebra.character_space_to_spectrum x φ = ⟨⇑φ ⟨x, _⟩, _⟩

@[simp]

theorem elemental_star_algebra.character_space_to_spectrum_coe {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (x : A) (φ : ↥(weak_dual.character_space ℂ ↥(elemental_star_algebra ℂ x))) :

↑(elemental_star_algebra.character_space_to_spectrum x φ) = ⇑φ ⟨x, _⟩

theorem elemental_star_algebra.continuous_character_space_to_spectrum {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (x : A) :

continuous (elemental_star_algebra.character_space_to_spectrum x)

theorem elemental_star_algebra.bijective_character_space_to_spectrum {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (a : A) [is_star_normal a] :

function.bijective (elemental_star_algebra.character_space_to_spectrum a)

noncomputable def elemental_star_algebra.character_space_homeo {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (a : A) [is_star_normal a] :

↥(weak_dual.character_space ℂ ↥(elemental_star_algebra ℂ a)) ≃ₜ ↥(spectrum ℂ a)

The homeomorphism between the character space of the unital C⋆-subalgebra generated by a single normal element a : A and spectrum ℂ a.

Equations

elemental_star_algebra.character_space_homeo a = _.homeo_of_equiv_compact_to_t2

noncomputable def continuous_functional_calculus {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (a : A) [is_star_normal a] :

C(↥(spectrum ℂ a), ℂ ) ≃⋆ₐ[ℂ ] ↥(elemental_star_algebra ℂ a)

Continuous functional calculus. Given a normal element a : A of a unital C⋆-algebra, the continuous functional calculus is a star_alg_equiv from the complex-valued continuous functions on the spectrum of a to the unital C⋆-subalgebra generated by a. Moreover, this equivalence identifies (continuous_map.id ℂ).restrict (spectrum ℂ a)) with a; see continuous_functional_calculus_map_id. As such it extends the polynomial functional calculus.

Equations

continuous_functional_calculus a = (homeomorph.comp_star_alg_equiv' ℂ ℂ (elemental_star_algebra.character_space_homeo a)).trans (gelfand_star_transform ↥(elemental_star_algebra ℂ a)).symm

theorem continuous_functional_calculus_map_id {A : Type u_1} [normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [star_module ℂ A] [complete_space A] (a : A) [is_star_normal a] :

⇑(continuous_functional_calculus a) (continuous_map.restrict (spectrum ℂ a) (continuous_map.id ℂ)) = ⟨a, _⟩