Points of the geometric structure space

Statement

The geometric structure space of a normed space has as its points the support-kernel unions arising from maximal proper real convex faces of the closed unit ball. A point is the resulting subset of the vector space. Faces yielding the same subset represent the same point.

Definition

Let be a normed space over a real-or-complex scalar field , with closed unit ball . Let be the family of maximal proper real convex faces of . Explicitly, a member is a nonempty convex subset of , different from , such that

\begin{gathered} x,y\in B_E,\quad 0<t<1,\quad (1-t)x+ty\in M\\ \Longrightarrow\quad x,y\in M, \end{gathered}

and every proper convex face containing equals . The scalar is real, including when is complex.

Write for the continuous -linear dual. For , 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 .

The family of geometric points is

\mathcal F_{\mathbb K}(E)=\{I_{\mathbb K}(M):M\in\mathfrak M_E\}.

The geometric structure space has precisely these subsets as its points. Thus an element is a subset with a face satisfying . Choosing a representing face does not add data to the point. The assignment is not asserted to be injective.

Assumptions

The space is normed over ; completeness and nontriviality are not required. Convexity and the face condition are taken over the reals. Exposedness and supporting-functional existence are not additional conditions on the maximal-face predicate.

Conclusion

The resulting point set is . Each point is a proper subset of : if and , then for every , so . Consequently , as required by the later hull–kernel closure construction.

The cited zero-space result gives when . The present declaration specifies the points; the closure operation is a separate construction.

Main citations

Maximal proper real convex faces: NormedSpace.IsMaximalFace, lines 32–39; its zero-space exclusion, lines 45–52.
Supporting functionals and their kernel union: NormedSpace.supportFunctionals, lines 42–43; NormedSpace.supportKernelUnion, lines 108–109, and properness, lines 130–142.
The family and the exact point type: NormedSpace.geometricStructureFamily and NormedSpace.GeometricStructureSpace, lines 37–54; the zero-space result, lines 73–86.
arXiv:2504.05551v1, Definition 4.1: the face-based construction. The formal source separates its carrier from its closure and allows normed spaces without completeness or nontriviality.

Lean source signature (exact)

The following definition and the related family definition share the surrounding scalar and space context reproduced below.

def GeometricStructureSpace : Type u := {I : Set E // I ∈ 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`I : Set E`	A subset , regarded as a possible geometric point.
Exact declaration`I ∈ geometricStructureFamily 𝕜 E`	The condition : there exists a maximal proper real convex face of the closed unit ball with .
Exact declaration`{I : Set E // I ∈ geometricStructureFamily 𝕜 E}`	The complete defining type consists of such subsets with their membership condition. A point `p` has underlying subset `p.val`; no chosen face is stored.
Exact declaration`: Type u`	The output is the point set , before any closure-space structure is attached.

Related definition — separate exact excerpt. The family used above is defined at lines 37–39 of the same source file.

def geometricStructureFamily : Set (Set E) :=
  letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
  {I | ∃ F : Set E, IsMaximalFace F ∧ supportKernelUnion 𝕜 F = I}

In the source	Mathematical meaning
Exact declaration`letI ... := NormedSpace.restrictScalars ℝ 𝕜 E`	Convexity and faces use the real vector-space structure induced from the given -space; this is not an extra choice or assumption.
Exact declaration`∃ F : Set E, IsMaximalFace F ∧ supportKernelUnion 𝕜 F = I`	One subset must satisfy both conditions: it is a maximal proper real convex face of the closed unit ball and its support-kernel union equals . Here the source name `F` denotes .
Exact declaration`: Set (Set E)`	The full RHS defines the family of resulting subsets. Equal subsets give the same member even when their witnessing faces differ; no face is chosen as part of the output.

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]