Version 1 source-bound exposition export. Original text SHA-256: 2003f1e785393ef4b8e1086293afd301319a515e2d470cd1236c5ac74ecfa348. Link targets are adapted for this edition; the registered Card identity is unchanged. # Components of coefficient kernels encode unitary equivalence ## Statement Let $A\ne\{0\}$ be a complex C*-algebra and let $\pi:A\to\mathcal B(H)$ and $\sigma:A\to\mathcal B(K)$ be nonzero irreducible $\ast$-representations on complete complex Hilbert spaces. No identity in $A$ 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 $f^\sigma_{z,w}$ in the same way. The inner products are linear in the second slot. The geometric structure space $S(A)$ consists, by [the extreme-kernel identification](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ExtremeKernel.lean.html?from=18&start=49&end=65#L49), of kernels $\ker\rho\subseteq A$ of bounded complex-linear functionals $\rho:A\to\mathbb C$ that are extreme points, for real convexity, of the entire closed dual unit ball $B_{A^*}$. Its closure is $$ c_A(\mathcal T)=\left\{I\in S(A):\bigcap_{J\in\mathcal T}J\subseteq I\right\}. $$ Write $I\leftrightarrow J$ when $I=J$ or $c_A(\{I,J\})\ne\{I,J\}$, and write $I\sim J$ for the equivalence relation generated by these links. For nonzero $x,y\in H$ and $z,w\in K$, $$ \ker f^\pi_{x,y}\sim \ker f^\sigma_{z,w} \quad\Longleftrightarrow\quad \pi\simeq_u\sigma. $$ Here $\pi\simeq_u\sigma$ means that $\pi$ and $\sigma$ are unitarily equivalent, that is, there is one surjective complex-linear isometry $U:H\to K$ satisfying $U\pi(a)=\sigma(a)U$ for every $a\in A$. ## Assumptions The source carries the compatible C*-order on $A$. 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](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/RepresentationComponents.lean.html?from=18&start=104&end=113#L104): `related_matrixCoefficientKernel_iff_unitaryEquivalent`. - Ryotaro Tanaka, [arXiv:2504.05551v1, Theorem 5.8](https://arxiv.org/abs/2504.05551v1). 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. ```lean 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 ``` | In the source | Mathematical meaning | |---|---| | [Algebra and order](https://exactmathematics.org/mathlibannex/cards/dc5425431b0c12bf15137e6002c16b5ba2c600bde91d02b23dd813e4369498d1/versions/gss-r1-e6b09cd26ba001ea/index.html#card-18--source-row-0)
`variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]`
`variable [PartialOrder A] [StarOrderedRing A]` | The nonzero complex C*-algebra $A$ with its compatible order is the domain of both representations. | | [Hilbert spaces](https://exactmathematics.org/mathlibannex/cards/dc5425431b0c12bf15137e6002c16b5ba2c600bde91d02b23dd813e4369498d1/versions/gss-r1-e6b09cd26ba001ea/index.html#card-18--source-row-1)
`variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]`
`variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]` | The complex Hilbert spaces $H,K$ are complete. Their universe levels may differ. | | [Representations and irreducibility](https://exactmathematics.org/mathlibannex/cards/dc5425431b0c12bf15137e6002c16b5ba2c600bde91d02b23dd813e4369498d1/versions/gss-r1-e6b09cd26ba001ea/index.html#card-18--source-row-2)
` (pi : NonUnitalCStarRepresentation A H) (sigma : NonUnitalCStarRepresentation A K)`
` (hpi : pi.IsIrreducible) (hsigma : sigma.IsIrreducible)` | The representations $\pi:A\to\mathcal B(H)$ and $\sigma:A\to\mathcal B(K)$ are nonzero and irreducible. Faithfulness is not assumed. | | [Coefficient vectors](https://exactmathematics.org/mathlibannex/cards/dc5425431b0c12bf15137e6002c16b5ba2c600bde91d02b23dd813e4369498d1/versions/gss-r1-e6b09cd26ba001ea/index.html#card-18--source-row-3)
` (x y : H) (z w : K) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hw : w ≠ 0) :` | The four vectors satisfy $x,y\in H\setminus\{0\}$ and $z,w\in K\setminus\{0\}$. They are not required to have unit norm. | | [Finite-chain relation of the two kernels](https://exactmathematics.org/mathlibannex/cards/dc5425431b0c12bf15137e6002c16b5ba2c600bde91d02b23dd813e4369498d1/versions/gss-r1-e6b09cd26ba001ea/index.html#card-18--source-row-4)
` (NormedSpace.geometricStructureClosure ℂ A).Related`
` (matrixCoefficientKernel pi hpi x y hx hy) (matrixCoefficientKernel sigma hsigma z w hz hw) ↔` | The ambient closure is $c_A$ on $S(A)$. 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](https://exactmathematics.org/mathlibannex/cards/dc5425431b0c12bf15137e6002c16b5ba2c600bde91d02b23dd813e4369498d1/versions/gss-r1-e6b09cd26ba001ea/index.html#card-18--source-row-5)
` pi.UnitaryEquivalent sigma :=` | The right side says that there is one surjective complex-linear isometry $U:H\to K$ 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. | ### Source context (separate exact excerpt) Exact surrounding source: ```lean variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A] ``` Exact surrounding source: ```lean variable [PartialOrder A] [StarOrderedRing A] ``` Exact surrounding source: ```lean variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] ``` Exact surrounding source: ```lean variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] ```