MATHLIBANNEX / CANONICAL DECLARATION CARD

An infinite-dimensional unital algebra has no separable singleton model

MathlibAnnex.Analysis.CStarAlgebra.Representation.not_singleton_amongNonUnital_of_infiniteDimensional

theorem

Uses the finite-dimensional algebra conclusion to contradict the proposed singleton condition.

Statement

Let be an infinite-dimensional nonzero unital complex -algebra, let be a separable complex Hilbert space, and let be a unital -representation. Then cannot satisfy the singleton condition of R11.

Assumptions

Infinite dimensionality is a hypothesis on . The conclusion excludes the conjunction of nonzero irreducibility and unitary equivalence with every nonzero irreducible -representation of .

Conclusion

The specified cannot represent a unique irreducible class. This does not rule out separable irreducible representations in general or construct a particular competing representation.

Proof route

Assume the singleton condition and apply the preceding theorem for the dimension of the algebra.

Proof steps
  1. If this satisfied the proposed condition, then Finite dimension of the algebra from an unrestricted singleton model would apply: is nonzero and unital, is separable, and the assumed condition supplies its remaining input. It would give , contrary to the stated infinite dimensionality. Therefore that condition cannot hold.

Main citations

Lean source signature (exact)

theorem not_singleton_amongNonUnital_of_infiniteDimensional
    [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A)
    [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H) :
    ¬ IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi
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.
(hA : ¬ FiniteDimensional ℂ A) is not finite dimensional as a complex vector space.
[TopologicalSpace.SeparableSpace H] The chosen Hilbert space is separable.
(pi : Representation A H) The specified unital -representation .
¬ 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.

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.not_singleton_amongNonUnital_of_infiniteDimensional

Accepted content SHA-256: ad46eedc9d849a091ae1c205d9dc8bc7c7b9b7ae0b2e16f87b70500f544777fd

Accepted source guide SHA-256: bceb9d4a4d4382a64f449b77417ad81888162ae4179842d387732732c9460f69

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑