I have an open ended question. I have recently been thinking about how nice the `finite-subcover <-> ultrafilters converge`

theorem is for compactness. The proof is fairly rote, but the statement seems magical. I am not be clever enough to start with the open-cover version, and create the ultrafilter version. I'm wondering if there's a general technique to lift statements about open sets to equivalent statements about filters. As an alternative phrasing, is there a generic way to transport a definition on a topological space to one on a convergence space? Then the real prize would be a coq algorithm that takes an open-set definition, and emits _both_ the filter version, and a proof of equivalence. It seems like a powerful tool for formalizing topics like manifolds, or spectra, that are full of local properties, traditionally phrased with open covers, separations, ect.

To start, I found https://www.bioinf.uni-leipzig.de/~studla/Publications/PREPRINTS/01-pfs-007-subl1.pdf, which contains a great summary of how to define filter versions of separation axioms. But no general pattern jumps out. Is anyone here aware of some texts/papers I can continue to study on the matter?

Maybe @Damien Rouhling would know?

These two axioms give candidate translations, don't they?

Those axioms do give a translation, and I'm trying to formalize why I feel it's not enough. Maybe it's about translating quantifiers on sets or covers, to quantifiers on points and filters. The compactness statement, and the statements for regularity/normality are both examples of this.

The two axioms suggested by @Cyril Cohen indeed give candidate translations. However they won't give nice statements such as the equivalence between the existence of finite subcovers and the convergence of ultrafilters.

Unfortunately, I don't know of any means of getting such statements in a systematic way.

Last updated: Feb 05 2023 at 07:03 UTC