Scalar corner from a representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner

theorem

Produces a nonzero projection with one-dimensional corner from a separably acting representative of the unique irreducible-representation class.

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 is a nonzero star projection p in A whose every corner p a p is a complex scalar multiple of p.

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 is a nonzero star projection p in A whose every corner p a p is a complex scalar multiple of p.

Proof route

The source takes a nonzero a, inserts b=a* a into a maximal abelian subalgebra of the unitization, uses separability to count its characters, and obtains an isolated character distinct from the scalar character. A projection supported at that character has a scalar corner; the zero scalar coordinate forces that projection back into A.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton

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

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_isolated_character_ne_infinity

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

• MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint

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

Lean source signature (exact)

theorem exists_nonzero_projection_scalar_corner [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧
      ∀ a : A, ∃ c : ℂ, p * a * p = c • p

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