The geometric spectrum

Statement

The geometric spectrum of a normed space is the set of finite-chain components of its geometric structure space. Each spectrum point is an actual component subset. Two choices of a geometric point in the same component give one spectrum point.

Definition

Let be a normed space over a real-or-complex scalar field , with closed unit ball and continuous -linear dual . For each nonempty maximal proper real convex face of , put

\begin{aligned} \Sigma_{\mathbb K}(M)&=\{f\in E^*: \|f\|\leq1,\ f|_M=1\},\\ I_{\mathbb K}(M)&=\bigcup_{f\in\Sigma_{\mathbb K}(M)}\ker f. \end{aligned}

Here means for every .

Here a face is a convex subset containing both endpoints of any segment in the ball whose interior meets it; maximality is among proper convex faces. The geometric point set consists of the resulting subsets , with equal subsets regarded as the same point. Its hull–kernel closure is

\begin{gathered} c_E(\mathscr A)=\left\{I\in S_{\mathbb K}(E):\bigcap_{J\in\mathscr A}J\subseteq I\right\},\\ \mathscr A\subseteq S_{\mathbb K}(E), \end{gathered}

where the empty intersection is .

For , write when or . Write when they can be joined by a finite chain of these linked pairs, allowing a chain with no steps. Define

\begin{aligned} C_E(I)&=\{J\in S_{\mathbb K}(E):I\sim_{c_E}J\},\\ \operatorname{GS}_{\mathbb K}(E)&=\{C_E(I):I\in S_{\mathbb K}(E)\}. \end{aligned}

The second set is the geometric spectrum. Its elements are subsets of , while the members of each such subset are themselves subsets of . Equality of spectrum points means equality of component sets.

Assumptions

The space is normed over . Completeness and nontriviality are not required. The component relation is formed using ; it does not assume that this closure preserves finite unions.

Conclusion

The declaration supplies the point set . Every member is nonempty, because . The separately cited projection

q_E:S_{\mathbb K}(E)\longrightarrow\operatorname{GS}_{\mathbb K}(E), \qquad q_E(I)=C_E(I),

is surjective, and exactly when . This makes explicit how the same component is independent of its chosen starting point.

For the zero space, the geometric spectrum is empty. Its closure structure is defined separately from this carrier; it uses the intersections of component members. The component itself is not replaced by its closure .

Main citations

The geometric points and their closure: NormedSpace.geometricStructureFamily, NormedSpace.GeometricStructureSpace and NormedSpace.geometricStructureClosure, lines 37–65; the face predicate, NormedSpace.IsMaximalFace, lines 32–39.
Linked pairs and finite-chain components: ClosureSpace.Linked, ClosureSpace.Related and ClosureSpace.component, lines 30–71.
The component family and equality criterion: ClosureSpace.component_eq_iff_related and ClosureSpace.componentFamily, lines 30–44.
Exact spectrum carrier and the projection: NormedSpace.geometricSpectrumFamily and NormedSpace.GeometricSpectrum, lines 36–41; NormedSpace.toGeometricSpectrum, lines 57–58, and its surjectivity, lines 81–82.
Separate closure and zero-space results: NormedSpace.geometricSpectrumClosure, lines 114–115; emptiness of the carrier, lines 169–192.
Ryotaro Tanaka, arXiv:2504.05551v1, Definition 4.6: the component-set realization of the geometric spectrum. The formal source allows the weaker normed-space assumptions above.

Lean source signature (exact)

The scalar and normed-space declarations shared by this definition are reproduced separately below.

def GeometricSpectrum : Type u :=
  {C : Set (GeometricStructureSpace 𝕜 E) // C ∈ geometricSpectrumFamily 𝕜 E}

In the source	Mathematical meaning
Exact declaration`𝕜`, `[RCLike 𝕜]`	The real or complex scalar field .
Exact declaration`E`, `[NormedAddCommGroup E]`, `[NormedSpace 𝕜 E]`	A normed vector space over , possibly zero and not necessarily complete.
Exact declaration`GeometricStructureSpace 𝕜 E`	The geometric point set of maximal-face support-kernel unions, equipped in the component construction with .
Exact declaration`C : Set (GeometricStructureSpace 𝕜 E)`	A possible component subset ; its members are themselves subsets of .
Exact declaration`C ∈ geometricSpectrumFamily 𝕜 E`	There exists such that , where is the finite-chain component for .
Exact declaration`{C : Set ... // C ∈ geometricSpectrumFamily 𝕜 E}`	The full defining type contains exactly those component subsets with their membership condition. The underlying component is `C.val`; no representative is stored.
Exact declaration`: Type u`	The output is the spectrum carrier. The spectrum closure and the surjective map are separately defined or proved, as cited above.

Source context (separate exact excerpt)

The surrounding declarations below are from lines 32–33; their mathematical meaning is included in the guide above.

variable (𝕜 : Type v) [RCLike 𝕜]
variable (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E]