Uniqueness of the continuous functional calculus

Let s : Set 𝕜 be compact where 𝕜 is either ℝ or ℂ. By the Stone-Weierstrass theorem, the (star) subalgebra generated by polynomial functions on s is dense in C(s, 𝕜). Moreover, this star subalgebra is generated by X : 𝕜[X] (i.e., ContinuousMap.restrict s (.id 𝕜)) alone. Consequently, any continuous star 𝕜-algebra homomorphism with domain C(s, 𝕜), is uniquely determined by its value on X : 𝕜[X].

The same is true for 𝕜 := ℝ≥0, so long as the algebra A is an ℝ-algebra, which we establish by upgrading a map C((s : Set ℝ≥0), ℝ≥0) →⋆ₐ[ℝ≥0] A to C(((↑) '' s : Set ℝ), ℝ) →⋆ₐ[ℝ] A in the natural way, and then applying the uniqueness for ℝ-algebra homomorphisms.

This is the reason the UniqueContinuousFunctionalCalculus class exists in the first place, as opposed to simply appealing directly to Stone-Weierstrass to prove StarAlgHom.ext_continuousMap.

theorem RCLike.uniqueContinuousFunctionalCalculus_of_compactSpace_spectrum {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [TopologicalSpace A] [T2Space A] [Ring A] [StarRing A] [Algebra 𝕜 A] [h : ∀ (a : A), CompactSpace ↑(spectrum 𝕜 a)] : UniqueContinuousFunctionalCalculus 𝕜 A

instance RCLike.instUniqueContinuousFunctionalCalculus {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] : UniqueContinuousFunctionalCalculus 𝕜 A

Equations

• ⋯ = ⋯

noncomputable def ContinuousMap.toNNReal {X : Type u_1} [TopologicalSpace X] (f : C(X, ℝ)) : C(X, NNReal)

This map sends f : C(X, ℝ) to Real.toNNReal ∘ f, bundled as a continuous map C(X, ℝ≥0).

Equations

• f.toNNReal = ContinuousMap.realToNNReal.comp f

theorem ContinuousMap.continuous_toNNReal {X : Type u_1} [TopologicalSpace X] : Continuous ContinuousMap.toNNReal

@[simp]

theorem ContinuousMap.toNNReal_apply {X : Type u_1} [TopologicalSpace X] (f : C(X, ℝ)) (x : X) : f.toNNReal x = (f x).toNNReal

theorem ContinuousMap.toNNReal_add_add_neg_add_neg_eq {X : Type u_1} [TopologicalSpace X] (f g : C(X, ℝ)) : (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

theorem ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq {X : Type u_1} [TopologicalSpace X] (f g : C(X, ℝ)) : (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

@[simp]

theorem ContinuousMap.toNNReal_algebraMap {X : Type u_1} [TopologicalSpace X] (r : NNReal) : ((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = (algebraMap NNReal C(X, NNReal)) r

@[simp]

theorem ContinuousMap.toNNReal_neg_algebraMap {X : Type u_1} [TopologicalSpace X] (r : NNReal) : (-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = 0

@[simp]

theorem ContinuousMap.toNNReal_one {X : Type u_1} [TopologicalSpace X] : ContinuousMap.toNNReal 1 = 1

@[simp]

theorem ContinuousMap.toNNReal_neg_one {X : Type u_1} [TopologicalSpace X] : (-1).toNNReal = 0

noncomputable def StarAlgHom.realContinuousMapOfNNReal {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) : C(X, ℝ) →⋆ₐ[ℝ] A

Given a star ℝ≥0-algebra homomorphism φ from C(X, ℝ≥0) into an ℝ-algebra A, this is the unique extension of φ from C(X, ℝ) to A as a star ℝ-algebra homomorphism.

Equations

• φ.realContinuousMapOfNNReal = { toFun := fun (f : C(X, ℝ)) => φ f.toNNReal - φ (-f).toNNReal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem StarAlgHom.realContinuousMapOfNNReal_apply {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) (f : C(X, ℝ)) : φ.realContinuousMapOfNNReal f = φ f.toNNReal - φ (-f).toNNReal

theorem StarAlgHom.continuous_realContinuousMapOfNNReal {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [TopologicalRing A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) (hφ : Continuous ⇑φ) : Continuous ⇑φ.realContinuousMapOfNNReal

@[simp]

theorem StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) (f : C(X, NNReal)) : φ.realContinuousMapOfNNReal ({ toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe }.comp f) = φ f

theorem StarAlgHom.realContinuousMapOfNNReal_injective {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] : Function.Injective StarAlgHom.realContinuousMapOfNNReal

instance NNReal.instUniqueContinuousFunctionalCalculus {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [TopologicalRing A] [UniqueContinuousFunctionalCalculus ℝ A] : UniqueContinuousFunctionalCalculus NNReal A

Equations

• ⋯ = ⋯

theorem RCLike.uniqueNonUnitalContinuousFunctionalCalculus_of_compactSpace_quasispectrum {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [TopologicalSpace A] [T2Space A] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [h : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)] : UniqueNonUnitalContinuousFunctionalCalculus 𝕜 A

instance RCLike.instUniqueNonUnitalContinuousFunctionalCalculus {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [CompleteSpace A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : UniqueNonUnitalContinuousFunctionalCalculus 𝕜 A

Equations

• ⋯ = ⋯

noncomputable def ContinuousMapZero.toNNReal {X : Type u_1} [TopologicalSpace X] [Zero X] (f : ContinuousMapZero X ℝ) : ContinuousMapZero X NNReal

This map sends f : C(X, ℝ) to Real.toNNReal ∘ f, bundled as a continuous map C(X, ℝ≥0).

Equations

• f.toNNReal = { toContinuousMap := ContinuousMap.realToNNReal.comp ↑f, map_zero' := ⋯ }

@[simp]

theorem ContinuousMapZero.toNNReal_apply {X : Type u_1} [TopologicalSpace X] [Zero X] (f : ContinuousMapZero X ℝ) (x : X) : f.toNNReal x = (f x).toNNReal

theorem ContinuousMapZero.continuous_toNNReal {X : Type u_1} [TopologicalSpace X] [Zero X] : Continuous ContinuousMapZero.toNNReal

theorem ContinuousMapZero.toContinuousMapHom_toNNReal {X : Type u_1} [TopologicalSpace X] [Zero X] (f : ContinuousMapZero X ℝ) : (ContinuousMapZero.toContinuousMapHom f).toNNReal = ContinuousMapZero.toContinuousMapHom f.toNNReal

@[simp]

theorem ContinuousMapZero.toNNReal_smul {X : Type u_1} [TopologicalSpace X] [Zero X] (r : NNReal) (f : ContinuousMapZero X ℝ) : (r • f).toNNReal = r • f.toNNReal

@[simp]

theorem ContinuousMapZero.toNNReal_neg_smul {X : Type u_1} [TopologicalSpace X] [Zero X] (r : NNReal) (f : ContinuousMapZero X ℝ) : (-(r • f)).toNNReal = r • (-f).toNNReal

theorem ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eq {X : Type u_1} [TopologicalSpace X] [Zero X] (f g : ContinuousMapZero X ℝ) : (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

theorem ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq {X : Type u_1} [TopologicalSpace X] [Zero X] (f g : ContinuousMapZero X ℝ) : (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

noncomputable def NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal {X : Type u_1} [TopologicalSpace X] [Zero X] {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A) : ContinuousMapZero X ℝ →⋆ₙₐ[ℝ] A

Given a non-unital star ℝ≥0-algebra homomorphism φ from C(X, ℝ≥0)₀ into a non-unital ℝ-algebra A, this is the unique extension of φ from C(X, ℝ)₀ to A as a non-unital star ℝ-algebra homomorphism.

Equations

• φ.realContinuousMapZeroOfNNReal = { toFun := fun (f : ContinuousMapZero X ℝ) => φ f.toNNReal - φ (-f).toNNReal, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply {X : Type u_1} [TopologicalSpace X] [Zero X] {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A) (f : ContinuousMapZero X ℝ) : φ.realContinuousMapZeroOfNNReal f = φ f.toNNReal - φ (-f).toNNReal

theorem NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal {X : Type u_1} [TopologicalSpace X] [Zero X] {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] [TopologicalSpace A] [TopologicalRing A] (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A) (hφ : Continuous ⇑φ) : Continuous ⇑φ.realContinuousMapZeroOfNNReal

@[simp]

theorem NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal {X : Type u_1} [TopologicalSpace X] [Zero X] {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A) (f : ContinuousMapZero X NNReal) : φ.realContinuousMapZeroOfNNReal ({ toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe, map_zero' := ⋯ }.comp f) = φ f

theorem NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective {X : Type u_1} [TopologicalSpace X] [Zero X] {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] : Function.Injective NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal

instance NNReal.instUniqueNonUnitalContinuousFunctionalCalculus {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] [TopologicalSpace A] [TopologicalRing A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] : UniqueNonUnitalContinuousFunctionalCalculus NNReal A

Equations

• ⋯ = ⋯

theorem NonUnitalStarAlgHomClass.map_cfcₙ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalRing B] [StarRing B] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B] [NonUnitalContinuousFunctionalCalculus R p] [NonUnitalContinuousFunctionalCalculus R q] [UniqueNonUnitalContinuousFunctionalCalculus R B] [FunLike F A B] [NonUnitalAlgHomClass F S A B] [StarHomClass F A B] (φ : F) (f : R → R) (a : A) [CompactSpace ↑(quasispectrum R a)] (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (hφ : Continuous ⇑φ := by fun_prop) (ha : p a := by cfc_tac) (hφa : q (φ a) := by cfc_tac) : φ (cfcₙ f a) = cfcₙ f (φ a)

Non-unital star algebra homomorphisms commute with the non-unital continuous functional calculus.

theorem NonUnitalStarAlgHom.map_cfcₙ {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalRing B] [StarRing B] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B] [NonUnitalContinuousFunctionalCalculus R p] [NonUnitalContinuousFunctionalCalculus R q] [UniqueNonUnitalContinuousFunctionalCalculus R B] (φ : A →⋆ₙₐ[S] B) (f : R → R) (a : A) [CompactSpace ↑(quasispectrum R a)] (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (hφ : Continuous ⇑φ := by fun_prop) (ha : p a := by cfc_tac) (hφa : q (φ a) := by cfc_tac) : φ (cfcₙ f a) = cfcₙ f (φ a)

Non-unital star algebra homomorphisms commute with the non-unital continuous functional calculus. This version is specialized to A →⋆ₙₐ[S] B to allow for dot notation.

theorem StarAlgHomClass.map_cfc {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [Ring B] [StarRing B] [TopologicalSpace B] [Algebra R B] [CommSemiring S] [Algebra R S] [Algebra S A] [Algebra S B] [IsScalarTower R S A] [IsScalarTower R S B] [ContinuousFunctionalCalculus R p] [ContinuousFunctionalCalculus R q] [UniqueContinuousFunctionalCalculus R B] [FunLike F A B] [AlgHomClass F S A B] [StarHomClass F A B] (φ : F) (f : R → R) (a : A) [CompactSpace ↑(spectrum R a)] (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hφ : Continuous ⇑φ := by fun_prop) (ha : p a := by cfc_tac) (hφa : q (φ a) := by cfc_tac) : φ (cfc f a) = cfc f (φ a)

Star algebra homomorphisms commute with the continuous functional calculus.

theorem StarAlgHom.map_cfc {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [Ring B] [StarRing B] [TopologicalSpace B] [Algebra R B] [CommSemiring S] [Algebra R S] [Algebra S A] [Algebra S B] [IsScalarTower R S A] [IsScalarTower R S B] [ContinuousFunctionalCalculus R p] [ContinuousFunctionalCalculus R q] [UniqueContinuousFunctionalCalculus R B] (φ : A →⋆ₐ[S] B) (f : R → R) (a : A) [CompactSpace ↑(spectrum R a)] (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (hφ : Continuous ⇑φ := by fun_prop) (ha : p a := by cfc_tac) (hφa : q (φ a) := by cfc_tac) : φ (cfc f a) = cfc f (φ a)

Star algebra homomorphisms commute with the continuous functional calculus. This version is specialized to A →⋆ₐ[S] B to allow for dot notation.