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 used 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 ℂ A IsStarNormal and produce both of the instances
ContinuousFunctionalCalculus ℝ A IsSelfAdjoint and ContinuousFunctionalCalculus ℝ≥0 A (0 ≤ ·)
simply by proving:
IsSelfAdjoint x ↔ IsStarNormal x ∧ SpectrumRestricts Complex.re x,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)
:
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)]
:
CompactSpace ↑(spectrum R a)
def
SpectrumRestricts.starAlgHom
{R : Type u}
{S : Type v}
{A : Type w}
[Semifield R]
[StarRing R]
[TopologicalSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[TopologicalSpace S]
[IsTopologicalSemiring 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
@[simp]
theorem
SpectrumRestricts.starAlgHom_apply
{R : Type u}
{S : Type v}
{A : Type w}
[Semifield R]
[StarRing R]
[TopologicalSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[TopologicalSpace S]
[IsTopologicalSemiring 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✝ : C(↑(spectrum R a), R))
:
(starAlgHom φ h) a✝ = φ
({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
(a✝.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
theorem
SpectrumRestricts.starAlgHom_id
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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)
:
theorem
SpectrumRestricts.starAlgHom_injective
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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}
(hφ : Function.Injective ⇑φ)
{f : C(S, R)}
(h : SpectrumRestricts a ⇑f)
(halg : Function.Injective ⇑(algebraMap R S))
:
Function.Injective ⇑(starAlgHom φ h)
theorem
SpectrumRestricts.continuous_starAlgHom
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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]
{a : A}
{φ : C(↑(spectrum S a), S) →⋆ₐ[S] A}
(hφ : Continuous ⇑φ)
{f : C(S, R)}
(h : SpectrumRestricts a ⇑f)
:
Continuous ⇑(starAlgHom φ h)
theorem
SpectrumRestricts.isClosedEmbedding_starAlgHom
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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]
[CompleteSpace R]
{a : A}
{φ : C(↑(spectrum S a), S) →⋆ₐ[S] A}
(hφ : Topology.IsClosedEmbedding ⇑φ)
{f : C(S, R)}
(h : SpectrumRestricts a ⇑f)
(halg : IsUniformEmbedding ⇑(algebraMap R S))
:
theorem
SpectrumRestricts.cfc
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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 A q]
(f : C(S, R))
(halg : Topology.IsClosedEmbedding ⇑(algebraMap R S))
(h0 : p 0)
(h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f)
:
Given a ContinuousFunctionalCalculus S A 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 A p.
theorem
SpectrumRestricts.cfcHom_eq_restrict
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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 A q]
[ContinuousFunctionalCalculus R A p]
[ContinuousMap.UniqueHom R A]
(f : C(S, R))
{a : A}
(hpa : p a)
(hqa : q a)
(h : SpectrumRestricts a ⇑f)
:
theorem
SpectrumRestricts.cfc_eq_restrict
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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 A q]
[ContinuousFunctionalCalculus R A p]
[ContinuousMap.UniqueHom R A]
(f : C(S, R))
(halg : Topology.IsClosedEmbedding ⇑(algebraMap R S))
{a : A}
(hpa : p a)
(hqa : q a)
(h : SpectrumRestricts a ⇑f)
(g : R → R)
:
theorem
SpectrumRestricts.closedEmbeddingCFC
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Semifield S]
[StarRing S]
[MetricSpace S]
[IsTopologicalSemiring 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]
[ClosedEmbeddingContinuousFunctionalCalculus S A q]
[ContinuousMap.UniqueHom R A]
[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 A 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 A p.
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
def
QuasispectrumRestricts.nonUnitalStarAlgHom
{R : Type u}
{S : Type v}
{A : Type w}
[Semifield R]
[StarRing R]
[TopologicalSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[TopologicalSpace S]
[IsTopologicalRing 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)
:
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
@[simp]
theorem
QuasispectrumRestricts.nonUnitalStarAlgHom_apply
{R : Type u}
{S : Type v}
{A : Type w}
[Semifield R]
[StarRing R]
[TopologicalSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[TopologicalSpace S]
[IsTopologicalRing 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✝ : ContinuousMapZero (↑(quasispectrum R a)) R)
:
(nonUnitalStarAlgHom φ h) a✝ = φ
({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
(a✝.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
theorem
QuasispectrumRestricts.nonUnitalStarAlgHom_id
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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]
{a : A}
{φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A}
{f : C(S, R)}
(h : QuasispectrumRestricts a ⇑f)
(h_id : φ (ContinuousMapZero.id (quasispectrum S a)) = a)
:
theorem
QuasispectrumRestricts.nonUnitalStarAlgHom_injective
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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]
{a : A}
{φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A}
(hφ : Function.Injective ⇑φ)
{f : C(S, R)}
(h : QuasispectrumRestricts a ⇑f)
(halg : Function.Injective ⇑(algebraMap R S))
:
theorem
QuasispectrumRestricts.continuous_nonUnitalStarAlgHom
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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]
{a : A}
{φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A}
(hφ : Continuous ⇑φ)
{f : C(S, R)}
(h : QuasispectrumRestricts a ⇑f)
:
Continuous ⇑(nonUnitalStarAlgHom φ h)
theorem
QuasispectrumRestricts.isClosedEmbedding_nonUnitalStarAlgHom
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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]
[CompleteSpace R]
{a : A}
{φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A}
(hφ : Topology.IsClosedEmbedding ⇑φ)
{f : C(S, R)}
(h : QuasispectrumRestricts a ⇑f)
(halg : IsUniformEmbedding ⇑(algebraMap R S))
:
theorem
QuasispectrumRestricts.cfc
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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 A q]
[IsScalarTower R A A]
[SMulCommClass R A A]
(f : C(S, R))
(halg : Topology.IsClosedEmbedding ⇑(algebraMap R S))
(h0 : p 0)
(h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f)
:
Given a NonUnitalContinuousFunctionalCalculus S A 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 A p.
theorem
QuasispectrumRestricts.cfcₙHom_eq_restrict
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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 A q]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalContinuousFunctionalCalculus R A p]
[ContinuousMapZero.UniqueHom R A]
(f : C(S, R))
{a : A}
(hpa : p a)
(hqa : q a)
(h : QuasispectrumRestricts a ⇑f)
:
theorem
QuasispectrumRestricts.cfcₙ_eq_restrict
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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 A q]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalContinuousFunctionalCalculus R A p]
[ContinuousMapZero.UniqueHom R A]
(f : C(S, R))
(halg : Topology.IsClosedEmbedding ⇑(algebraMap R S))
{a : A}
(hpa : p a)
(hqa : q a)
(h : QuasispectrumRestricts a ⇑f)
(g : R → R)
:
theorem
QuasispectrumRestricts.nonUnitalClosedEmbeddingCFC
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{p q : A → Prop}
[Semifield R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Field S]
[StarRing S]
[MetricSpace S]
[IsTopologicalRing 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]
[NonUnitalClosedEmbeddingContinuousFunctionalCalculus S A q]
[IsScalarTower R A A]
[SMulCommClass R A A]
[ContinuousMapZero.UniqueHom R A]
[CompleteSpace R]
(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 A 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 A p.