Transfer instances of the continuous functional calculus #
One may transfer instances of the continuous functional calculus across a star algebra equivalence, so long as this equivalence is continuous. Crucially, its inverse need not be continuous. This allows to, for example, equip type synonyms of a C⋆-algebra with weaker topologies with instances of the continuous functional calculus.
Main declarations #
ContinuousFunctionalCalculus.transfer: transfer a continuous functional calculus instance through a continuous (in only one direction)StarAlgEquiv.NonUnitalContinuousFunctionalCalculus.transfer: transfer a non-unital continuous functional calculus instance through a continuous (in only one direction)StarAlgEquiv.cfc_eq_cfc_transfer: the equality between a functional calculus and its transferred instance.cfcₙ_eq_cfcₙ_transfer: the equality between a functional calculus and its transferred instance.
noncomputable def
cfcHomTransfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
Transfer cfcHom across a star algebra equivalence.
Equations
- cfcHomTransfer e hpq b hb = ((Homeomorph.compStarAlgEquiv' R R (Homeomorph.setCongr ⋯)).arrowCongr e) (cfcHom ⋯)
Instances For
@[simp]
theorem
cfcHomTransfer_apply
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
(x : C(↑(spectrum R b), R))
:
theorem
cfcHomTransfer_injective
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
Function.Injective ⇑(cfcHomTransfer e hpq b hb)
theorem
cfcHomTransfer_id
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
theorem
continuous_cfcHomTransfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
(he : Continuous ⇑e)
:
Continuous ⇑(cfcHomTransfer e hpq b hb)
theorem
ContinuousFunctionalCalculus.transfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
:
Transfer a continuous functional calculus instance to a type synonym with a weaker topology.
theorem
cfcHom_eq_cfcHomTransfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
[ContinuousFunctionalCalculus R B q]
[ContinuousMap.UniqueHom R B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
theorem
cfc_eq_cfc_transfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[Ring B]
[StarRing B]
[Algebra R B]
[instCFC : ContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
[ContinuousFunctionalCalculus R B q]
[ContinuousMap.UniqueHom R B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
(f : R → R)
(b : B)
:
noncomputable def
cfcₙHomTransfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
Transfer cfcₙHom across a star algebra equivalence.
Equations
- cfcₙHomTransfer e hpq b hb = ((ContinuousMapZero.starAlgEquivPrecomp R (Homeomorph.setCongr ⋯) ⋯).arrowCongr' e) (cfcₙHom ⋯)
Instances For
@[simp]
theorem
cfcₙHomTransfer_apply
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
(a✝ : ContinuousMapZero (↑(quasispectrum R b)) R)
:
(cfcₙHomTransfer e hpq b hb) a✝ = e ((cfcₙHom ⋯) ((ContinuousMapZero.starAlgEquivPrecomp R (Homeomorph.setCongr ⋯) ⋯).symm a✝))
theorem
cfcₙHomTransfer_injective
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
Function.Injective ⇑(cfcₙHomTransfer e hpq b hb)
theorem
cfcₙHomTransfer_id
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
theorem
continuous_cfcₙHomTransfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
(e : A ≃⋆ₐ[R] B)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
(he : Continuous ⇑e)
:
Continuous ⇑(cfcₙHomTransfer e hpq b hb)
theorem
NonUnitalContinuousFunctionalCalculus.transfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
[IsScalarTower R B B]
[SMulCommClass R B B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
:
Transfer a continuous functional calculus instance to a type synonym with a weaker topology.
@[deprecated NonUnitalContinuousFunctionalCalculus.transfer (since := "2026-09-02")]
theorem
NonUnitalContinuousFunctionCalculus.transfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
[IsScalarTower R B B]
[SMulCommClass R B B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
:
Alias of NonUnitalContinuousFunctionalCalculus.transfer.
Transfer a continuous functional calculus instance to a type synonym with a weaker topology.
theorem
cfcₙHom_eq_cfcₙHomTransfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
[IsScalarTower R B B]
[SMulCommClass R B B]
[NonUnitalContinuousFunctionalCalculus R B q]
[ContinuousMapZero.UniqueHom R B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
(b : B)
(hb : q b)
:
theorem
cfcₙ_eq_cfcₙ_transfer
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{p : A → Prop}
{q : B → Prop}
[CommSemiring R]
[Nontrivial R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module R A]
[IsScalarTower R A A]
[SMulCommClass R A A]
[NonUnitalRing B]
[StarRing B]
[Module R B]
[instCFC : NonUnitalContinuousFunctionalCalculus R A p]
[TopologicalSpace B]
[IsScalarTower R B B]
[SMulCommClass R B B]
[NonUnitalContinuousFunctionalCalculus R B q]
[ContinuousMapZero.UniqueHom R B]
(e : A ≃⋆ₐ[R] B)
(he : Continuous ⇑e)
(hpq : ∀ (x : A), p x ↔ q (e x))
(f : R → R)
(b : B)
: