Countability of the full character space

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton

theorem

Shows that the full character space of a closed unitization subalgebra is countable when π is a separably acting representative of the unique irreducible-representation class.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a separable complex Hilbert space; let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A; and let D be a closed unital star subalgebra of Unitization ℂ A. The entire character space of D is countable, including the distinguished scalar character.

Assumptions

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a separable complex Hilbert space; let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A; and let D be a closed unital star subalgebra of Unitization ℂ A.

Conclusion

The entire character space of D is countable, including the distinguished scalar character.

Proof route

For each character other than infinityCharacterOn D, the prior source theorem supplies a joint unit eigenvector. Distinct characters give orthogonal vectors, so separability of H makes that complement countable. The source then maps the disjoint sum of the complement and one Unit onto the entire character space.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity

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

Lean source signature (exact)

theorem countable_characterSpace_of_nonUnital_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (D : StarSubalgebra ℂ (Unitization ℂ A))
    [IsClosed (D : Set (Unitization ℂ A))] :
    Countable (WeakDual.characterSpace ℂ D)

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