MATHLIBANNEX / CANONICAL DECLARATION CARD

A representative of the unique irreducible class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel

def

Defines when one nonzero irreducible -representation represents the sole unitary-equivalence class of such representations.

Statement

Let be a complex -algebra, with no unit assumed, and let be a -representation. The predicate below says that is nonzero irreducible and that every other nonzero irreducible -representation of is unitarily equivalent to .

Definition

Require first that act nontrivially and have no proper nonzero closed reducing subspace. Then, for every complex Hilbert space and every nonzero irreducible -representation , require a unitary operator such that

Assumptions

No separability or faithfulness condition is part of this definition. The algebra may be unital, but the definition does not require a unit or a unit-preservation equation.

Conclusion

The output is a property of the specified : it represents the unique unitary-equivalence class of nonzero irreducible -representations of .

Faithfulness is not part of this definition. Later theorems impose hypotheses to deduce it. “Non-unital” permits an algebra with a unit; it does not assert that a unit fails to exist.

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.

/-- A displayed nonzero irreducible representation representing every
nonzero irreducible representation of a genuinely nonunital C-star algebra.
Faithfulness is deliberately not part of this predicate. -/
def IsSingletonIrreducibleModel
    (pi : NonUnitalCStarRepresentation A H) : Prop :=
  pi.IsIrreducible ∧
    ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
      [CompleteSpace K] (rho : NonUnitalCStarRepresentation A K),
      rho.IsIrreducible → pi.UnitaryEquivalent rho
In the source Mathematical meaning
(pi : NonUnitalCStarRepresentation A H) The chosen representation , without a unit-preservation requirement.
: Prop The output is a condition on this .
pi.IsIrreducible ∧ First require that some acts by a nonzero operator and that the only closed reducing subspaces are ; the comparison condition must hold as well.
∀ (K : Type w) For every comparison space in its own size universe.
[NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] For every complete complex Hilbert-space structure on ; separability is not added.
(rho : NonUnitalCStarRepresentation A K) For each representation of the same on that .
rho.IsIrreducible → pi.UnitaryEquivalent rho If is nonzero irreducible, there is a unitary intertwining every and as in the displayed equation.

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel

Accepted content SHA-256: 081be484bba44478a0ab817625d1047efc169cd8ebd56028441216aeda834972

Accepted source guide SHA-256: c1e093326531c3965b07bfd304478df48dcc642d68fa7f7259a986d78fa4eadb

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑