Transporting a continuous functional calculus along an isomorphism

ContinuousFunctionalCalculus R A p is an existential statement about A: every a with p a admits a continuous injective ⋆-algebra map from symbols on its spectrum sending the identity symbol to a. Nothing in it is intrinsic to the carrier, so it transports along any isomorphism of topological R-⋆-algebras that matches the two predicates:

(A ≃⋆ₐ[R] B) → ContinuousFunctionalCalculus R B q → ContinuousFunctionalCalculus R A p

Mathlib has no such transport. Its instances are all built directly, and the two mechanisms it does provide for moving a calculus — SpectrumRestricts for shrinking the scalar ring and StarAlgHom images for subalgebras — do not cover a change of carrier.

Why this repository needs it

ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint is registered at 𝕜 = ℂ by Mathlib and at 𝕜 = ℝ by ForTauCeti/Analysis/InnerProductSpace/ RealContinuousFunctionalCalculus.lean, and an arbitrary RCLike field is isomorphic to one of those two. Transporting the calculus across that isomorphism is what turns the hypothesis block

[Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)]
[ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint]

that the operator-modulus and angle-operator API carries into an inferable instance, so that a scalar-generic theorem about angles between subspaces exposes [RCLike 𝕜] and nothing else.

The statement below is deliberately about an arbitrary pair of algebras rather than about that application: it is the general fact, and it is the shape a reviewer would expect to see upstream.

Only one direction of continuity is used

Continuous Φ.symm is a hypothesis; Continuous Φ is not, and adding it would be dead weight. The calculus of a is built as the calculus of Φ a followed by Φ.symm, so only that composite has to be continuous. Everything Φ itself contributes is algebraic: AlgEquiv.spectrum_eq identifies the spectra, and hpq identifies the predicates.

theorem ContinuousFunctionalCalculus.of_starAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [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] {p : A → Prop} {q : B → Prop} [ContinuousFunctionalCalculus R B q] (Φ : A ≃⋆ₐ[R] B) (hΦsymm : Continuous ⇑Φ.symm) (hpq : ∀ (a : A), p a ↔ q (Φ a)) : ContinuousFunctionalCalculus R A p

A continuous functional calculus transports along an isomorphism of topological R-⋆-algebras that matches the two predicates.

Every field of the class is read off through Φ: spectra agree by AlgEquiv.spectrum_eq, so the symbol algebras agree, and the calculus of a is the calculus of Φ a followed by Φ.symm.

Naturality of cfc

The transport also computes: an isomorphism carries the calculus of a to the calculus of Φ a, symbol by symbol. This is the form a consumer uses, and it needs the calculus on both sides rather than producing one.

theorem ContinuousFunctionalCalculus.map_cfc {R : Type u_1} {A : Type u_2} {B : Type u_3} [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] {p : A → Prop} {q : B → Prop} [ContinuousFunctionalCalculus R A p] [ContinuousFunctionalCalculus R B q] [ContinuousMap.UniqueHom R B] (Φ : A ≃⋆ₐ[R] B) (hΦ : Continuous ⇑Φ) (hpq : ∀ (a : A), p a ↔ q (Φ a)) (f : R → R) {a : A} (ha : p a) (hf : ContinuousOn f (spectrum R a)) : Φ (cfc f a) = cfc f (Φ a)

A ⋆-algebra isomorphism commutes with the continuous functional calculus.

Both Φ ∘ cfcHom and cfcHom at Φ a are continuous ⋆-algebra maps out of the symbol algebra sending the identity symbol to Φ a, and ContinuousMap.UniqueHom says there is only one such.