Ordering on filters

Stream: general

[Bernd Losert]

Is it just me or is the ordering of filters backwards?

[Bernd Losert]

Ultrafilters are supposed to be maximal filters, but not according to the ≤.

[Adam Topaz]

The ordering on filters mimics the ordering of sets. See docs#filter.principal_mono

[Kyle Miller]

Filters are "generalized sets", and ultrafilters are "generalized points" (that lemma Adam linked to shows that sets can be faithfully represented as filters).

[Bernd Losert]

Hmm... but this "generalized sets" point of view is not that common, is it?

[Kevin Buzzard]

In the mathematical literature it seems to be common to not let the entire power set be a filter either. But there are conventions here and this order does stick to the conventions. The type of topological space structures on a fixed type is also ordered "backwards" if you think about a topology as being a collection of open sets. But this is not the only way to think about a topology. There seems to be a general principle in mathlib that a ≤ b means "there's a map from a to b or some kind of idea of that form. So for example with topological spaces T1<=T2 means that the identity function from (X,T1) to (X,T2) is continuous, which means that T1 has more sets than T2. Similarly for filters F1<=F2 means that the predicate tendsto id F1 F2 is true, ie F1 tends to F2 along the identity map. Thinking about filters like this took some getting used to for me but now I think that it's a good idea because it better encapsulates the "meaning" of a filter than the naive approach. We don't think of a topology as a collection of open sets whten though that's what the formal definition is. If you buy into this "a<=b if there's a map from a to b" idea then you can see that the more open sets there are, the easier it is to map out of, so it makes some kind of sense. Similarly I now think that this is a good way to think about filters, eg the neighborhood filter of a point can fruitfully be thought of as an infinitesimal neighborhood of the point which turns out to be a powerful picture in topology, for example it makes it intuitively obvious that a function is continuous iff infinitesimal neighbourhoods in the source tend to infinitesimal neighbourhoods in the target rather than getting ripped apart as they would be for discontinuous functions. Perhaps you could say that this point of view was a geometric one, and perhaps it's not surprising that this is the viewpoint here because topology is all done using filters in mathlib

[Kyle Miller]

(Category theory question: are filters the pro-completion of the poset set X? is this the precise sense in which filters are generalized sets?)

[Kevin Buzzard]

I like the idea that ideals are the ind-completion and if that's true then taking complements you get that filters are the pro-completion. This is not a proof :-)

[Bernd Losert]

I do research in convergence spaces, which are defined by specifying which filters convergence to which points. In this area, a filter is thought of as just a generalization of a sequence. A typical property of convergent sequences is that every subsequence converges. In terms of filters, it would be that every subfilter of a convergent filter converges. One thing I like about the ≤ ordering in lean is that "subfilter" makes sense with this ordering.

[Patrick Massot]

Bernd Losert said:

In this area, a filter is thought of as just a generalization of a sequence.

In mathlib (and other formalized libraries), filters are used a lot more that this. As far as I can tell, the ubiquity of filters in mathlib has no analogue in the real world. For instance Bourbaki barely uses filters compared to mathlib. And Bourbaki never write an inequality sign between two filters or any two topologies, they always use words like finer or coarser.

[Bernd Losert]

Yep. Finer and coarser is pretty typical nomenclature. You'll also find the term "corefines" in my area.

[Bernd Losert]

I just realized I have an issue: Since the power set is a subfilter of every filter including all the pure filters, it follows that the power set converges to everything. I'm going to have to rule out the power set in the definitions.

[Yury G. Kudryashov]

We have docs#filter.ne_bot

[David Wärn]

Kevin Buzzard said:

I like the idea that ideals are the ind-completion and if that's true then taking complements you get that filters are the pro-completion. This is not a proof :-)

In order-theoretic lingo you would say that ideals form the free "directed complete partial order" or dcpo on a preorder. The proof is straightforward. I wrote in out in Lean here

[Kevin Buzzard]

Oh nice! Thanks for sorting out that loose end!