Documentation

Mathlib.Analysis.CstarAlgebra.ContinuousFunctionalCalculus.Unique

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.

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

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

Equations
Instances For
    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_neg_algebraMap {X : Type u_1} [TopologicalSpace X] (r : NNReal) :
    (-(algebraMap C(X, )) r).toNNReal = 0
    @[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

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

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

      Equations
      Instances For
        @[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 : ContinuousMapZero X ) (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 : ContinuousMapZero X ) (g : ContinuousMapZero X ) :
        (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
        @[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

        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' := }
        Instances For
          @[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