From components to their common kernel

Statement

The natural map from the geometric spectrum to the primitive geometric spectrum sends a component to the intersection of all its geometric points. The map is surjective. With the separately defined spectrum closures, it preserves the closure of each selected set by an exact image formula.

Definition

Let be a normed space over a real-or-complex scalar field , with closed unit ball and continuous -linear dual . The geometric point set consists of the subsets

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

where ranges over nonempty maximal proper real convex faces of . A face is a convex subset containing both endpoints of every segment in the ball whose interior meets it; maximality is among proper convex faces. Equal resulting subsets are the same geometric point. Here means for every .

For , the geometric structure closure is

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

Two points are linked if or . Let be all points reachable from by a finite chain of such linked pairs, including itself. Define

\begin{aligned} \operatorname{GS}_{\mathbb K}(E)&=\{C_E(I):I\in S_{\mathbb K}(E)\},\\ J_C&=\bigcap_{I\in C}I,\\ \operatorname{PS}_{\mathbb K}(E)&=\{J_C:C\in\operatorname{GS}_{\mathbb K}(E)\}. \end{aligned}

The component-intersection map is

\gamma_E:\operatorname{GS}_{\mathbb K}(E)\longrightarrow\operatorname{PS}_{\mathbb K}(E), \qquad \gamma_E(C)=J_C.

It takes a set of geometric points to a subset of . It uses the component set itself, so changing its representative does not change the output.

The cited surjectivity theorem has a direct witness argument. Given , choose a geometric point witnessing . Then satisfies

\gamma_E(C)=J_{C_E(I_0)}=J.

This choice proves existence of a preimage. It makes no uniqueness assertion about the witnessing point or component.

Assumptions

The space is normed over , without completeness or nontriviality hypotheses. All component kernels are intersections of subsets of . The map has no additional input, and injectivity is not an assumption or a conclusion of this declaration.

Conclusion

The output is the specified map ; the separately cited theorem proves that it is surjective. Its role in the closure constructions is expressed by the following formulas. For selections and , put

\begin{aligned} d_E(\mathscr T)&=\left\{J\in\operatorname{PS}_{\mathbb K}(E): \bigcap_{J'\in\mathscr T}J'\subseteq J\right\},\\ g_E(\mathscr U)&=\gamma_E^{-1}\bigl(d_E(\gamma_E(\mathscr U))\bigr). \end{aligned}

Empty intersections are . These separately defined operations are the primitive and geometric spectrum closures. The pullback formula makes closure-continuous, and surjectivity gives the stronger identity

\gamma_E(g_E(\mathscr U))=d_E(\gamma_E(\mathscr U)).

Indeed, surjectivity gives for every subset of the codomain; apply this to . These closure statements are supplied by the cited companion declarations. They do not turn into a homeomorphism without an additional injectivity result. For the zero space, both carriers are empty and the same definition applies.

Main citations

The face-defined geometric points and closure: NormedSpace.geometricStructureFamily, NormedSpace.GeometricStructureSpace and NormedSpace.geometricStructureClosure, lines 37–65; the face condition, NormedSpace.IsMaximalFace, lines 32–39.
Linked pairs and components: ClosureSpace.Linked, ClosureSpace.Related and ClosureSpace.component, lines 30–71.
The two spectrum carriers and component kernel: NormedSpace.GeometricSpectrum, NormedSpace.geometricSpectrumKernel and NormedSpace.PrimitiveGeometricSpectrum, lines 36–54; the primitive range characterization, lines 93–101.
Exact map, its value and surjectivity: NormedSpace.geometricSpectrumToPrimitive, lines 68–74; NormedSpace.geometricSpectrumToPrimitive_surjective, lines 88–90. Surjectivity is supplied by this separate theorem.
The witness used by the generic construction: ClosureSpace.HullKernel.componentPointToComponentKernelPoint and its surjectivity theorem, lines 80–95.
The closures and their exact image formula: NormedSpace.primitiveGeometricSpectrumClosure, NormedSpace.geometricSpectrumClosure, NormedSpace.continuous_geometricSpectrumToPrimitive and NormedSpace.image_geometricSpectrumToPrimitive_closure, lines 109–157; the generic image-of-pullback identity is here, ClosureSpace.image_induced_closure, lines 74–80.
Ryotaro Tanaka, arXiv:2504.05551v1, Definition 4.6 and Theorem 4.7: the map and the two closure formulas. The formal source allows the weaker normed-space assumptions stated above.

Lean source signature (exact)

The scalar and normed-space declarations used in this construction are reproduced separately below.

def geometricSpectrumToPrimitive : GeometricSpectrum 𝕜 E → PrimitiveGeometricSpectrum 𝕜 E :=
  ClosureSpace.HullKernel.componentPointToComponentKernelPoint
    (geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕜 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`GeometricSpectrum 𝕜 E → PrimitiveGeometricSpectrum 𝕜 E`	The entire output type is a map , from component subsets to their intersection subsets.
Exact declaration`ClosureSpace.HullKernel.componentPointToComponentKernelPoint`	For every component , the defining value is . The component membership supplies a witness that this intersection lies in the target family.
Exact declaration`geometricStructureFamily 𝕜 E`	The family of geometric points on which the generic component-intersection construction is applied.
Exact declaration`univ_notMem_geometricStructureFamily 𝕜 E`	The already proved properness is the constructor input; it is not an extra assumption on .
The complete RHSExact declaration	These arguments specify the map on all components. Its cited surjectivity theorem gives ; neither a unique preimage nor closure continuity is a field of this function definition.

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]