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) : C(↑(spectrum R b), R) →⋆ₐ[R] B

The star algebra homomorphism underlying ContinuousFunctionalCalculus.transfer. The proof that this is equal to that one is cfcHom_eq_cfcHomTransfer.

Equations

• cfcHomTransfer e hpq b hb = ((Homeomorph.compStarAlgEquiv' R R (Homeomorph.setCongr ⋯)).arrowCongr e) (cfcHom ⋯)

@[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) (a✝ : C(↑(spectrum R b), R)) : (cfcHomTransfer e hpq b hb) a✝ = e ((cfcHom ⋯) (a✝.comp ↑(Homeomorph.setCongr ⋯).symm))

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] [TopologicalSpace 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) (he : Continuous ⇑e) : Continuous ⇑(cfcHomTransfer e hpq b hb)

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) : (cfcHomTransfer e hpq b hb) (ContinuousMap.restrict (spectrum R b) (ContinuousMap.id R)) = b

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] [TopologicalSpace B] [Algebra R B] [instCFC : ContinuousFunctionalCalculus R A p] (e : A ≃⋆ₐ[R] B) (he : Continuous ⇑e) (hpq : ∀ (x : A), p x ↔ q (e x)) : ContinuousFunctionalCalculus R B q

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] [TopologicalSpace B] [Algebra R B] [instCFC : ContinuousFunctionalCalculus R A p] [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) : cfcHom hb = cfcHomTransfer e hpq b hb

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] [TopologicalSpace B] [Algebra R B] [instCFC : ContinuousFunctionalCalculus R A p] [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) : cfc f b = e (cfc f (e.symm b))

@[simp]

theorem AlgEquiv.quasispectrum_eq {F : Type u_4} {R : Type u_5} {A : Type u_6} {B : Type u_7} [CommSemiring R] [NonUnitalRing A] [NonUnitalRing B] [Module R A] [Module R B] [Star A] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B] (f : F) (a : A) : quasispectrum R (f a) = quasispectrum R a

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) : ContinuousMapZero (↑(quasispectrum R b)) R →⋆ₙₐ[R] B

The non-unital star algebra homomorphism underlying NonUnitalContinuousFunctionalCalculus.transfer. The proof that this is equal to that one is cfcₙHom_eq_cfcₙHomTransfer.

Equations

• cfcₙHomTransfer e hpq b hb = ((ContinuousMapZero.starAlgEquiv_precomp R (Homeomorph.setCongr ⋯) ⋯).arrowCongr' e) (cfcₙHom ⋯)

@[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.starAlgEquiv_precomp R (Homeomorph.setCongr ⋯) ⋯).symm a✝))

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] [TopologicalSpace 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) (he : Continuous ⇑e) : Continuous ⇑(cfcₙHomTransfer e hpq b hb)

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) : (cfcₙHomTransfer e hpq b hb) (ContinuousMapZero.id (quasispectrum R b)) = b

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] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [instCFC : NonUnitalContinuousFunctionalCalculus R A p] (e : A ≃⋆ₐ[R] B) (he : Continuous ⇑e) (hpq : ∀ (x : A), p x ↔ q (e x)) : NonUnitalContinuousFunctionalCalculus R B q

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] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [instCFC : NonUnitalContinuousFunctionalCalculus R A p] [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) : cfcₙHom hb = cfcₙHomTransfer e hpq b hb

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] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [instCFC : NonUnitalContinuousFunctionalCalculus R A p] [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) : cfcₙ f b = e (cfcₙ f (e.symm b))