Stream: math-comp analysis

Topic: filter versions of topological properties

view this post on Zulip Zachary Stone (Aug 04 2021 at 19:29):

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, 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?

view this post on Zulip Cyril Cohen (Aug 05 2021 at 07:04):

Maybe @Damien Rouhling would know?

view this post on Zulip Cyril Cohen (Aug 05 2021 at 07:11):

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

view this post on Zulip Zachary Stone (Aug 06 2021 at 14:33):

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.

view this post on Zulip Damien Rouhling (Aug 23 2021 at 12:13):

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: Aug 11 2022 at 02:03 UTC