Filter vs Cover characterization of covering properties

Question

In mathlib, topological properties are generally characterized in terms of filters wherever possible. In particular, a set $K$ is said to be compact provided that for every nontrivial filter $F$ that contains $K$, there exists a point $k\in K$ such that every set of $F$ meets every neighborhood of $k$. This is then proven to be equivalent to the usual covers-have-finite-subcovers property. Similarly, Lindelöf spaces are defined using filters, then proven to covers-have-countable-subcovers.

A pending pull request https://github.com/leanprover-community/mathlib4/pull/11800 aims to add $\kappa$-Lindelöf by this filter definition:

Say a $\kappa$-filter is a filter $F$ for which $G\in[F]^{<\kappa}$ implies $\bigcap G\in F$. A set $S$ is $\kappa$-Lindelöf if every nontrivial $\kappa$-filter that contains $S$ has a point $s\in S$ such that every set of $F$ meets every neighborhood of $s$.

Is this equivalent to the following covering property definition?

A set $S$ is $\kappa$-Lindelöf if every open cover has a subcover of cardinality $<\kappa$.

In particular, the pull request proves this equivalence for the case $\kappa$ is regular. Is this assumption necessary?

Answer 1

These two definitions are not equivalent for singular cardinals.

To see this, let $\kappa$ be a singular cardinal, and let me describe a space that is not $\kappa$-Lindelöf in the sense of open coverings, but is $\kappa$-Lindelöf in the sense of filters: the size-$\kappa$ discrete space!

This space clearly fails to be $\kappa$-Lindelöf in the sense of open coverings -- just consider the open cover consisting of singletons.

On the other hand, suppose $F$ is a filter on $\kappa$ such that if $G \in [F]^{<\kappa}$ then $\bigcap G \in F$. Using the fact that $\kappa$ is singular, fix a collection $\mathcal C$ of subsets of $\kappa$ with $|\mathcal C| < \kappa$ such that $\bigcup \mathcal C = \kappa$ and $|X| < \kappa$ for all $X \in \mathcal C$. For each $\alpha \in \kappa$, suppose there is some $A_\alpha \in F$ with $\alpha \notin A_\alpha$ (since otherwise $\alpha \in \bigcap F$). By our condition on $F$, if $X \in \mathcal C$ then $B_X = \bigcap \{ A_\alpha :\, \alpha \in X \} \in F$, because $|X| < \kappa$. But $|\mathcal C| < \kappa$, so this means $\bigcap \{ B_X :\, X \in \mathcal C\} \in F$ as well. But $\bigcap \{ B_X :\, X \in \mathcal C\} = \emptyset$. So $F$ is not a nontrivial filter.

This shows that for any nontrivial filter $F$ on $\kappa$ such that if $G \in [F]^{<\kappa}$ then $\bigcap G \in F$, there is some $\alpha \in \kappa$ such that $\alpha \in \bigcap F$. But this means our discrete space is $\kappa$-Lindelöf in the filter sense.