Theorems · Theorem · functional analysis

gelfandStarTransform_naturality

∀ {A : Type u_1} {B : Type u_2} [inst : CommCStarAlgebra A] [inst_1 : CommCStarAlgebra B] (φ : A →⋆ₐ[ℂ] B),
  (↑(gelfandStarTransform B)).comp φ =
    (ContinuousMap.compStarAlgHom' ℂ ℂ (WeakDual.CharacterSpace.compContinuousMap φ)).comp ↑(gelfandStarTransform A)

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, ℂ) ``

Defined in

Mathlib.Analysis.CStarAlgebra.GelfandDuality

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommCStarAlgebraCommCStarAlgebra