Theorems · Definition · functional analysis

StarAlgebra.elemental.characterSpaceToSpectrum

{A : Type u_1} →
  [inst : CStarAlgebra A] → (x : A) → ↑(WeakDual.characterSpace ℂ ↥(StarAlgebra.elemental ℂ x)) → ↑(spectrum ℂ x)

The natural map from characterSpace ℂ (elemental ℂ x) to spectrum ℂ x given by evaluating φ at x. This is essentially just evaluation of the gelfandTransform of x, but because we want something in spectrum ℂ x, as opposed to spectrum ℂ ⟨x, elemental.self_mem ℂ x⟩ there is slightly more work to do.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CStarAlgebra