MATHLIBANNEX / CANONICAL DECLARATION CARD

Finite-dimensional representation space in the unital singleton case

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton_amongNonUnital

theorem

Applies the unital finite-dimensional-space theorem after checking the representation-interface conversion.

Statement

Let be a nonzero unital complex -algebra, let be a separable complex Hilbert space, and let satisfy the singleton condition of R11. Then is finite dimensional over .

Assumptions

The universal condition quantifies over every nonzero irreducible -representation of ; representations presented without a unit equation are unital by irreducibility, as explained in R11.

Conclusion

The same representation space has a finite complex basis.

Proof route

Convert the comparison condition for the same representation and apply the finite-dimensional-space theorem.

Proof steps

  1. Apply The all-representations singleton condition implies the unital singleton condition to . For a unital nonzero irreducible -representation , write for the same operator map viewed through the interface that does not require a unit equation. The assumed condition then supplies a unitary with for every . Hence satisfies the unital singleton condition.

  2. Apply Finite dimension of the unital singleton representation space to the same nonzero ordered unital , same separable , and same with that converted condition. Its conclusion is . In that theorem the closed compact-preimage ideal becomes all of , so is compact and the compact-identity criterion supplies the finite dimension.

Main citations

Lean source signature (exact)

theorem finiteDimensional_space_of_singleton_amongNonUnital
    [Nontrivial A] [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{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 complete complex Hilbert representation space is separable.
(pi : Representation A H) The specified unital -representation .
(hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) The specified representation is nonzero irreducible, and every nonzero irreducible -representation of the same algebra is unitarily equivalent to it.
FiniteDimensional ℂ H The conclusion concerns the whole original Hilbert space . The declaration does not replace it by a different representation space.

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_amongNonUnital

Accepted content SHA-256: e5822068e7563379ffb66299e3be1de3b253ff8679aa712e6a9543e1bef46c8e

Accepted source guide SHA-256: 3cf2c2af0bd2a1b454b241fe8ae488ad19531d4a53d63e71b4f5be6115f79a82

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑