Version 1 source-bound exposition export. Original text SHA-256: 964b5ca961e42940c244e402d89766a54b832c8a601d109d14e086705f0943b4. Link targets are adapted for this edition; the registered Card identity is unchanged.

# The intersection of a pure-state component is its GNS representation kernel

## Statement

Let $A\ne\{0\}$ be a complex C*-algebra, possibly without an identity. A state on $A$ is a positive bounded complex-linear functional of norm one. It is pure if it is an extreme point of the state space, regarded as a real convex set. Let $\varphi$ be a pure state. Let $(H_\varphi,\widetilde\pi_\varphi,\xi_\varphi)$ be the GNS model of its canonical state extension $\widetilde\varphi(\lambda,a)=\lambda+\varphi(a)$ to the forced unitization $\mathbb C\oplus A$, and let $\pi_\varphi=\widetilde\pi_\varphi|_A$.

By [the extreme-kernel theorem](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ExtremeKernel.lean.html?from=21&start=49&end=65#L49), $S(A)$ is the family 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^*}$, with closure $c_A(\mathcal T)=\{I\in S(A):\bigcap_{J\in\mathcal T}J\subseteq I\}$. The pure-state kernel $\ker\varphi$ is one such point, by the [pure-state extremality theorem](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/FacialStructure/PureStateExtreme.lean.html?from=21&start=29&end=76#L29). Let $C(\ker\varphi)$ denote its component for the finite-chain relation generated by equal points and nonclosed pairs. Write $\mathrm{GS}(A)$ for the set of these components. For a component $C$, put $J_C=\bigcap_{I\in C}I$, and write $\mathrm{PS}(A)$ for the family of all such intersections. The canonical map is

$$
\gamma:\mathrm{GS}(A)\longrightarrow\mathrm{PS}(A),\qquad \gamma(C)=J_C.
$$

Then, as subsets of the original algebra,

$$
\gamma(C(\ker\varphi))=J_{C(\ker\varphi)}=\ker\pi_\varphi.
\tag{1}
$$

On the left we display the underlying subset of the primitive geometric point.

## Assumptions

The given functional $\varphi\in A^*$ is positive, has norm one, and is extreme in the state space for real convexity; $A$ carries its compatible C*-order. The GNS action is formed from this very state's canonical extension. The representation is fixed by $\varphi$; faithfulness is not assumed.

## Conclusion

The whole component's intersection is the representation kernel $\ker\pi_\varphi$, using this fixed GNS representation. An individual functional kernel $\ker\varphi$ need not equal that intersection. Formula (1) is an equality of subsets; it gives neither injectivity of $\gamma$ nor a comparison of topologies by itself.

## Main citations

- [Exact pure-state gamma identity](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/AbsoluteState.lean.html?from=21&start=281&end=294#L281): `geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val`.
- [Component intersections](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/Normed/GeometricStructure/Spectrum.lean.html?from=21&start=44&end=45#L44), [their family](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/Normed/GeometricStructure/Spectrum.lean.html?from=21&start=48&end=50#L48) and [the component-intersection map](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/Normed/GeometricStructure/Spectrum.lean.html?from=21&start=68&end=72#L68): the definitions of $J_C$, $\mathrm{PS}(A)$ and $\gamma$.
- Ryotaro Tanaka, [arXiv:2504.05551v1, Lemma 5.10](https://arxiv.org/abs/2504.05551v1): the component-family and representation-kernel comparison.

## Lean source signature (exact)

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

```lean
theorem geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val
    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :
    (NormedSpace.geometricSpectrumToPrimitive ℂ A
      (NormedSpace.toGeometricSpectrum ℂ A
        (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩))).val =
      ((absoluteStateContinuousMap (NonUnitalStateGNS.representation phi hpure.1)).ker : Set A)
```

| In the source | Mathematical meaning |
|---|---|
| [Algebra and order](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-0)<br>`variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]`<br>`variable [PartialOrder A] [StarOrderedRing A]` | The nonzero complex C*-algebra $A$ and its compatible order are fixed. |
| [Given pure state](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-1)<br>`    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :` | The given $\varphi$ is a positive bounded complex-linear functional of norm one, extreme in the state space for real convexity. This same state determines the GNS model. |
| [Kernel, component and its intersection](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-2)<br>`    (NormedSpace.geometricSpectrumToPrimitive ℂ A`<br>`      (NormedSpace.toGeometricSpectrum ℂ A`<br>`        (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩))).val =` | The innermost input is the geometric point $\ker\varphi$, with its extremality certificate. Sending it to its component gives $C(\ker\varphi)\in\mathrm{GS}(A)$. Applying $\gamma$ and taking the underlying subset gives $$\gamma(C(\ker\varphi))=J_{C(\ker\varphi)}\subseteq A.$$ The nested applications act on this same point in that order. |
| [The component map](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-3)<br>`def toGeometricSpectrum (I : GeometricStructureSpace 𝕜 E) : GeometricSpectrum 𝕜 E :=`<br>`  (geometricStructureClosure 𝕜 E).toComponentPoint I` | This map sends a point $I\in S(A)$ to its entire finite-chain component. In the preceding application, $I=\ker\varphi$. |
| [The intersection map](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-4)<br>`def geometricSpectrumToPrimitive : GeometricSpectrum 𝕜 E → PrimitiveGeometricSpectrum 𝕜 E :=`<br>`  ClosureSpace.HullKernel.componentPointToComponentKernelPoint`<br>`    (geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕜 E)` | This is $\gamma:\mathrm{GS}(A)\to\mathrm{PS}(A)$, sending a component $C$ to $J_C=\bigcap_{I\in C}I$. Its value is a subset of the algebra, rather than a subset of $S(A)$. |
| [Kernel of the same GNS representation](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-5)<br>`      ((absoluteStateContinuousMap (NonUnitalStateGNS.representation phi hpure.1)).ker : Set A) := by` | The right side is $\ker\pi_\varphi\subseteq A$. The GNS action is formed from the canonical extension of this same state, and the continuous-linear-map wrapper changes no values. Thus (1) identifies the whole component intersection with the representation kernel, not with the individual functional kernel. |
| [Operator-valued linear map](https://exactmathematics.org/mathlibannex/cards/407f570c29b53ad2e9ffa1b46613c142a0e8c631c2aca03ec172505aade4b777/versions/gss-r1-6167c2d975ac02b4/index.html#card-21--source-row-6)<br>`private def absoluteStateContinuousMap {H : Type v}`<br>`    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]`<br>`    (pi : NonUnitalCStarRepresentation A H) : A →L[ℂ] (H →L[ℂ] H) :=`<br>`  LinearMap.mkContinuous`<br>`    { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }` | The wrapper has domain $A$ and codomain $\mathcal B(H_\varphi)$. Its function is the given representation $\pi_\varphi$, with the same addition and complex-scalar action. It supplies the operator-valued map whose kernel appears on the right of (1). |

### 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]
```

The continuous-map wrapper in the same source is copied separately; its forward function is the given action; the continuous-map constructor receives the existing contractive bound:

```lean
private def absoluteStateContinuousMap {H : Type v}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (pi : NonUnitalCStarRepresentation A H) : A →L[ℂ] (H →L[ℂ] H) :=
  LinearMap.mkContinuous
    { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }
    1 (fun a => by
      change ‖pi a‖ ≤ 1 * ‖a‖
      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi a)
```