Counting distinct topological bases for finite sets of size N
On the Number of Distinct Topological Bases of a Finite Set of Size $N$
Logic in Computer Science
Summary
When you have a set with a certain number of items, there are many ways to build a structure called a topology on it. The authors found a precise formula for counting how many different basic building blocks, called bases, can generate these topologies. They used a computer proof assistant called Lean 4 to verify their results and explored small examples and growth behavior. This work helps in understanding the underlying complexity of finite topologies.
What this means in practice
- •For computational topologists: Count and classify all possible bases of topologies on small finite sets to aid computational experiments in topology.
- •For software verification engineers: Use the formalized counting results in Lean 4 to improve proofs involving finite topologies in verified software modules.
A theory result. No direct application yet.
Authors
Lars Warren Ericson
Abstract
For a finite set $S$ with $\lvert S\rvert = N$, the number of families $\mathcal{B} \subseteq \mathcal{P}(S)$ that are topological bases is $\#(N) = \sum_{\mathcal{T} \in \operatorname{Top}(S)} 2^{\lvert\mathcal{T}\rvert - \lvert\mathcal{M}_{\mathcal{T}}\rvert}$, where $\mathcal{M}_{\mathcal{T}}$ is the canonical minimal basis of minimal open neighborhoods. The identity is proved in Lean 4 / Mathlib (`CARDB.lean`): bases generating $\mathcal{T}$ are exactly the sets with $\mathcal{M}_{\mathcal{T}} \subseteq \mathcal{B} \subseteq \mathcal{T}$. The small-$N$ table and the discrete-dominance sandwich are proved in `CARDB/SmallN.lean` and `CARDB/Asymptotics.lean`.