The primitive geometric spectrum

Statement

The primitive geometric spectrum records the common intersections of the points belonging to each component of the geometric structure space. A primitive geometric point is an actual subset of the original normed space. Repeated intersections give one point, even if they arise from different components.

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 , define

\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 .

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. Let be the family of the resulting subsets , equipped with the following operation on :

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

The empty intersection is . Two geometric points are linked when or . Their finite-chain equivalence relation is denoted by , and

C_E(I)=\{J\in S_{\mathbb K}(E):I\sim_{c_E}J\}

is the component of . For a component set , put

J_C=\bigcap_{I\in C}I.

Define the primitive geometric spectrum by

\operatorname{PS}_{\mathbb K}(E) =\{J_{C_E(I)}:I\in S_{\mathbb K}(E)\}.

This is a family of subsets of . A vector belongs to precisely when it belongs to every geometric point in . All intersections are set intersections; no subspace or ideal structure is assumed.

Assumptions

The space is normed over , without a completeness or nontriviality hypothesis. The component construction uses the stated hull–kernel closure. Neither closedness of the component sets nor injectivity of the assignment is assumed.

Conclusion

The resulting carrier contains exactly the component intersections. The cited properness result follows from

I\in C_E(I)\quad\Longrightarrow\quad J_{C_E(I)}\subseteq I\ne E.

Thus no primitive geometric point is all of . This permits the separately defined hull–kernel closure: for ,

d_E(\mathscr T)=\left\{J\in\operatorname{PS}_{\mathbb K}(E): \bigcap_{J'\in\mathscr T}J'\subseteq J\right\}.

The present declaration supplies the carrier; the cited closure declaration supplies . For the zero space the carrier is empty. The empty-intersection convention therefore does not introduce an extra primitive point in that case.

Main citations

Geometric points and their closure: NormedSpace.geometricStructureFamily and NormedSpace.geometricStructureClosure, lines 37–65; maximal faces, NormedSpace.IsMaximalFace, lines 32–39.
Finite-chain components: ClosureSpace.component and its generating relation, lines 30–71.
Intersections and properness: ClosureSpace.HullKernel.componentKernel_ne_univ, lines 35–50; the intersection family is defined at lines 72–75.
Exact carrier and range description: NormedSpace.PrimitiveGeometricSpectrum, lines 48–54; the range characterization, lines 93–101.
Closure and emptiness: NormedSpace.primitiveGeometricSpectrumClosure, lines 109–121; the zero-space case, lines 179–199.
Ryotaro Tanaka, arXiv:2504.05551v1, Definition 4.6 and Theorem 4.7: component intersections and their closure for nontrivial Banach spaces.

Lean source signature (exact)

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

def PrimitiveGeometricSpectrum : Type u :=
  {J : Set E // J ∈ primitiveGeometricSpectrumFamily 𝕜 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`J : Set E`	A subset , rather than a subset of the geometric point set.
Exact declaration`J ∈ primitiveGeometricSpectrumFamily 𝕜 E`	There exists a geometric point with . The component is formed using .
Exact declaration`{J : Set E // J ∈ primitiveGeometricSpectrumFamily 𝕜 E}`	The full RHS defines as exactly these intersection subsets with their membership condition. The underlying subset is `J.val`; neither a representative point nor a component witness is stored.
Exact declaration`: Type u`	The output is the primitive geometric carrier. Equality is equality of subsets of , so equal intersections give one point; no ideal structure or injectivity of the component-intersection assignment is asserted.

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]