Filters

Stream: new members

[Valery Isaev]

I heard that analysis and topology in Lean is implemented using filters which are supposed to be more convenient from formalization point of view. I'd like to know what are advantages of this approach compared to the ordinary way of doing things.

[Johan Commelin]

@Valery Isaev Patrick wrote a nice short discussion in our perfectoid paper: https://math.commelin.net/files/poplws20cpp_perfectoid.pdf

[Johan Commelin]

You will want section 4

[Kevin Buzzard]

I think Johannes Hoelzl ported a lot of the basic results from Isabelle, following a book by I James. Hoelzl might well have written the Isabelle code as well

[Patrick Massot]

The first step is to read the module docstring at https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html. Then indeed there should be stuff in the perfectoid paper (I already started to forgot what's in there exactly). The book by James is "Topologies and uniformities". PM me if you have difficulties finding it

[Rob Lewis]

I see a badly formed doc string there!

[Patrick Massot]

Also note that the new book Mathematics in Lean will eventually contain explanations about you need to know here

[Patrick Massot]

Rob Lewis said:

I see a badly formed doc string there!

Probably a bad space again

[Valery Isaev]

Thanks for the references. If I understand correctly, the advantage is that various notions of limits are defined in terms of filters and hence the same lemmas and definitions can be used to establish the basic theory for them.

[Kevin Buzzard]

As a mathematician the advantages I see to filters are pretty much what you say: I can say "this sequence of reals tends to 7", "this sequence of reals diverges to +infinity", "this continuous function of x tends to 7 as x tends to 37", "this continuous function tends to 0 as x tends to -infinity" etc. But my impression is that there are other advantages too.

[Kevin Buzzard]

Note in particular this very general "tendsto" predicate; I think that this was one of the key insights.

[Callum Cassidy-Nolan]

So I started watching Patrick Massots video on filters in topology but I was having some trouble understanding it. I'm reading out of this : https://www.imo.universite-paris-saclay.fr/~pmassot/topology.pdf

I understand the definition of filter:
image.png

I've also been able to understand that these examples are filters:

image.png

The part I don't really understand is why this means "limit":

image.png

(Maybe an example of a limit which is equivalent to lim x -> a, f(x) = l in the filter form could help me understand)

[Adam Topaz]

Is docs#continuous.tendsto something that would be helpful for you?

[Yaël Dillies]

The idea is like this. You want to describe neighborhoods of a point, so you take a set around that point. But being in that neighborhood is not quite enough, so you set out to find more neighborhoods. Now, you have a bunch. What can you say about them. Well surely if a set contains some neighborhood, it must be a neighborhhod itself. And if two sets are neighborhoods, then their intersection is a neighborhood. univ should definitely be a neighborhood. Is anything else obvious from the intuition of neighborhoods? Not really

[Yaël Dillies]

So somehow you have a set of sets around your point which respect a bunch of properties. You can picture them as being vanishingly smmal around that point.

[Yaël Dillies]

But really this didn't use the fact that you were around a point. You could also have had a bunch of sets "vanishing at infinity". This gives you the at_top filter.

[Callum Cassidy-Nolan]

I'm trying to remember if neighborhood is an open set containing x, or just a set which contains x...

[Callum Cassidy-Nolan]

Oh found it in the docs

[Adam Topaz]

In this context, a neighborhood is a subset which contains an open neighborhood of the given point.

[Yaël Dillies]

It's a set which contains an open set containing x

[Callum Cassidy-Nolan]

Ah ok thanks for the confirmation.

[Callum Cassidy-Nolan]

What is the inverse function doing though?

[Callum Cassidy-Nolan]

Or the pre-image

[Yaël Dillies]

For a function to tend to something, you want to know that being close to a point in the domain means you're close to its image in the codomain.

[Yaël Dillies]

This means that neighborhoods in the codomain must come from neighborhoods in the domain. This is confusing, yeah.

[Callum Cassidy-Nolan]

Would this be saying that the limit of f as x -> a is l ? image.png

[Callum Cassidy-Nolan]

So neighborhoods from the codomain come from neighborhoods from the domain:

(y should be l & x should be a)

[Callum Cassidy-Nolan]

But how does that mean that if a neighborhood from the codomain is close to l , then the neighborhood it came from is close to a ?

[Callum Cassidy-Nolan]

Like what if a neighborhood really close to l came from a neighborhood that was not close to a ?

[Adam Topaz]

That's okay, because you're taking the preimage of the nhd of l!

[Adam Topaz]

(and filters are upward closed)

[Callum Cassidy-Nolan]

But then how does that capture the idea of " you want to know that being close to a point in the domain means you're close to its image in the codomain." ?

[Yaël Dillies]

Think about it the other way around. If the preimage of something to a doesn't contain everything close to l, that means there's something close to l whose image is far from a!

[Adam Topaz]

Because if l' is "close" to l in the codomain, then there should have been something, say x' in the domain, which should be close to x, such that x' maps to l'

[Adam Topaz]

So you take the preimage of the stuff that's close to l and that should contain the stuff that's close to x. Since you're dealing with filters, if something contains the stuff which is close to x, then it is already "close" as well

[Callum Cassidy-Nolan]

Adam Topaz said:

Because if l' is "close" to l in the codomain, then there should have been something, say x' in the domain, which should be close to x, such that x' maps to l'

So why is a situation like this impossible ? https://i.imgur.com/r2qfIcK.jpg

[Callum Cassidy-Nolan]

a maps to l and a' maps to a' but a and a' are far away in the domain.

[Adam Topaz]

What's the preimage of the stuff that's close to l?

[Adam Topaz]

Does it contain the stuff close to a?

[Kevin Buzzard]

Remember that the constant function is continuous

[Callum Cassidy-Nolan]

If the stuff close to l is a set V then the preimage is the set of points {x in X | f(x) in V}

[Adam Topaz]

In your picture, it would be the oval on the left, and that certainly contains the stuff close to a!

[Callum Cassidy-Nolan]

but why? a' is far away from a

[Callum Cassidy-Nolan]

What does far even mean in the context of filters?

[Adam Topaz]

I think @Kevin Buzzard has a blogpost on filters and ultrafilters which you might find helpful.

[Callum Cassidy-Nolan]

Oh if l and l' are from the same neighborhood in Y and we know that f(a') = l' and f(a) = l then a and a' are from the same neighborhood in X and are therefore "close"?

[Callum Cassidy-Nolan]

Is that the right idea?

[Adam Topaz]

https://xenaproject.wordpress.com/2018/08/04/what-is-a-filter-how-some-computer-scientists-think-about-limits/

[Jake Levinson]

Some of this discussion seems not necessarily specific to filters. @Callum Cassidy-Nolan are you familiar with the topological definition of continuity?

[Jake Levinson]

(i.e. preimages of open sets are open)

[Callum Cassidy-Nolan]

I know the definition, but I think I have a hard time understanding it

[Kevin Buzzard]

https://xenaproject.wordpress.com/2021/02/18/formalising-mathematics-workshop-5-filters/ is newer but I don't say much about limits

[Callum Cassidy-Nolan]

Maybe I'll try to show it's equivalent to the epsilon delta definition to try and understand the idea more ...

[Jake Levinson]

For example -- Munkres's Intro to Topology textbook, Theorem 18.1(4), shows that the statement "f is continuous at x" is equivalent to "for all neighborhoods V of f(x), there is a neighborhood U of x such that f(U) \subseteq V (equivalently f^{-1}(V) contains U)". The latter is the epsilon-delta definition of continuity.

[Kevin Buzzard]

In that latter post I argue that a filter on X is a generalisation of a subset of X. If X is a topological space then the neighborhood filter of a point x in X is like an infinitesimally small subset of X containing x and a tiny bit more, not enough to contain any other points of X but enough to remember that you have some wiggle room. A function f : X -> Y being continuous at x means that the preimage of the infinitesimal neighborhood of f(x) contains the infinitesimal neighborhood of x. Callum you seem to be focussed on the other things it contains but that's not the right way to think about it. I don't care what's happening a long way from x.

[Jake Levinson]

You might also find it instructive to see why a simple discontinuous function, e.g. the sign function f(x) = sign(x), fails both definitions of continuity (in this case at x=0).

[Kevin Buzzard]

Another way to think of continuity is via images not preimages (there's a Galois connection going on so there are two equivalent definitions of a filter tending to another filter along a function). The pushforward way to say it is that f is continuous at x iff the image of the infinitesimal neighborhood of x is contained in the infinitesimal neighborhood of y. This way makes it clear that elements of X far from x have nothing to do with it

[Callum Cassidy-Nolan]

Ok, I'll keep reading about it and trying more examples

[Callum Cassidy-Nolan]

However, filters still have an ordering on them, written F ≤ G

Kevin, is that the same one as here?

image.png

[Kevin Buzzard]

Right, that's the two equivalent definitions of a filter on X tending to a filter on Y

[Kevin Buzzard]

The example I found terrifically helpful was the case of principal filters ie actual subsets of X

[Kevin Buzzard]

If A is a subset of X and B is a subset of Y then A tends to B along f iff f restricts to a function from A to B iff f(A) is a subset of B iff A is a subset of f-1(B)

[Kevin Buzzard]

And now imagine A is a small neighborhood of x and B is a small neighborhood of f(x) and you get the statement that moving x a tiny amount must only move f(x) a tiny amount, which is continuity

[Kevin Buzzard]

Note that it says nothing about what happens if you move x a large amount, which is what you were asking about