Isolated character away from infinity

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_isolated_character_ne_infinity

theorem

Finds an isolated character distinct from the scalar character in a countable character space.

Statement

Let A be a complex C*-algebra, not assumed unital. Let D be a closed commutative unital star subalgebra of Unitization ℂ A with countable character space, and let 0 ≠ d ∈ D have zero scalar coordinate. There exists a character χ distinct from the restricted infinity character for which {χ} is open in the character space. This theorem itself does not assume that any representation represents a unique irreducible-representation class.

Assumptions

Let A be a complex C*-algebra, not assumed unital. Let D be a closed commutative unital star subalgebra of Unitization ℂ A with countable character space, and let 0 ≠ d ∈ D have zero scalar coordinate.

Conclusion

There exists a character χ distinct from the restricted infinity character for which {χ} is open in the character space. This theorem itself does not assume that any representation represents a unique irreducible-representation class.

Proof route

Gelfand-transform injectivity finds a character not annihilating d; the zero scalar coordinate excludes the infinity character. The complement of that closed singleton is a nonempty open Baire subspace. The countable T1 Baire lemma yields an isolated point there, and openness transfers back to the full character space.

Main citations

• MathlibAnnex.Topology.exists_isOpen_singleton

  Exact formal dependency; inspect the linked Card and exact source.

Lean source signature (exact)

theorem exists_isolated_character_ne_infinity
    (D : StarSubalgebra ℂ (Unitization ℂ A))
    [IsClosed (D : Set (Unitization ℂ A))]
    [IsMulCommutative D]
    [Countable (WeakDual.characterSpace ℂ D)]
    (d : D) (hd : d ≠ 0)
    (hdfst : (d : Unitization ℂ A).fst = 0) :
    ∃ chi : WeakDual.characterSpace ℂ D,
      chi ≠ infinityCharacterOn (A := A) D ∧
        IsOpen ({chi} : Set (WeakDual.characterSpace ℂ D))

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON