MATHLIBANNEX / CANONICAL DECLARATION CARD

A unital singleton model acts in finite dimension

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton

theorem

Uses simplicity to put the identity operator in the compact image ideal.

Statement

Let be a nonzero unital complex -algebra and let be a nonzero irreducible unital -representation. Assume every nonzero irreducible unital -representation of is unitarily equivalent to . Then is finite dimensional over .

Assumptions

The uniqueness-of-class condition is essential to the argument; mere irreducibility is not asserted to force finite dimension. Separability is assumed for , not for .

Conclusion

The representation space has a finite complex basis.

Proof route

Obtain faithfulness and simplicity, find a nonzero compact image, and use the resulting nonzero closed ideal to make the identity compact.

Proof steps

  1. Apply Faithfulness of a unital singleton representation to the given nonzero ordered unital and singleton to obtain injectivity. Then Simplicity from a faithful singleton model applies with that injectivity and shows that every closed two-sided ideal of is or .

  2. Use A scalar-corner projection in the unital algebra with this singleton representation on separable to obtain a nonzero projection with for every . Injectivity gives . Irreducibility, this nonzero image, and the scalar-corner equations are precisely the inputs of A nonzero represented scalar corner is compact, whose output is compactness of .

  3. Let , the two-sided ideal of The compact-preimage ideal. It is norm closed by Closedness of the compact-preimage ideal. Since and , ; simplicity therefore forces . In particular .

  4. By the definition of , is compact. Unitality now matters:

    The Compact-identity criterion applied to the same H gives , as used in the final source step.

Main citations

Lean source signature (exact)

theorem finiteDimensional_space_of_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    FiniteDimensional ℂ H
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 complex Hilbert space is separable.
(pi : Representation A H) The unital representation , so .
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) is nonzero irreducible and is unitarily equivalent to every nonzero irreducible unital comparison representation.
FiniteDimensional ℂ H The whole space has finite dimension over the complex numbers, not just some invariant subspace.

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.Representation.finiteDimensional_space_of_singleton

Accepted content SHA-256: a4f79a7fa90ac053be76ab39d9bd079b721167a74f9b9d274ffaa13cc80310d8

Accepted source guide SHA-256: 5a6b7d3c8b56391e3b141b5fc8d4ccb21b4f0ac304ac0a26efb3996846deac4a

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑