Components of coefficient kernels encode unitary equivalence

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.related_matrixCoefficientKernel_iff_unitaryEquivalent

theorem

Characterizes equality of coefficient-kernel components by unitary equivalence of representations.

Statement

Let be a complex C*-algebra and let and be nonzero irreducible -representations on complete complex Hilbert spaces. No identity in is required. Put

f^\pi_{x,y}:A\longrightarrow\mathbb C,\qquad f^\pi_{x,y}(a)=\langle y,\pi(a)(x)\rangle \quad(x,y\ne0),

and define in the same way. The inner products are linear in the second slot. The geometric structure space consists, by the extreme-kernel identification, of kernels of bounded complex-linear functionals that are extreme points, for real convexity, of the entire closed dual unit ball . Its closure is

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

Write when or , and write for the equivalence relation generated by these links. For nonzero and ,

\ker f^\pi_{x,y}\sim \ker f^\sigma_{z,w} \quad\Longleftrightarrow\quad \pi\simeq_u\sigma.

Here means that and are unitarily equivalent, that is, there is one surjective complex-linear isometry satisfying for every .

Assumptions

The source carries the compatible C*-order on . The Hilbert spaces may have different dimensions, and neither representation is assumed faithful. Each of the four vectors is required to be nonzero. The relation on the left is the pre-existing geometric finite-chain relation, not a relation defined by representation equivalence.

Conclusion

The assertion concerns the full finite-chain relation and one simultaneous intertwiner of the two original representations. Neither direction replaces that relation by direct linking of every pair in a component. Faithfulness is not a conclusion.

Main citations

Exact equivalence and its finite-chain converse: related_matrixCoefficientKernel_iff_unitaryEquivalent.
Ryotaro Tanaka, arXiv:2504.05551v1, Theorem 5.8. This declaration states the result directly for arbitrary irreducible representations and nonzero coefficient vectors.

Lean source signature (exact)

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

theorem related_matrixCoefficientKernel_iff_unitaryEquivalent
    (pi : NonUnitalCStarRepresentation A H) (sigma : NonUnitalCStarRepresentation A K)
    (hpi : pi.IsIrreducible) (hsigma : sigma.IsIrreducible)
    (x y : H) (z w : K) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hw : w ≠ 0) :
    (NormedSpace.geometricStructureClosure ℂ A).Related
      (matrixCoefficientKernel pi hpi x y hx hy) (matrixCoefficientKernel sigma hsigma z w hz hw) ↔
        pi.UnitaryEquivalent sigma

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 is the domain of both representations.
Hilbert spaces`variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]`Fixed source	The complex Hilbert spaces are complete. Their universe levels may differ.
Representations and irreducibility`(pi : NonUnitalCStarRepresentation A H) (sigma : NonUnitalCStarRepresentation A K) (hpi : pi.IsIrreducible) (hsigma : sigma.IsIrreducible)`Fixed source	The representations and are nonzero and irreducible. Faithfulness is not assumed.
Coefficient vectors`(x y : H) (z w : K) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hw : w ≠ 0) :`Fixed source	The four vectors satisfy and . They are not required to have unit norm.
Finite-chain relation of the two kernels`(NormedSpace.geometricStructureClosure ℂ A).Related (matrixCoefficientKernel pi hpi x y hx hy) (matrixCoefficientKernel sigma hsigma z w hz hw) ↔`Fixed source	The ambient closure is on . The complete two arguments are the coefficient-kernel points of the displayed representations and vectors. The left side of the equivalence is $\ker f^\pi_{x,y}\sim\ker f^\sigma_{z,w}.$ This is finite-chain relatedness, including equality, rather than direct linking alone.
Unitary equivalence`pi.UnitaryEquivalent sigma :=`Fixed source	The right side says that there is one surjective complex-linear isometry with $U\pi(a)=\sigma(a)U\qquad(a\in A).$ The equivalence joins this single simultaneous intertwiner condition to the preceding finite-chain relation.

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

Exact surrounding source:

variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]

Back to the reading-guide item

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

Technical documentation