A represented rank-one projection from a representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_rankOne_map

theorem

Produces a nonzero projection whose represented image is a compact rank-one orthogonal projection.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital, H a separable complex Hilbert space, and π a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. There are a nonzero star projection p∈A and a unit vector e∈H with π(p)=rankOne e e; the represented operator π(p) is compact. Minimality is not an explicit clause of this theorem type.

Assumptions

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

Conclusion

There are a nonzero star projection p∈A and a unit vector e∈H with π(p)=rankOne e e; the represented operator π(p) is compact. Minimality is not an explicit clause of this theorem type.

Proof route

The preceding scalar-corner theorem gives p. Injectivity makes π(p) nonzero, and the scalar-corner/rank-one lemma gives a unit e and the image equation. Compactness follows from compactness of a rank-one operator.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner

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

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton

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

Lean source signature (exact)

theorem exists_nonzero_projection_rankOne_map [Nontrivial A]
    [PartialOrder A] [StarOrderedRing A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧
      (∃ e : H, ‖e‖ = 1 ∧ pi p = InnerProductSpace.rankOne ℂ e e) ∧
      IsCompactOperator (pi p)

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