Restriction of the continuous functional calculus to a scalar subring #
The main declaration in this file is:
SpectrumRestricts.cfc: builds a continuous functional calculus over a subring of scalars. This is use for automatically deriving the continuous functional calculi on selfadjoint or positive elements from the one for normal elements.
This will allow us to take an instance of the
ContinuousFunctionalCalculus ℂ IsStarNormal and produce both of the instances
ContinuousFunctionalCalculus ℝ IsSelfAdjoint and ContinuousFunctionalCalculus ℝ≥0 (0 ≤ ·)
simply by proving:
IsSelfAdjoint x ↔ IsStarNormal x ∧ SpectrumRestricts Complex.re x,0 ≤ x ↔ IsSelfAdjoint x ∧ SpectrumRestricts Real.toNNReal x.
theorem
SpectrumRestricts.compactSpace
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[CommSemiring R]
[CommSemiring 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)]
:
CompactSpace ↑(spectrum R a)
@[simp]
theorem
SpectrumRestricts.starAlgHom_apply
{R : Type u}
{S : Type v}
{A : Type w}
[CommSemiring R]
[StarRing R]
[TopologicalSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring 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}
[CommSemiring R]
[StarRing R]
[TopologicalSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring 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.closedEmbedding_starAlgHom
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring S]
[StarRing S]
[MetricSpace S]
[TopologicalSemiring S]
[ContinuousStar S]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra S A]
[Algebra R S]
[Algebra R A]
[IsScalarTower R S A]
[StarModule R S]
[ContinuousSMul R S]
[CompleteSpace R]
{a : A}
{φ : C(↑(spectrum S a), S) →⋆ₐ[S] A}
(hφ : ClosedEmbedding ⇑φ)
{f : C(S, R)}
(h : SpectrumRestricts a ⇑f)
(h_isom : Isometry ⇑(algebraMap R S))
[h_cpct : CompactSpace ↑(spectrum S a)]
:
theorem
SpectrumRestricts.starAlgHom_id
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring 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]
{a : A}
{φ : C(↑(spectrum S a), S) →⋆ₐ[S] A}
{f : C(S, R)}
(h : SpectrumRestricts a ⇑f)
(h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a)
:
(SpectrumRestricts.starAlgHom φ h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
theorem
SpectrumRestricts.cfc
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p : A → Prop}
{q : A → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring S]
[StarRing S]
[MetricSpace S]
[TopologicalSemiring S]
[ContinuousStar S]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra S A]
[ContinuousFunctionalCalculus S q]
[Algebra R S]
[Algebra R A]
[IsScalarTower R S A]
[StarModule R S]
[ContinuousSMul R S]
[CompleteSpace R]
(f : C(S, R))
(h_isom : Isometry ⇑(algebraMap R S))
(h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f)
(h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a))
:
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.cfcHom_eq_restrict
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p : A → Prop}
{q : A → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring S]
[StarRing S]
[MetricSpace S]
[TopologicalSemiring S]
[ContinuousStar S]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra S A]
[ContinuousFunctionalCalculus S q]
[Algebra R S]
[Algebra R A]
[IsScalarTower R S A]
[StarModule R S]
[ContinuousSMul R S]
[CompleteSpace R]
[ContinuousFunctionalCalculus R p]
[UniqueContinuousFunctionalCalculus R A]
(f : C(S, R))
(h_isom : Isometry ⇑(algebraMap R S))
{a : A}
(hpa : p a)
(hqa : q a)
(h : SpectrumRestricts a ⇑f)
[CompactSpace ↑(spectrum S a)]
:
cfcHom hpa = SpectrumRestricts.starAlgHom (cfcHom hqa) h
theorem
SpectrumRestricts.cfc_eq_restrict
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p : A → Prop}
{q : A → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[CommSemiring S]
[StarRing S]
[MetricSpace S]
[TopologicalSemiring S]
[ContinuousStar S]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra S A]
[ContinuousFunctionalCalculus S q]
[Algebra R S]
[Algebra R A]
[IsScalarTower R S A]
[StarModule R S]
[ContinuousSMul R S]
[CompleteSpace R]
[ContinuousFunctionalCalculus R p]
[UniqueContinuousFunctionalCalculus R A]
(f : C(S, R))
(h_isom : Isometry ⇑(algebraMap R S))
{a : A}
(hpa : p a)
(hqa : q a)
(h : SpectrumRestricts a ⇑f)
[CompactSpace ↑(spectrum S a)]
(g : R → R)
:
cfc g a = cfc (fun (x : S) => (algebraMap R S) (g (f x))) a