MATHLIBANNEX / CANONICAL DECLARATION CARD

A singleton model is faithful and exactly compact-valued

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.faithful_and_compactOperatorModel_of_singleton

theorem

Combines faithfulness with both inclusions needed to identify the represented range.

Statement

Let be a nonzero complex -algebra, with no unit assumed, and let represent the unique unitary-equivalence class of nonzero irreducible -representations on a separable complex Hilbert space . Then Equivalently, is a faithful -representation and implements a -isomorphism .

Assumptions

There is no assumption that is separable, simple, or already faithfully represented. The singleton condition quantifies over nonzero irreducible comparison representations, without restricting them to separable spaces.

Conclusion

is injective and satisfies the compact-operator model predicate: every is compact and each compact operator has a preimage in .

Proof route

Apply the three established results to the same singleton representation and assemble their outputs.

Proof steps

  1. Apply Faithfulness of a singleton representation to and the given singleton . Nontriviality and the usual -algebra order are among the present assumptions; no separability is needed in that step. Its output is injectivity of this .

  2. Apply Every represented operator is compact to the same . Its additional hypothesis is precisely the assumed separability of . For every it gives compactness of , hence .

  3. For any compact , apply Every compact operator has a preimage using these same assumptions and that particular . The result is with , hence . Substituting all three outputs into The three clauses of a compact-operator model proves the model property, alongside the explicitly stated injectivity.

Main citations

Lean source signature (exact)

theorem faithful_and_compactOperatorModel_of_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    Function.Injective pi ∧ IsCompactOperatorModel 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.
[TopologicalSpace.SeparableSpace H] The Hilbert representation space is separable; need not be.
(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.
Function.Injective pi Faithfulness of that same .
∧ IsCompactOperatorModel pi In addition, the same map is injective, sends every algebra element to a compact operator, and represents every compact operator on .

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

Accepted content SHA-256: eed3881f6dc85cb263d42bfa06504b8c4dc4fba1eb04fb1915765d936bdec28a

Accepted source guide SHA-256: c45f6044a98837da67009d9746af5e60edc6faaa8db76c0dd652cb843d317d2f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑