Theorems · Theorem · functional analysis

WeakDual.CharacterSpace.compContinuousMap_comp

∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [inst_3 : CompleteSpace A] [inst_4 : StarRing A] [inst_5 : NormedRing B]
  [inst_6 : NormedAlgebra 𝕜 B] [inst_7 : CompleteSpace B] [inst_8 : StarRing B] [inst_9 : NormedRing C]
  [inst_10 : NormedAlgebra 𝕜 C] [inst_11 : CompleteSpace C] [inst_12 : StarRing C] (ψ₂ : B →⋆ₐ[𝕜] C) (ψ₁ : A →⋆ₐ[𝕜] B),
  WeakDual.CharacterSpace.compContinuousMap (ψ₂.comp ψ₁) =
    (WeakDual.CharacterSpace.compContinuousMap ψ₁).comp (WeakDual.CharacterSpace.compContinuousMap ψ₂)

WeakDual.CharacterSpace.compContinuousMap is functorial.

Defined in

Mathlib.Analysis.CStarAlgebra.GelfandDuality

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraCompleteSpaceStarRingNormedRingNormedAlgebraCompleteSpaceStarRingNormedRingNormedAlgebraCompleteSpaceStarRing