The geometric structure closure

Statement

The geometric structure closure equips the set of geometric points with the hull–kernel rule. It closes a collection of points by intersecting them as subsets of the original vector space and then taking all geometric points containing that intersection.

Definition

Let be a normed space over a real-or-complex scalar field , and let denote its continuous -linear dual. Write . A maximal proper real convex face of is a nonempty convex subset, different from , that contains both endpoints of any segment in whose interior meets , and is maximal among proper convex faces.

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 .

Let be the set of resulting subsets as ranges over these faces. Equal subsets are the same geometric point.

For , define

\begin{aligned} k_E(\mathscr A)&=\bigcap_{J\in\mathscr A}J,\\ c_E(\mathscr A)&=\{I\in S_{\mathbb K}(E):k_E(\mathscr A)\subseteq I\}. \end{aligned}

The intersection is taken inside , with , while is a set of geometric points. Each geometric point is proper: any in a representing face satisfies for all its supporting functionals and hence lies outside their kernel union. The cited hull–kernel construction therefore applies to this family and proves, for all ,

\begin{gathered} \mathscr A\subseteq c_E(\mathscr A),\qquad \mathscr A\subseteq\mathscr B\Longrightarrow c_E(\mathscr A)\subseteq c_E(\mathscr B),\\ c_E(c_E(\mathscr A))=c_E(\mathscr A),\qquad c_E(\varnothing)=\varnothing. \end{gathered}

Assumptions

The space is normed over , without a completeness or nontriviality hypothesis. Properness of every geometric point follows from the defining faces and is supplied internally to the hull–kernel construction.

Conclusion

The result is the closure space . A collection of geometric points is closed when it is fixed by the displayed operation. This operation acts on collections of points; it is distinct from norm closure inside .

The source separately proves (distinct points have distinct singleton closures) and later (every singleton is closed), the latter using incomparability of distinct geometric points under inclusion. Finite-union preservation is not asserted here. For the zero space, the carrier is empty and the same construction applies.

Main citations

Faces, functionals and the point family: NormedSpace.IsMaximalFace; the family and its properness, NormedSpace.geometricStructureFamily and NormedSpace.univ_notMem_geometricStructureFamily, lines 37–54.
Exact closure and its membership formula: NormedSpace.geometricStructureClosure, lines 57–65; and the zero-space results, lines 68–86.
The construction proving the four axioms: ClosureSpace.HullKernel.space, lines 69–89.
Incomparability and singleton closedness: NormedSpace.GeometricStructureSpace.eq_of_subset and NormedSpace.isT1_geometricStructureClosure, lines 52–72.
arXiv:2504.05551v1, Definition 4.1: the same hull–kernel formula on geometric points; the source retains the weaker normed-space assumptions stated here.

Lean source signature (exact)

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

def geometricStructureClosure : ClosureSpace (GeometricStructureSpace 𝕜 E) :=
  ClosureSpace.HullKernel.space (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 ; it may be zero and need not be complete.
Exact declaration`GeometricStructureSpace 𝕜 E`, `geometricStructureFamily 𝕜 E`	The point set and its underlying family of subsets , defined by maximal-face support-kernel unions.
Exact declaration`ClosureSpace.HullKernel.space (geometricStructureFamily 𝕜 E)`	The defining construction gives for every subfamily ; an empty intersection is .
Exact declaration`univ_notMem_geometricStructureFamily 𝕜 E`	The cited properness theorem supplies . It is a proved input to the constructor, not an additional hypothesis on .
Exact declaration`: ClosureSpace (GeometricStructureSpace 𝕜 E)`	The returned object is the operation together with extensivity, monotonicity, idempotence and . Finite-union preservation is not 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]