MATHLIBANNEX / CANONICAL DECLARATION CARD

Faithfulness from a unique irreducible class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton

theorem

Uses a pure state on the unitization to detect any hypothetical nonzero element of the kernel.

Statement

Let be a nonzero complex -algebra, with no unit assumed, and let represent the unique unitary-equivalence class of nonzero irreducible -representations of . Then is injective:

Assumptions

No separability of or is required. Faithfulness of the representation of the unitization is neither assumed nor concluded.

Conclusion

The original representation of has zero kernel.

Proof route

A nonzero kernel element would be detected in a pure GNS representation of the unitization. Its nonzero irreducible restriction is compared with the given representation, forcing that detected operator to be zero.

Proof steps

  1. If , put , so . Suppose and let be the canonical injective inclusion into the complex unitization. Then . Apply Pure-state detection of a nonzero square in the nonzero unital ordered -algebra to this element. It gives a pure state with .

  2. Let be its GNS representation with . By Irreducibility of the GNS representation of a pure state, purity makes irreducible. Restrict it to by . The GNS identity gives

    so and the restriction is a nonzero representation.

  3. A closed subspace reducing also reduces all , and conversely. Thus irreducibility of , together with the nonzero restriction established in Step 2, gives nonzero irreducibility of . This is the restriction criterion applied in the exact proof.

  4. The singleton condition applied to this supplies a unitary with . Since is surjective, every equals for some , and

    Hence , contradicting Step 2. Therefore and .

Main citations

Lean source signature (exact)

theorem injective_of_singleton [Nontrivial A]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    Function.Injective 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.
(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 For all , equality of operators forces . No separability binder occurs.

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

Accepted content SHA-256: 726046b9971256077466b6abf602fbead45b711fab5f18643e07f1dc30fc8426

Accepted source guide SHA-256: 1ba4b9c85e4b62339a1564e27eddd8c98de64f97996aa740c4d07d3f91d20ce5

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑