Documentation

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Restriction of the continuous functional calculus to a scalar subring #

The main declaration in this file is:

This will allow us to take an instance of the ContinuousFunctionalCalculusIsStarNormal and produce both of the instances ContinuousFunctionalCalculusIsSelfAdjoint and ContinuousFunctionalCalculus ℝ≥0 (0 ≤ ·) simply by proving:

  1. IsSelfAdjoint x ↔ IsStarNormal x ∧ SpectrumRestricts Complex.re x,
  2. 0 ≤ x ↔ IsSelfAdjoint x ∧ SpectrumRestricts Real.toNNReal x.
def SpectrumRestricts.homeomorph {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] [ContinuousSMul R S] {a : A} {f : C(S, R)} (h : SpectrumRestricts a f) :
(spectrum S a) ≃ₜ (spectrum R a)

The homeomorphism spectrum S a ≃ₜ spectrum R a induced by SpectrumRestricts a f.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem SpectrumRestricts.compactSpace {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] {a : A} (f : C(S, R)) (h : SpectrumRestricts a f) [h_cpct : CompactSpace (spectrum S a)] :
    @[simp]
    theorem SpectrumRestricts.starAlgHom_apply {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R] [TopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [TopologicalSpace S] [TopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A} (φ : C((spectrum S a), S) →⋆ₐ[S] A) {f : C(S, R)} (h : SpectrumRestricts a f) :
    ∀ (a_1 : C((spectrum R a), R)), (SpectrumRestricts.starAlgHom φ h) a_1 = φ ({ toFun := (StarAlgHom.ofId R S), continuous_toFun := }.comp (a_1.comp { toFun := Subtype.map f , continuous_toFun := }))
    def SpectrumRestricts.starAlgHom {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R] [TopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [TopologicalSpace S] [TopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A} (φ : C((spectrum S a), S) →⋆ₐ[S] A) {f : C(S, R)} (h : SpectrumRestricts a f) :

    If the spectrum of an element restricts to a smaller scalar ring, then a continuous functional calculus over the larger scalar ring descends to the smaller one.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem SpectrumRestricts.cfc {R : Type u_1} {S : Type u_2} {A : Type u_3} {p : AProp} {q : AProp} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [MetricSpace S] [TopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra S A] [Algebra R S] [Algebra R A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [TopologicalSpace A] [ContinuousFunctionalCalculus S q] [CompleteSpace R] (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0) (h : ∀ (a : A), p a q a SpectrumRestricts a f) :

      Given a ContinuousFunctionalCalculus S q. If we form the predicate p for a : A characterized by: q a and the spectrum of a restricts to the scalar subring R via f : C(S, R), then we can get a restricted functional calculus ContinuousFunctionalCalculus R p.

      theorem SpectrumRestricts.cfc_eq_restrict {R : Type u_1} {S : Type u_2} {A : Type u_3} {p : AProp} {q : AProp} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [MetricSpace S] [TopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra S A] [Algebra R S] [Algebra R A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [TopologicalSpace A] [ContinuousFunctionalCalculus S q] [CompleteSpace R] [ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a) (h : SpectrumRestricts a f) (g : RR) :
      cfc g a = cfc (fun (x : S) => (algebraMap R S) (g (f x))) a
      def QuasispectrumRestricts.homeomorph {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] [ContinuousSMul R S] [IsScalarTower S A A] [SMulCommClass S A A] {a : A} {f : C(S, R)} (h : QuasispectrumRestricts a f) :

      The homeomorphism quasispectrum S a ≃ₜ quasispectrum R a induced by QuasispectrumRestricts a f.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem QuasispectrumRestricts.nonUnitalStarAlgHom_apply {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R] [TopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [TopologicalSpace S] [TopologicalRing S] [ContinuousStar S] [NonUnitalRing A] [StarRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A} (φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A) {f : C(S, R)} (h : QuasispectrumRestricts a f) :
        ∀ (a_1 : ContinuousMapZero (↑(quasispectrum R a)) R), (QuasispectrumRestricts.nonUnitalStarAlgHom φ h) a_1 = φ ({ toFun := (StarAlgHom.ofId R S), continuous_toFun := , map_zero' := }.comp (a_1.comp { toFun := Subtype.map f , continuous_toFun := , map_zero' := }))

        If the quasispectrum of an element restricts to a smaller scalar ring, then a non-unital continuous functional calculus over the larger scalar ring descends to the smaller one.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem QuasispectrumRestricts.cfc {R : Type u_1} {S : Type u_2} {A : Type u_3} {p : AProp} {q : AProp} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [MetricSpace S] [TopologicalRing S] [ContinuousStar S] [NonUnitalRing A] [StarRing A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Algebra R S] [Module R A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus S q] [CompleteSpace R] [IsScalarTower R A A] [SMulCommClass R A A] (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0) (h : ∀ (a : A), p a q a QuasispectrumRestricts a f) :

          Given a NonUnitalContinuousFunctionalCalculus S q. If we form the predicate p for a : A characterized by: q a and the quasispectrum of a restricts to the scalar subring R via f : C(S, R), then we can get a restricted functional calculus NonUnitalContinuousFunctionalCalculus R p.

          theorem QuasispectrumRestricts.cfcₙ_eq_restrict {R : Type u_1} {S : Type u_2} {A : Type u_3} {p : AProp} {q : AProp} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [MetricSpace S] [TopologicalRing S] [ContinuousStar S] [NonUnitalRing A] [StarRing A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Algebra R S] [Module R A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus S q] [CompleteSpace R] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a f) (g : RR) :
          cfcₙ g a = cfcₙ (fun (x : S) => (algebraMap R S) (g (f x))) a