MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible
def
Requires nonzero action as well as the absence of proper closed reducing subspaces.
Statement
Let be a complex -algebra, with no unit assumed, a complex Hilbert space, and a -representation. The following predicate defines nonzero irreducibility.
Definition
The first condition is The second says: for every complex linear subspace which is closed and satisfies one has or . These are the definitions of nonzero action and reduction in Nonzero action and closed reducing subspaces. Because and is closed under adjoints, invariance under every also gives the stated adjoint invariance; the source records both explicitly.
Assumptions
No separability or injectivity is assumed. The nonzero requirement is a property of the action , not merely of its underlying Hilbert space.
Conclusion
The zero representation is excluded, and every closed reducing complex subspace is either or .
Main citations
Lean source signature (exact)
The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.
def IsIrreducible (pi : NonUnitalCStarRepresentation A H) : Prop :=
pi.IsNonzero ∧ ∀ L : Submodule ℂ H, pi.Reduces L → L = ⊥ ∨ L = ⊤| In the source | Mathematical meaning |
|---|---|
(pi : NonUnitalCStarRepresentation A H) |
The given action of by bounded operators on . |
: Prop |
The output is a condition on that action. |
pi.IsNonzero |
Some has as an operator. The condition alone would not suffice. |
∀ L : Submodule ℂ H |
For every complex linear subspace of . |
pi.Reduces L |
is norm closed and, for all and , both and belong to . |
L = ⊥ ∨ L = ⊤ |
That same reducing subspace must be the zero subspace or all of . |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible
Accepted content SHA-256: aa751ea4410d8355c45121a59a85d0ab17c226cd1e7f3cd8c34029d23bd0d1c3
Accepted source guide SHA-256: cf556951fbe8a29a172dc5d8b4612d1ae29b0418a509394655d6ff179929d52c
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73