MathlibAnnex.Analysis.CStarAlgebra.primitiveSpectrumHomeomorph
def
Identifies the primitive ideal spectrum with the primitive geometric spectrum.
Statement
Let be a complex C*-algebra, possibly without an identity. There is a specified ordinary homeomorphism
from the independently defined primitive ideal spectrum to the primitive geometric spectrum. Both spaces have points that are subsets of , and this homeomorphism retains each such subset. The two spectra have the hull-kernel topologies described below.
Definition
Write for the primitive spectrum: its points are subsets , where is a pure norm-one positive bounded complex-linear functional and is its GNS representation of the original algebra. This is a representation kernel, not the zero set of .
For the geometric side, let be the family of kernels of extreme points of the closed unit ball of the Banach dual of , with convexity over . The identification of this family with the face-and-support geometric structure is the conclusion of the extreme-functional kernel characterization. Its closure is . Components use the equivalence relation generated by equality and nonclosed two-point sets. For a component , put and , with repeated subsets identified.
The source topology on and target topology on have the hull-kernel closures
The ambient space in each formula is the indicated spectrum; an empty intersection is .
The map 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 supplies this bijection with closure continuity in both directions. The primitive-spectrum topologizability theorem and geometric-spectrum topologizability theorem 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 .
Conclusion
The output is the ordinary homeomorphism 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:
primitiveSpectrumHomeomorph.Primitive family equality and SpectralComparison.lean,
primitiveSpectrumEquivGeometric: the forward and inverse carrier maps.Spectrum/Topology.lean: the independent hull–kernel topology and its finite-union proof.
SpectralHomeomorph.lean,
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: the primitive-spectrum comparison and topologizability.
primitiveSpectrumClosureHomeomorph: the subset-preserving closure homeomorphism.
isTopologizable_primitiveGeometricSpectrumClosure: the target topology guarantee.
Lean source signature (exact)
The full definition below is copied from the pinned source.
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 |
|---|---|
Exact declarationA and the surrounding instances |
The same nonzero complex C*-algebra with compatible order; a unit is not required. |
Exact declarationPrimitiveSpectrum A and primitiveGeometricSpectrumTopology A |
The representation-kernel spectrum and the stated hull-kernel topology on the component-intersection family. |
Exact declarationprimitiveSpectrumClosureHomeomorph A |
The same subset-preserving bijection with full closure continuity in both directions. |
Exact declaration.toTopologicalHomeomorph and the two isTopologizable inputs |
The same bijection is a homeomorphism for the two ordinary topologies with the specified closures. |
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 ·