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 : C(X, ℝ)) (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 : C(X, ℝ)) (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] : 1.toNNReal = 1

@[simp]

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

@[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

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' := ⋯ }

theorem StarAlgHom.continuous_realContinuousMapOfNNReal {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℝ 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} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalRing A] [UniqueContinuousFunctionalCalculus ℝ A] : UniqueContinuousFunctionalCalculus NNReal A

Equations

• ⋯ = ⋯