Representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel

def

Defines when a nonzero irreducible representation π is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A.

Statement

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and π a representation of A on H. The representation π is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A: π is nonzero and irreducible, and every nonzero irreducible representation of A on any complex Hilbert space is unitarily equivalent to π. The definition does not assume faithfulness or separability of A or H.

Definition

IsSingletonIrreducibleModel π ↔ IsIrreducible π ∧ ∀ K ρ, IsIrreducible ρ → UnitaryEquivalent π ρ.

Assumptions

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and π a representation of A on H.

Conclusion

The representation π is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A: π is nonzero and irreducible, and every nonzero irreducible representation of A on any complex Hilbert space is unitarily equivalent to π. The definition does not assume faithfulness or separability of A or H.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible

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

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent

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

Lean source signature (exact)

def IsSingletonIrreducibleModel
    (pi : NonUnitalCStarRepresentation A H) : Prop

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