A representation component is the full coefficient-kernel family

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.component_matrixCoefficientKernel_eq_family

theorem

Describes each irreducible representation component by all of its nonzero vector coefficients.

Statement

Let be a complex C*-algebra, with no identity required, and let be a nonzero irreducible -representation on a complete complex Hilbert space. The inner product is conjugate-linear in its first argument. For nonzero , put

f^\pi_{p,q}(a)=\langle q,\pi(a)(p)\rangle, \qquad \mathcal F_\pi=\{\ker f^\pi_{p,q}:p,q\ne0\}.

Write for the geometric structure space of . In this C*-algebra setting its points are precisely , where is extreme, for real convexity, in the closed unit ball of the Banach dual; the extreme-kernel identification guarantees this description from the original face definition. For , its closure is

c_A(\mathcal T)=\left\{I\in S(A):\bigcap_{J\in\mathcal T}J\subseteq I\right\}.

Two points are linked if they are equal or their pair is not closed. Let be the equivalence class of under finite chains of linked points. Then, for every nonzero ,

C(\ker f^\pi_{x,y})=\mathcal F_\pi.

Assumptions

The source uses the compatible C*-order on . Irreducibility includes nonzero action and excludes proper nonzero closed reducing subspaces. No faithfulness, finite dimension or separability is required. Under this irreducibility hypothesis, is a point of for every . The component is defined by the closure relation above, without assuming that is a topological closure.

Conclusion

Every point of the entire component, including one initially presented without reference to , is a coefficient kernel of this fixed representation. Conversely, every pair of nonzero coefficient vectors gives a point of the component. Thus the choice of the initial pair has no effect on this component. This is an equality of subsets of ; it does not identify an individual coefficient kernel with .

Main citations

Exact whole-component theorem: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.component_matrixCoefficientKernel_eq_family.
Component–representation correspondence: the equivalence between finite-chain components and unitary equivalence.
The coefficient-kernel family and its same-component inclusion: matrixCoefficientKernelFamily and matrixCoefficientKernelFamily_subset_component.
Ryotaro Tanaka, arXiv:2504.05551v1, Lemma 5.10. The present declaration gives the component formula for an arbitrary irreducible representation; the pure-state specialization and the intersection calculation have separate explanations.

Lean source signature (exact)

The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.

theorem component_matrixCoefficientKernel_eq_family
    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)
    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :
    (NormedSpace.geometricStructureClosure ℂ A).component
      (matrixCoefficientKernel pi hpi x y hx hy) = matrixCoefficientKernelFamily pi hpi

Back to the reading-guide item

In the source	Mathematical meaning
Algebra and order`variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A] variable [PartialOrder A] [StarOrderedRing A]`Fixed source	The nonzero complex C*-algebra with its compatible order; no identity is required.
Representation space`variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]`Fixed source	The complex Hilbert space is complete.
One irreducible representation`(pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)`Fixed source	The same fixed nonzero irreducible representation supplies all coefficient kernels. It need not be faithful.
Starting vectors`(x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :`Fixed source	The starting pair is , without a normalization assumption.
Component and full family`(NormedSpace.geometricStructureClosure ℂ A).component (matrixCoefficientKernel pi hpi x y hx hy) = matrixCoefficientKernelFamily pi hpi := by`Fixed source	The component is taken in the ambient closure , starting at . The complete equality is $C(\ker f^\pi_{x,y})=\mathcal F_\pi.$ It concerns all points of that component, not just kernels chosen in advance.
The coefficient-kernel family`def matrixCoefficientKernelFamily (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) : Set (NormedSpace.GeometricStructureSpace ℂ A) := {I \| ∃ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), matrixCoefficientKernel pi hpi x y hx hy = I}`Fixed source	A point belongs to exactly when there are with . The vectors may depend on ; the representation is the same throughout.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]

Back to the reading-guide item

Exact surrounding source:

variable [PartialOrder A] [StarOrderedRing A]

Back to the reading-guide item

Exact surrounding source:

variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

Back to the reading-guide item

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation