Preimages for all operators of the form rankOne

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_rankOne_of_singleton

theorem

Provides preimages for every operator of the form rankOne ℂ x y, the rank-at-most-one generators used to obtain all compact operators.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a separable complex Hilbert space; and let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. For every pair x,y∈H, including zero vectors, there exists a∈A with π(a)=rankOne ℂ x y; this operator has rank at most one.

Assumptions

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a separable complex Hilbert space; and let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A.

Conclusion

For every pair x,y∈H, including zero vectors, there exists a∈A with π(a)=rankOne ℂ x y; this operator has rank at most one.

Proof route

The source obtains one nonzero rank-one projection in π(A), uses the unique-class hypothesis for π together with injectivity, and invokes the rank-one-preimage theorem to move from that projection to every x and y, including zero vectors.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_rankOne_map

  Exact formal dependency; inspect the linked Card and exact source.

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

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON