Unions of kernels of supporting functionals

Statement

For a subset of a seminormed space, consider the contractive continuous linear functionals that equal throughout that subset. The support-kernel union consists of the vectors annihilated by at least one of these functionals. It is a union of kernels, with no assertion that the union is a vector subspace.

Definition

Let be a seminormed space over a real-or-complex scalar field , and let be its continuous -linear dual with the operator norm. For , put

\Sigma_{\mathbb K}(M)=\{f\in E^*: \|f\|\leq1,\ f|_M=1\},

where means for every . Define

\begin{aligned} I_{\mathbb K}(M)&=\bigcup_{f\in\Sigma_{\mathbb K}(M)}\ker f\\ &=\{y\in E:\exists f\in\Sigma_{\mathbb K}(M),\ f(y)=0\}. \end{aligned}

Thus membership requires one witnessing functional. It does not require all supporting functionals to vanish. For nonempty , the condition is equivalent to . The pointwise formulation also covers .

The cited elementary identities make the empty cases explicit:

\begin{aligned} \Sigma_{\mathbb K}(M)=\varnothing&\Longrightarrow I_{\mathbb K}(M)=\varnothing,\\ 0\in I_{\mathbb K}(M)&\Longleftrightarrow\Sigma_{\mathbb K}(M)\ne\varnothing,\\ I_{\mathbb K}(\varnothing)&=E. \end{aligned}

The last equality follows because the zero functional belongs to and has kernel .

Assumptions

The space may have a seminorm: definiteness and completeness are not required. The subset is arbitrary. It need not be nonempty, convex or contained in the unit ball, and the definition does not assume that a supporting functional exists.

Conclusion

The output is the subset of . For each , a supporting functional has , so it cannot also annihilate . Consequently

M\cap I_{\mathbb K}(M)=\varnothing, \qquad M\ne\varnothing\Longrightarrow I_{\mathbb K}(M)\ne E.

This properness result, proved in the cited source, is what later permits the hull–kernel construction for maximal faces.

Main citations

The supporting family and its nonempty image characterization: NormedSpace.supportFunctionals, lines 42–43; the equivalence for nonempty subsets is at lines 59–78.
Exact union and union-of-kernels formula: NormedSpace.supportKernelUnion, lines 108–122.
Disjointness, properness and the empty cases: lines 130–161.
The real-or-complex scalar interface: Mathlib RCLike, at the pinned mathlib commit.
arXiv:2504.05551v1, Definition 4.1: the support-kernel union for maximal faces of a nontrivial Banach space. The present declaration allows arbitrary subsets of seminormed spaces.

Lean source signature (exact)

The exact definition uses the scalar and space declarations reproduced separately below.

def supportKernelUnion (F : Set E) : Set E :=
  {x | ∃ f ∈ supportFunctionals 𝕜 F, f x = 0}

In the source	Mathematical meaning
Exact declaration`𝕜`, `[RCLike 𝕜]`	The scalar field is real or complex.
Exact declaration`E`, `[SeminormedAddCommGroup E]`, `[NormedSpace 𝕜 E]`	is a seminormed vector space over ; completeness and a nonzero vector are not assumed.
Exact declaration`F : Set E`	The arbitrary subset , possibly empty.
Exact declaration`supportFunctionals 𝕜 F`	, where is the continuous linear dual (`StrongDual 𝕜 E`).
Exact declaration`{x \| ∃ f ∈ supportFunctionals 𝕜 F, f x = 0}`	The full defining subset . For each vector , one functional must satisfy both supporting conditions and annihilate .
Exact declaration`: Set E`	The output is a subset of , the union of these kernels. It is not bundled as a linear subspace, and the supporting family need not be nonempty.

Source context (separate exact excerpt)

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

variable (𝕜 : Type v) [RCLike 𝕜]
variable {E : Type u} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]