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

# The primitive spectrum and the primitive geometric spectrum

## Statement

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

$$
\Psi_A:\operatorname{Prim}(A)\longrightarrow\mathrm{PS}(A),
$$

from the independently defined primitive ideal spectrum to the primitive geometric spectrum. Both spaces have points that are subsets of $A$, and this homeomorphism retains each such subset. The two spectra have the hull-kernel topologies described below.

## Definition

Write $\operatorname{Prim}(A)$ for the [primitive spectrum](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Primitive.lean.html?from=23&start=33&end=33#L33): its points are subsets $P=\ker\pi_\varphi\subseteq A$, where $\varphi$ is a pure norm-one positive bounded complex-linear functional and $\pi_\varphi$ is its GNS representation of the original algebra. This is a representation kernel, not the zero set of $\varphi$.

For the geometric side, let $S(A)$ be the family of kernels of extreme points of the closed unit ball of the Banach dual of $A$, with convexity over $\mathbb R$. The identification of this family with the face-and-support geometric structure is the conclusion of [the extreme-functional kernel characterization](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ExtremeKernel.lean.html?from=23&start=49&end=65#L49). Its closure is $c_A(\mathcal U)=\{I\in S(A):\bigcap_{J\in\mathcal U}J\subseteq I\}$. Components use the equivalence relation generated by equality and nonclosed two-point sets. For a component $C$, put $J_C=\bigcap_{I\in C}I$ and $\mathrm{PS}(A)=\{J_C:C\text{ a component}\}$, with repeated subsets identified.

The source topology on $\operatorname{Prim}(A)$ and target topology on $\mathrm{PS}(A)$ have the hull-kernel closures
$$
\overline{\mathcal U}=\left\{P:\bigcap_{Q\in\mathcal U}Q\subseteq P\right\},
\qquad
\overline{\mathcal V}=\left\{J:\bigcap_{K\in\mathcal V}K\subseteq J\right\}.
$$
The ambient space in each formula is the indicated spectrum; an empty intersection is $A$.

The map $\Psi_A$ sends a primitive kernel to the identical subset regarded as a primitive geometric point; its inverse also retains the subset. The [subset-preserving closure homeomorphism](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=23&start=32&end=38#L32) supplies this bijection with closure continuity in both directions. The [primitive-spectrum topologizability theorem](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Topology.lean.html?from=23&start=88&end=89#L88) and [geometric-spectrum topologizability theorem](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=23&start=98&end=101#L98) supply ordinary topologies with exactly these closures, making the same bijection an ordinary homeomorphism.

## Assumptions

The input is a nonzero complex C*-algebra, not necessarily unital, with the compatible partial order and star order in the displayed scope. Both spectra carry the hull-kernel topologies stated above. The correspondence of the two families and the topologizability results are provided by the cited source declarations, not additional assumptions on $A$.

## Conclusion

The output is the ordinary homeomorphism $\Psi_A$ with the same underlying subset in both directions. It includes continuity of that map and its inverse. It does not identify a functional kernel with a representation kernel.

## Main citations

- [Exact full definition](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=23&start=128&end=133#L128): `primitiveSpectrumHomeomorph`.
- [Primitive family equality](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralComparison.lean.html?from=23&start=142&end=159#L142) and [SpectralComparison.lean](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralComparison.lean.html), `primitiveSpectrumEquivGeometric`: the forward and inverse carrier maps.
- [Spectrum/Topology.lean](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Topology.lean.html): the independent hull–kernel topology and its finite-union proof.
- [SpectralHomeomorph.lean](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html), `primitiveSpectrumClosureHomeomorph`, `image_primitiveSpectrumClosure`, `image_symm_primitiveGeometricSpectrumClosure`: the two closure directions and their ordinary topological conversion.
- Ryotaro Tanaka, [arXiv:2504.05551v1, Theorem 5.11 and Corollary 5.12](https://arxiv.org/abs/2504.05551v1): the primitive-spectrum comparison and topologizability.

- [primitiveSpectrumClosureHomeomorph: the subset-preserving closure homeomorphism](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=23&start=32&end=38#L32).
- [isTopologizable_primitiveGeometricSpectrumClosure: the target topology guarantee](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.lean.html?from=23&start=98&end=101#L98).

## Lean source signature (exact)

The full definition below is copied from the pinned source.

```lean
def primitiveSpectrumHomeomorph :
    @_root_.Homeomorph (PrimitiveSpectrum A) (NormedSpace.PrimitiveGeometricSpectrum ℂ A)
      inferInstance (primitiveGeometricSpectrumTopology A) :=
  (primitiveSpectrumClosureHomeomorph A).toTopologicalHomeomorph
    (isTopologizable_primitiveSpectrumClosure A)
    (isTopologizable_primitiveGeometricSpectrumClosure A)
```

| In the source | Mathematical meaning |
|---|---|
| `A` and the surrounding instances | The same nonzero complex C*-algebra with compatible order; a unit is not required. |
| `PrimitiveSpectrum A` and `primitiveGeometricSpectrumTopology A` | The representation-kernel spectrum and the stated hull-kernel topology on the component-intersection family. |
| `primitiveSpectrumClosureHomeomorph A` | The same subset-preserving bijection with full closure continuity in both directions. |
| `.toTopologicalHomeomorph` and the two `isTopologizable` inputs | The same bijection is a homeomorphism for the two ordinary topologies with the specified closures. |

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