English
The homeomorphism η implementing the duality is natural with respect to continuous maps between compact spaces: it commutes with precomposition by f.
Русский
Единая естественность η, реализующая дуальность, сохраняется при непрерывных отображениях между компактными пространствами: диаграмма commuting с f.
LaTeX
$$$homeoEval_naturality: (homeoEval_Y) \\\\circ f = (f \\\\circ) \\\\circ (homeoEval_X)$$$
Lean4
/-- 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, ℂ)
```
-/
theorem homeoEval_naturality {X Y 𝕜 : Type*} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X]
[TopologicalSpace Y] [CompactSpace Y] [T2Space Y] (f : C(X, Y)) :
(homeoEval Y 𝕜 : C(_, _)).comp f = (f.compStarAlgHom' 𝕜 𝕜 |> compContinuousMap).comp (homeoEval X 𝕜 : C(_, _)) :=
rfl
