Theorems · Theorem · functional analysis

RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict

∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : PseudoEMetricSpace E]
  {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
  Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ)
      (Subalgebra.comap (BoundedContinuousFunction.AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm ⋯)
        (Subalgebra.restrictScalars ℝ A.toSubalgebra)) =
    Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ
        (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).toSubalgebra)

On a star subalgebra of bounded continuous functions, the operations "restrict scalars to ℝ" and "forget that a bounded continuous function is a bounded" commute.

Defined in

Mathlib.Analysis.RCLike.BoundedContinuous

Cited by

1 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikePseudoEMetricSpace