Nonunital irreducibility

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible

def

Defines nonunital irreducibility as nonzero action with no nontrivial closed reducing subspaces.

Statement

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and π a representation of A on H. The predicate says that π acts nontrivially and every closed complex submodule L invariant under both π(a) and its adjoint for every a is either {0} or H.

Definition

IsIrreducible π ↔ (∃ a : A, π a ≠ 0) ∧ ∀ L, Reduces π L → L = ⊥ ∨ L = ⊤.

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 predicate says that π acts nontrivially and every closed complex submodule L invariant under both π(a) and its adjoint for every a is either {0} or H.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation

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

Lean source signature (exact)

def IsIrreducible (pi : NonUnitalCStarRepresentation A H) : Prop

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