MATHLIBANNEX / CANONICAL DECLARATION CARD

The full character space is countable

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton

theorem

Uses separated unit eigenvectors to count the non-scalar characters, then restores the one scalar character.

Statement

Let be a nonzero complex -algebra, with no unit assumed. Let be a separable complex Hilbert space, and let be nonzero irreducible and represent the unique unitary-equivalence class of nonzero irreducible comparisons. If is a norm-closed unital -subalgebra of , then the entire character space of is countable. Here denotes the scalar-coordinate character of .

Assumptions

Commutativity of is not an additional hypothesis in this theorem. Separability is imposed on , not on or .

Conclusion

Countability includes the scalar character , as well as all the other characters.

Proof route

Choose a unit eigenvector for each non-scalar character, prove their pairwise orthogonality, count disjoint small balls using separability, and adjoin the scalar character.

Proof steps

  1. Let . For each , apply A joint unit eigenvector for each non-scalar character with the same and that . Closedness of and its inequality from the scalar character supply the remaining hypotheses. Fix a unit vector for each character so that

    where .

  2. If , choose with . Put . Since is -closed, the eigenvector equation also gives . With the inner product linear in its second argument,

    The two coefficients differ, so .

  3. Consequently

    The open balls are therefore nonempty and pairwise disjoint. Choose a countable dense set in ; each ball contains a point of it, and disjoint balls require different points. Thus is countable. This is the separated-ball argument in Countability of the non-scalar character space.

  4. Finally

    Adding this one character to the countable set proves countability of the entire character space.

Main citations

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)
In the source Mathematical meaning
[Nontrivial A] The algebra is nonzero: . This condition does not say whether a unit is assumed; that information comes from the surrounding -algebra structure.
[TopologicalSpace.SeparableSpace H] The representation space has a countable dense subset, used to count the disjoint balls.
(pi : NonUnitalCStarRepresentation A H) The specified -representation ; no unit-preservation equation is required.
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) The specified representation is nonzero irreducible, and every nonzero irreducible -representation of the same algebra is unitarily equivalent to it.
(D : StarSubalgebra ℂ (Unitization ℂ A)) The unital -subalgebra of whose characters are being counted; no commutativity binder occurs.
[IsClosed (D : Set (Unitization ℂ A))] That is norm closed.
Countable (WeakDual.characterSpace ℂ D) The set of all nonzero continuous complex characters of is countable, including the scalar-coordinate character restricted to .

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton

Accepted content SHA-256: 6171dfe84b4bd371c4b8d431157f618e323b22aa042125daa2799444c4fefc18

Accepted source guide SHA-256: 6e9af28c687a9329f00ac4879a29fce4fcd65ee212edc36f94d196fd8aa278e0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑