Theorems · Theorem · functional analysis

WeakDual.CharacterSpace.homeoEval_naturality

∀ {X : Type u_1} {Y : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  [inst_3 : T2Space X] [inst_4 : TopologicalSpace Y] [inst_5 : CompactSpace Y] [inst_6 : T2Space Y] (f : C(X, Y)),
  (↑(WeakDual.CharacterSpace.homeoEval Y 𝕜)).comp f =
    (WeakDual.CharacterSpace.compContinuousMap (ContinuousMap.compStarAlgHom' 𝕜 𝕜 f)).comp
      ↑(WeakDual.CharacterSpace.homeoEval X 𝕜)

Consider the contravariant functors between compact Hausdorff spaces and commutative unital C⋆algebras F : Cpct → CommCStarAlg := X ↦ C(X, ℂ) and G : CommCStarAlg → Cpct := A → characterSpace ℂ A whose actions on morphisms are given by WeakDual.CharacterSpace.compContinuousMap and ContinuousMap.compStarAlgHom', respectively. Then η : id → G ∘ F := WeakDual.CharacterSpace.homeoEval is a natural isomorphism implementing (half of) the duality between these categories. That is, for compact Hausdorff spaces X and Y, f : C(X, Y) the following diagram commutes: `` X η X > characterSpace ℂ C(X, ℂ) | | f (G ∘ F) f | | V V Y η Y > characterSpace ℂ C(Y, ℂ) ``

Defined in

Mathlib.Analysis.CStarAlgebra.GelfandDuality

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeTopologicalSpaceCompactSpaceT2SpaceTopologicalSpaceCompactSpaceT2Space