MATHLIBANNEX / CANONICAL DECLARATION CARD

A faithful singleton model forces simplicity

MathlibAnnex.Analysis.CStarAlgebra.Representation.isSimpleCStarAlgebra_of_singleton_of_injective

theorem

Uses irreducible representations annihilating proper ideals to rule out nonzero proper closed ideals.

Statement

Let be a nonzero unital complex -algebra, and let be a complex Hilbert space. Let be a unital -representation. Assume that is injective and is a singleton irreducible model among unital representations. Then every norm-closed two-sided ideal of is either or .

Assumptions

The singleton condition includes irreducibility on a nonzero space and unitary equivalence with every nonzero irreducible unital representation in the class of all complex Hilbert-space representations quantified in the definition. Injectivity is an explicit, separate hypothesis here. Neither nor is assumed separable.

Conclusion

is simple in the sense of nontriviality and absence of nonzero proper norm-closed two-sided ideals.

Proof route

An irreducible GNS representation kills a proper closed ideal. Transfer its zero action back through the singleton unitary, then use faithfulness.

Proof steps

  1. Fix a closed two-sided ideal . If there is nothing to prove. Otherwise apply A pure GNS representation annihilating a proper closed ideal with this proper closed in the nonzero ordered unital algebra . It supplies a pure state and an irreducible GNS representation with for every . Its cyclic vector has norm one, so .

  2. The singleton assumption, applied to this very , gives a unitary such that

    If , the right side is zero. Injectivity of therefore gives for every , hence .

  3. Injectivity of and yield . Thus and . Together with the first case and the given , this is precisely the definition of simplicity.

Main citations

Lean source signature (exact)

theorem isSimpleCStarAlgebra_of_singleton_of_injective [Nontrivial A]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (hinj : Function.Injective pi) : IsSimpleCStarAlgebra 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.
pi : Representation A H The unital complex -representation on the complete Hilbert space ; the surrounding context also equips with the usual -algebra order.
hsingle : IsSingletonIrreducibleModel.{u, v, u} pi is irreducible on a nonzero , and every nonzero irreducible unital comparison representation is unitarily equivalent to it.
hinj : Function.Injective pi Equality of represented operators implies . This is a hypothesis of this theorem.
IsSimpleCStarAlgebra A , and for every norm-closed two-sided ideal of , either or .

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

Accepted content SHA-256: e40928fbcaf3b7f3ec23b5b63075ea7f4c9b9461c6cd1d0eb790a1bfbcfb8a98

Accepted source guide SHA-256: fa04ed368351cc59db031cf97a4a13442abce3ac07a164e07970853e2efd5cf0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑