Theorems · Theorem · functional analysis

WeakDual.CharacterSpace.compContinuousMap_apply

∀ {A : Type u_1} {B : Type u_2} {𝕜 : 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] (ψ : A →⋆ₐ[𝕜] B)
  (φ : ↑(WeakDual.characterSpace 𝕜 B)),
  (WeakDual.CharacterSpace.compContinuousMap ψ) φ =
    WeakDual.CharacterSpace.equivAlgHom.symm ((WeakDual.CharacterSpace.equivAlgHom φ).comp ↑ψ)

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

NontriviallyNormedFieldNormedRingNormedAlgebraCompleteSpaceStarRingNormedRingNormedAlgebraCompleteSpaceStarRing