The irreducible spectrum and the geometric spectrum

MathlibAnnex.Analysis.CStarAlgebra.irreducibleSpectrumHomeomorph

def

Identifies irreducible representation classes with components of the geometric structure space.

Statement

Let 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 and its GNS representation , its point map is

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

Here consists of kernels of extreme points of the closed unit ball of the Banach dual of , with convexity over . The extreme-functional kernel characterization identifies this family with the original geometric structure space, with closure . The component is taken for the finite-chain relation generated by equal points and nonclosed pairs.

Definition

The source is the irreducible spectrum: pure norm-one positive bounded complex-linear functionals on , modulo unitary equivalence of their GNS representations restricted to . Equality of representation kernels is not the equivalence relation. Its topology is induced by the kernel map into the primitive spectrum with hull-kernel topology.

The target consists of components of . For a component , put . Its closure is

\overline{\mathcal D}=\left\{C:\bigcap_{D\in\mathcal D}J_D\subseteq J_C\right\},

with empty intersection . The geometric-spectrum topology has this closure.

The spectral bijection sends to . 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 applies to every subset. The resulting closure-space homeomorphism, for the two specified ordinary topologies, is .

Assumptions

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

Conclusion

The output is the specified ordinary homeomorphism with action (1), for the kernel-induced topology on and the stated topology on . 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: irreducibleSpectrumHomeomorph.
Independent spectrum and topology, with its point construction in Spectrum/Basic.lean: the source of the displayed homeomorphism.
SpectralComparison.lean, 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: spectral reconstruction and the ordinary topological conclusion.
image_irreducibleSpectrumClosure: full closure preservation.
irreducibleSpectrumClosureHomeomorph: the bundled map and inverse.

Lean source signature (exact)

The full definition below is copied from the pinned source.

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
Exact declaration`A` and the surrounding instances	The nonzero nonunital complex C*-algebra with compatible order.
Exact declaration`IrreducibleSpectrum A`	The pure-GNS representation classes, with the topology induced by their representation kernels; not the quotient topology of pure states.
Exact declaration`NormedSpace.GeometricSpectrum ℂ A`	Components of the geometric structure space, with the ordinary topology having the stated component-intersection closure.
Exact declaration`irreducibleSpectrumClosureHomeomorph A`	The specific bijection with its inverse and full closure-continuity data.
Exact declaration`.toTopologicalHomeomorph`	Uses the two named topologizability guarantees, without replacing either closure by a new one.

Exact surrounding source context (separate excerpts)

Source lines 28–28:

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

Source lines 29–29:

variable [Nontrivial A]

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

Technical documentation