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

# The irreducible spectrum and the geometric spectrum

## Statement

Let $A\ne\{0\}$ be a complex C*-algebra, possibly without an identity. There is a specified homeomorphism

$$
\Phi_A:\widehat A\longrightarrow\mathrm{GS}(A)
$$

from its independent irreducible representation spectrum to its geometric spectrum. For a pure state $\varphi$ and its GNS representation $\pi_\varphi$, its point map is

$$
\Phi_A([\pi_\varphi])=C(\ker\varphi).
\tag{1}
$$

Here $S(A)$ consists of kernels of extreme points of the closed unit ball of the Banach dual of $A$, with convexity over $\mathbb R$. [The extreme-functional kernel characterization](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ExtremeKernel.lean.html?from=24&start=49&end=65#L49) identifies this family with the original geometric structure space, with closure $c_A(\mathcal U)=\{I:\bigcap_{J\in\mathcal U}J\subseteq I\}$. The component is taken for the finite-chain relation generated by equal points and nonclosed pairs.

## Definition

The source $\widehat A$ is the [irreducible spectrum](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Basic.lean.html?from=24&start=73&end=73#L73): pure norm-one positive bounded complex-linear functionals on $A$, modulo unitary equivalence of their GNS representations restricted to $A$. Equality of representation kernels is not the equivalence relation. Its topology is induced by the kernel map $\kappa([\pi])=\ker\pi$ into the primitive spectrum with hull-kernel topology.

The target $\mathrm{GS}(A)$ consists of components of $S(A)$. For a component $C$, put $J_C=\bigcap_{I\in C}I$. Its closure is
$$
\overline{\mathcal D}=\left\{C:\bigcap_{D\in\mathcal D}J_D\subseteq J_C\right\},
$$
with empty intersection $A$. The [geometric-spectrum topology](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=24&start=115&end=117#L115) has this closure.

The [spectral bijection](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralComparison.lean.html?from=24&start=131&end=134#L131) sends $[\pi_\varphi]$ to $C(\ker\varphi)$. Its inverse assigns the representation class of a pure state whose functional kernel lies in the given component, independently of the chosen pure state. The [closure-preservation theorem](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=24&start=57&end=81#L57) applies to every subset. The resulting [closure-space homeomorphism](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=24&start=84&end=88#L84), for the two specified ordinary topologies, is $\Phi_A$.

## Assumptions

The algebra is nonzero and has the compatible C*-order required by the pure-state and primitive-kernel constructions. The ordinary topology on $\widehat A$ is the kernel-induced topology just described; no topology from a quotient of the pure-state space is substituted. No injectivity of $\kappa$ is imposed.

## Conclusion

The output is the specified ordinary homeomorphism with action (1), for the kernel-induced topology on $\widehat A$ and the stated topology on $\mathrm{GS}(A)$. Its inverse is the inverse of this same bijection. No injectivity of the kernel map into the primitive spectrum is asserted.

## Main citations

- [Exact full definition](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=24&start=136&end=142#L136): `irreducibleSpectrumHomeomorph`.
- [Independent spectrum and topology](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Topology.lean.html), with its point construction in [Spectrum/Basic.lean](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Basic.lean.html): the source of the displayed homeomorphism.
- [SpectralComparison.lean](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralComparison.lean.html), `toGeometricSpectrum_ofRepresentation`: the formula for any irreducible action and any nonzero coefficient pair.
- Ryotaro Tanaka, [arXiv:2504.05551v1, Theorem 5.11 and Corollary 5.12](https://arxiv.org/abs/2504.05551v1): spectral reconstruction and the ordinary topological conclusion.

- [image_irreducibleSpectrumClosure: full closure preservation](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=24&start=57&end=81#L57).
- [irreducibleSpectrumClosureHomeomorph: the bundled map and inverse](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=24&start=84&end=88#L84).

## Lean source signature (exact)

The full definition below is copied from the pinned source.

```lean
def irreducibleSpectrumHomeomorph :
    @_root_.Homeomorph (IrreducibleSpectrum A) (NormedSpace.GeometricSpectrum ℂ A)
      inferInstance (geometricSpectrumTopology A) :=
  (irreducibleSpectrumClosureHomeomorph A).toTopologicalHomeomorph
    (isTopologizable_irreducibleSpectrumClosure A) (isTopologizable_geometricSpectrumClosure A)
```

| In the source | Mathematical meaning |
|---|---|
| `A` and the surrounding instances | The nonzero nonunital complex C*-algebra with compatible order. |
| `IrreducibleSpectrum A` | The pure-GNS representation classes, with the topology induced by their representation kernels; not the quotient topology of pure states. |
| `NormedSpace.GeometricSpectrum ℂ A` | Components of the geometric structure space, with the ordinary topology having the stated component-intersection closure. |
| `irreducibleSpectrumClosureHomeomorph A` | The specific bijection $[\pi_\varphi]\mapsto C(\ker\varphi)$ with its inverse and full closure-continuity data. |
| `.toTopologicalHomeomorph` | Uses the two named topologizability guarantees, without replacing either closure by a new one. |

### Source context (separate exact excerpt)

Source lines 28–28:

```lean
variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
```

Source lines 29–29:

```lean
variable [Nontrivial A]
```