MATHLIBANNEX / CANONICAL DECLARATION CARD

Every rank-one operator has an algebra preimage

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_rankOne_of_singleton

theorem

Turns one represented rank-one projection into every rank-one operator using dense orbits and a closed range.

Statement

Let be a nonzero complex -algebra, with no unit assumed, let be a separable complex Hilbert space, and let represent the unique unitary-equivalence class of nonzero irreducible -representations. For every there is such that

Assumptions

The vectors are arbitrary, including zero. They need not be unit vectors. The separability assumption concerns . No unit is required in .

Conclusion

Each rank-one operator belongs to the image of the original algebra, not merely to the image of its unitization.

Proof route

Find one rank-one projection in the range. Use irreducibility to obtain a dense original-algebra orbit, multiply around the projection, and pass to limits in both vectors.

Proof steps

  1. Apply A rank-one projection in a singleton model to the nonzero ordered , separable , and singleton . It supplies and a unit vector with . In particular . The theorem Faithfulness of a non-unital singleton model also gives injectivity of .

  2. The dense-orbit step in One rank-one projection generates all rank-one operators in the range uses irreducibility of the unitized representation. Its orbit of is dense; every unitization element has the form and acts by

    Thus already is dense in . This calculation is why the preimages below stay in .

  3. For and , multiplicativity and adjoints give

    Hence .

  4. Because is injective, it is isometric and has norm-closed range. Approximate arbitrary by vectors in the dense orbit. The estimates and

    show convergence of the corresponding rank-one operators. Closedness then puts in , which is the asserted existence of .

Main citations

Lean source signature (exact)

theorem exists_preimage_rankOne_of_singleton [Nontrivial A]
    [PartialOrder A] [StarOrderedRing A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    ∀ x y : H, ∃ a : A, pi a = InnerProductSpace.rankOne ℂ x y
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.
[PartialOrder A] [StarOrderedRing A] These typeclasses provide the usual order on a -algebra, equivalently when is positive. They are used by the state and positivity arguments.
[TopologicalSpace.SeparableSpace H] is a separable complex Hilbert space.
pi : NonUnitalCStarRepresentation A H The specified -representation ; its interface does not require a unit equation.
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.
∀ x y : H, ∃ a : A After any two vectors are chosen, an element may be chosen depending on both.
InnerProductSpace.rankOne ℂ x y The entire operator , with this order of .
pi a = InnerProductSpace.rankOne ℂ x y The chosen represents that operator on every vector .

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

Accepted content SHA-256: 68cc3dfce4a57d34a5ceddc31a6338a17696144595fd2bc2de1a79430aa4b053

Accepted source guide SHA-256: d3fbce5ad9638ab3a7f018d8d1539b09ef22f0656404058591811d5e8be72f62

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑