The hull–kernel closure construction

Statement

A family of proper subsets of a set carries a natural closure structure. To close a subfamily, intersect its members and then take every member of the original family containing that intersection. The points of the resulting closure space are the subsets themselves.

Definition

Let be a set and let satisfy . For and , define the kernel and hull by

\begin{aligned} k(\mathscr A)&=\bigcap_{I\in\mathscr A}I,\\ h(a)&=\{I\in\mathcal F:a\subseteq I\}. \end{aligned}

The empty intersection is . The hull–kernel closure on is

c_{\mathcal F}(\mathscr A)=h(k(\mathscr A)) =\{I\in\mathcal F:k(\mathscr A)\subseteq I\}.

There are two levels of subsets: a point is a subset of , while is a set of such points. Accordingly, and .

Both and reverse inclusion, so is monotone. Every contains , giving extensivity. The cited kernel identity proves idempotence:

\begin{gathered} k(h(k(\mathscr A)))=k(\mathscr A)\\ \Longrightarrow\quad c_{\mathcal F}(c_{\mathcal F}(\mathscr A))=c_{\mathcal F}(\mathscr A). \end{gathered}

Finally,

c_{\mathcal F}(\varnothing)=h(X) =\{I\in\mathcal F:X\subseteq I\}=\varnothing,

because . These are the four closure-space axioms.

Assumptions

The only restriction on is ; the family itself may be empty. Its members are arbitrary proper subsets of . No vector-space structure, topology, or closure of under intersections is assumed.

Conclusion

The construction yields the closure space with the displayed formula. A subfamily is closed precisely when .

The separate separation theorem shows that this closure is : distinct points have distinct singleton closures. If is an antichain under inclusion, every singleton is closed, the property. The antichain condition belongs to that further theorem, not to the construction.

Main citations

Kernel, hull and the idempotence identity: ClosureSpace.HullKernel.kernel, ClosureSpace.HullKernel.hull and ClosureSpace.HullKernel.kernel_hull_kernel, lines 30–66.
Exact construction and closure formula: ClosureSpace.HullKernel.space, lines 69–89.
The separation properties: ClosureSpace.HullKernel.isT0_space and ClosureSpace.HullKernel.isT1_space_of_antichain, lines 104–134.
The four closure axioms: ClosureSpace, lines 28–30, with its laws at lines 44–61.
arXiv:2504.05551v1, Definition 4.1: the later hull–kernel construction on geometric points. The generic construction here has purely set-theoretic assumptions.

Lean source signature (exact)

The carrier X is declared in the separate source context below.

def space (F : Set (Set X)) (hF : Set.univ ∉ F) : ClosureSpace F where
  toClosureOperator := ClosureOperator.mk'
    (fun s => hull F (kernel F s))
    (by
      intro s t hst
      exact hull_antitone F (kernel_antitone F hst))
    (subset_hull_kernel F)
    (by
      intro s
      rw [kernel_hull_kernel])
  map_empty' := by
    change hull F (kernel F ∅) = ∅
    rw [kernel_empty]
    apply Set.eq_empty_iff_forall_notMem.2
    intro I hI
    have hval : I.val = Set.univ := Set.Subset.antisymm (Set.subset_univ _) hI
    exact hF (hval ▸ I.property)

In the source	Mathematical meaning
Exact declaration`X`, `F : Set (Set X)`	An arbitrary set and a family . A point is itself a subset of (`I.val`).
Exact declaration`hF : Set.univ ∉ F`	: every member is proper. The family itself may be empty.
Exact declaration`kernel F s`, `hull F`	For `s` corresponding to , , with empty intersection , and .
Exact declaration`fun s => hull F (kernel F s)`	The whole closure operation on subfamilies of .
Exact declaration`ClosureOperator.mk'`, `map_empty'`	The construction certifies monotonicity, extensivity and idempotence of this operation, and using `hF`.
Exact declaration`: ClosureSpace F`	The returned closure-space structure is on the point set , with all four closure axioms; a topology on or finite-union preservation is not part of the output.

Source context (separate exact excerpt)

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

variable {X : Type u}