Commuting with applications of the continuous functional calculus

This file shows that if an element b commutes with both a and star a, then it commutes with cfc f a (or cfcₙ f a). In the case where a is selfadjoint, we may reduce the hypotheses.

Main results

• Commute.cfc and Commute.cfcₙ: an element commutes with cfc f a or cfcₙ f a if it commutes with both a and star a. Specialized versions for ℝ and ℝ≥0 or for IsSelfAdjoint a which do not require the user to show the element commutes with star a are provided for convenience.

Implementation notes

The proof of Commute.cfcHom and Commute.cfcₙHom could be made simpler by appealing to basic facts about double commutants, but doing so would require extra type class assumptions so that we can talk about topological star algebras. Instead, we avoid this to minimize the work Lean must do to call these lemmas, and give a straightforward proof by induction.

theorem Commute.cfcHom {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : p a) (hb₁ : Commute a b) (hb₂ : Commute (star a) b) (f : C(↑(spectrum 𝕜 a), 𝕜)) : Commute ((cfcHom ha) f) b

theorem IsSelfAdjoint.commute_cfcHom {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : p a) (ha' : IsSelfAdjoint a) (hb : Commute a b) (f : C(↑(spectrum 𝕜 a), 𝕜)) : Commute ((cfcHom ha) f) b

theorem Commute.cfc {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (hb₁ : Commute a b) (hb₂ : Commute (star a) b) (f : 𝕜 → 𝕜) : Commute (cfc f a) b

An element commutes with cfc f a if it commutes with both a and star a.

If the base ring is ℝ or ℝ≥0, see Commute.cfc_real or Commute.cfc_nnreal which don't require the Commute (star a) b hypothesis.

theorem IsSelfAdjoint.commute_cfc {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : IsSelfAdjoint a) (hb₁ : Commute a b) (f : 𝕜 → 𝕜) : Commute (cfc f a) b

For a selfadjoint, an element commutes with cfc f a if it commutes with a.

If the base ring is ℝ or ℝ≥0, see Commute.cfc_real or Commute.cfc_nnreal which don't require the IsSelfAdjoint hypothesis on a (due to the junk value cfc f a = 0).

theorem Commute.cfc_real {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] {a b : A} (hb : Commute a b) (f : ℝ → ℝ) : Commute (cfc f a) b

A version of Commute.cfc or IsSelfAdjoint.commute_cfc which does not require any interaction with star when the base ring is ℝ.

theorem Commute.cfc_nnreal {A : Type u_2} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] {a b : A} (hb : Commute a b) (f : NNReal → NNReal) : Commute (cfc f a) b

A version of Commute.cfc or IsSelfAdjoint.commute_cfc which does not require any interaction with star when the base ring is ℝ≥0.

theorem Commute.cfcₙHom {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : p a) (hb₁ : Commute a b) (hb₂ : Commute (star a) b) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) : Commute ((cfcₙHom ha) f) b

theorem IsSelfAdjoint.commute_cfcₙHom {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : p a) (ha' : IsSelfAdjoint a) (hb : Commute a b) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) : Commute ((cfcₙHom ha) f) b

theorem Commute.cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (hb₁ : Commute a b) (hb₂ : Commute (star a) b) (f : 𝕜 → 𝕜) : Commute (cfcₙ f a) b

An element commutes with cfcₙ f a if it commutes with both a and star a.

If the base ring is ℝ or ℝ≥0, see Commute.cfcₙ_real or Commute.cfcₙ_nnreal which don't require the Commute (star a) b hypothesis.

theorem IsSelfAdjoint.commute_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : IsSelfAdjoint a) (hb₁ : Commute a b) (f : 𝕜 → 𝕜) : Commute (cfcₙ f a) b

For a selfadjoint, an element commutes with cfcₙ f a if it commutes with a.

If the base ring is ℝ or ℝ≥0, see Commute.cfcₙ_real or Commute.cfcₙ_nnreal which don't require the IsSelfAdjoint hypothesis on a (due to the junk value cfcₙ f a = 0).

theorem Commute.cfcₙ_real {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] {a b : A} (hb : Commute a b) (f : ℝ → ℝ) : Commute (cfcₙ f a) b

A version of Commute.cfcₙ or IsSelfAdjoint.commute_cfcₙ which does not require any interaction with star when the base ring is ℝ.

theorem Commute.cfcₙ_nnreal {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] {a b : A} (hb : Commute a b) (f : NNReal → NNReal) : Commute (cfcₙ f a) b

A version of Commute.cfcₙ or IsSelfAdjoint.commute_cfcₙ which does not require any interaction with star when the base ring is ℝ≥0.