English
The Gelfand transform is natural with respect to star-algebra morphisms: composing with φ is the same as precomposing via the Gelfand transform.
Русский
Преобразование Гельфанда естественно по отношению к гомоморфизмам звёздных алгебр: композиция с φ равна предкомпозиции через преобразование Гельфанда.
LaTeX
$$$(gelfandStarTransform B) \circ φ = (compContinuousMap φ) \circ (gelfandStarTransform A)$$$
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 → F ∘ G := gelfandStarTransform` is a natural isomorphism implementing (half of)
the duality between these categories. That is, for commutative unital C⋆-algebras `A` and `B` and
`φ : A →⋆ₐ[ℂ] B` the following diagram commutes:
```
A --- η A ---> C(characterSpace ℂ A, ℂ)
| |
φ (F ∘ G) φ
| |
V V
B --- η B ---> C(characterSpace ℂ B, ℂ)
```
-/
theorem gelfandStarTransform_naturality {A B : Type*} [CommCStarAlgebra A] [CommCStarAlgebra B] (φ : A →⋆ₐ[ℂ] B) :
(gelfandStarTransform B : _ →⋆ₐ[ℂ] _).comp φ =
(compContinuousMap φ |>.compStarAlgHom' ℂ ℂ).comp (gelfandStarTransform A : _ →⋆ₐ[ℂ] _) :=
by rfl
