MATHLIBANNEX / CANONICAL DECLARATION CARD

Finite-dimensional algebra in the unital singleton case

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_algebra_of_singleton_amongNonUnital

theorem

Distinguishes finite dimension of the representation space from finite dimension of the algebra embedded in its operators.

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

Finite dimensionality of or is not an initial hypothesis. Neither faithfulness nor separability of is assumed.

Conclusion

The vector space itself has a finite complex basis.

Proof route

First obtain finite dimensionality of . The compact-operator conclusion gives injectivity of , so embeds linearly into the finite-dimensional space .

Proof steps

  1. Apply The all-representations singleton condition implies the unital singleton condition to the given condition. For a unital nonzero irreducible -representation , use the same operator map through the interface that does not require a unit equation. It is still nonzero irreducible, so the hypothesis supplies the required unitary equivalence. Thus the same satisfies the unital singleton condition.

  2. Apply Finite dimension of the unital singleton representation space with this singleton , nonzero ordered unital and separable to obtain a finite basis of . Hence the space of bounded complex-linear operators is finite dimensional: if , its dimension is .

  3. The theorem Faithfulness of a unital singleton model gives injectivity of the same complex-linear . Thus

    An injective linear map into a finite-dimensional space forces its domain to be finite dimensional. This is the final step of Finite dimension of the faithfully represented algebra, which the exact theorem applies after Step 1.

Main citations

Lean source signature (exact)

theorem finiteDimensional_algebra_of_singleton_amongNonUnital
    [Nontrivial A] [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) :
    FiniteDimensional ℂ A
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 ℂ A The conclusion is finite dimension of the algebra , as opposed to the intermediate finite dimension of .

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_algebra_of_singleton_amongNonUnital

Accepted content SHA-256: da016c6bd93367395562703b5bdc45df0e4b032f6c2469fcb03fa8b38b38b74e

Accepted source guide SHA-256: f879ee87182c1be0766c05ed4ceff535be006c5a47fab6ea5a015c2007986fb0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑