Formalising Mathematics : workshop 5 — filters

The word “filter” means different things to different people; just to clarify, this week we’ll be learning about the mathematical notion of a filter on a set. I’ve written about these filters before, but since then I’ve managed to pick up a much better understanding of how to think about filters, and I hope this shows here. When I wrote that post in 2018 I knew that filters were “something to do with limits”, but now I realise that this is wrong. They are used to talk about limits, but what a filter itself is, is simply a generalisation of a subset of a set.

What is a filter?

Let X be a type, i.e. what most mathematicians call a set. Then X has subsets, and the collection of all subsets of X has some really nice properties — you can take arbitrary unions and intersections, for example, and if you order subsets of X by inclusion then these constructions can be thought of as sups and infs and satisfy a bunch of axioms which one might expect sups and infs to satisfy, for example if X_i\subseteq Y for all i in an index set then \bigcup_i X_i \subseteq Y. In short, the subsets of a set form what is known in order theory as a complete lattice.

A filter can be thought of as a kind of generalised subset of X. Every subset S of X gives rise to a filter on X, called the principal filter π“Ÿ S associated to S, and we have π“Ÿ S = π“Ÿ T if and only if S = T. However if X is infinite then there are other, nonprincipal, filters F on X, which are slightly vaguer objects. However, filters still have an ordering on them, written F ≀ G, and it is true that S βŠ† T ↔ π“Ÿ S ≀ π“Ÿ T (indeed we’ll be proving this today). To give an example of a filter which is not principal, let’s let X be the real numbers. Then for a real number x there is a filter 𝓝 x, called the neighbourhood filter of x, with the property that if U is any open subset of \mathbb{R} containing x then π“Ÿ {x} < 𝓝 x < π“Ÿ U. In other words, 𝓝 x is some kind of “infinitesimal neighbourhood of x“, strictly bigger than {x} but strictly smaller than every open neighbourhood of x. This is a concept which cannot be formalised using sets alone, but can be formalised using filters.

The formal definition of a filter.

Let me motivate the definition before I give it. Say F is a filter. Let’s define F.sets to be the subsets of X which contain F, i.e., the S such that F ≀ π“Ÿ S . Here is a property of filters which I have not yet mentioned: If two filters F and G satisfy F.sets = G.sets, then F = G; in other words, a filter is determined by the principal filters which contain it. This motivates the following definition: why not define a filter F to be the set of subsets of X which contain it? We will need some axioms — what are reasonable axioms? We don’t want a filter to be bigger than X itself, and we want to make sure that if S contains F then T contains F for any T βŠ‡ S; finally if both S and T contain F then we want S ∩ T to contain F. That’s the definition of a filter!

structure filter (Ξ± : Type*) :=
(sets                   : set (set Ξ±))
(univ_sets              : set.univ ∈ sets)
(sets_of_superset {x y} : x ∈ sets β†’ x βŠ† y β†’ y ∈ sets)
(inter_sets {x y}       : x ∈ sets β†’ y ∈ sets β†’ x ∩ y ∈ sets)

A filter on X, or, as Lean would like to call it, a term F : filter X of type filter X, is a collection F.sets of subsets of X satisfying the three axioms mentioned above. That’s it. Unravelling the definitions, we see that a sensible definition of F ≀ G is that G.sets βŠ† F.sets, because we want G βŠ† S to imply F βŠ† S (or, more precisely, we want G ≀ π“Ÿ S to imply F ≀ π“Ÿ S).

It’s probably finally worth mentioning that in Bourbaki, where this concept was first introduced, they have an extra axiom on their filters — they do not allow π“Ÿ βˆ… to be a filter — the empty set is not a generalised set. In this optic this looks like a very strange decision, and this extra axiom was dropped in Lean. Indeed, we bless π“Ÿ βˆ… with a special name — it is βŠ₯, the unique smallest filter under our ≀ ordering. The (small) advantage of the Bourbaki convention is that an ultrafilter can be defined to literally be a minimal element in the type of all filters, rather than a minimal element in the type of all filters other than βŠ₯. This would be analogous to not allowing a ring R to be an ideal of itself, so one can define maximal ideals of a ring to be the maximal elements in the set of all ideals of the ring. However this convention for ideals would hugely break the functoriality of ideals, for example the image of an ideal along a ring homomorphism might not be an ideal any more, the sum of two ideals might not be an ideal, and so on. Similarly, we allow βŠ₯ to be a filter in Lean, because it enables us to take the intersection of filters, pull filters back and so on — it gives a far more functorial definition.

What’s in today’s workshop?

The material this week is in week_5 of the formalising-mathematics GitHub repo which you can download locally if you have leanproject installed or, if you have the patience of a saint and don’t mind missing some of the bells and whistles, you can try online (Part A, and Part B). NB all this infrastructure didn’t just appear by magic, I wrote the code in the repo but I had nothing to do with all these other tricks to make it easier for mathematicians to use — we have a lot to thank people like Patrick Massot and Bryan Gin-ge Chen for.

In Part A we start by defining principal filters and we make a basic API for them. I give a couple more examples of filters too, for example the cofinite filter C on X, which is all the subsets of X whose complement is finite. This filter is worth dwelling on. It corresponds to a generic “every element of X apart from perhaps finitely many” subset of X, perhaps analogous to a generic point in algebraic geometry. However, there exists no element a of X such that π“Ÿ {a} ≀ C, because X - {a} is a cofinite subset not containing a. In particular, thinking of filters as generalised subsets again, we note that whilst a generalised set is determined by the sets containing it, it is definitely not determined by the sets it contains: indeed, C contains no nonempty sets at all.

In Part B we go on to do some topology. We define neighbourhood filters and cluster points, and then talk about a definition of compactness which doesn’t involve open sets at all, but instead involves filters. I am still trying to internalise this definition, which is the following:

def is_compact (S : set X) := βˆ€ ⦃F⦄ [ne_bot F], F ≀ π“Ÿ S β†’ βˆƒ a  ∈ S, cluster_pt a F

In words, a subset S of a topological space is compact if every generalised non-empty subset F of S has closure containing a point of S.

Let’s think about an example here. Let’s stick to S = X. Say S is an infinite discrete topological space. Then the cofinite filter is a filter on S which has no cluster points at all, meaning that an infinite discrete topological space is not compact. Similarly imagine S is the semi-open interval (0,1]. Then the filter of neighbourhoods of zero in \mathbb{R}, restricted to this subset (i.e. just intersect all the sets in the filter with (0,1]), again has no cluster points, so this space is not compact either. Finally let’s consider \mathbb{R} itself. Then the at_top filter, which we will think about in Part A, consists of all subsets T of \mathbb{R} for which there exists some r\in\mathbb{R} such that (r,\infty)\subseteq T. This “neighbourhood of +\infty” filter has no cluster points in \mathbb{R} (note that +\infty would be a cluster point, but it’s not a real number). Hence \mathbb{R} is not compact either. We have certainly not proved here that this definition of compact is mathematically equivalent to the usual one, but it is, and if you’re interested, and you’ve learnt Lean’s language, you can just go and read the proof for yourself in Lean’s maths library.

The boss level this week is, again, that a closed subspace of a compact space is compact. But this time we prove it with filters. As last time, we prove something slightly more general: if X is any topological space, and if S is a compact subset and C is a closed subset, then S ∩ C is compact. Here’s the proof. Say F is a nonempty generalised subset (i.e. a filter) contained in S ∩ C. By compactness of S, F has a cluster point a in S. But F is contained in C, so all cluster points of F are cluster points of C, and the cluster points of C are just the closure of C, which is C again. Hence a is the element of S ∩ C which we seek. No covers, no finite subcovers.


About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in formalising mathematics course, Imperial, undergrad maths and tagged , . Bookmark the permalink.

5 Responses to Formalising Mathematics : workshop 5 — filters

  1. Apurva says:

    What’s the benefit of using filters in Lean? Many point-set topology textbooks (or algebraic topology textbooks for that matter) do not even mention the word filter. Is it possible to do topology in Lean while completely avoiding filters? I once tried reading the API for a topological space but got lost pretty soon because I could not translate the theorems I saw there into point-set topology theorems.

    Liked by 1 person

    • xenaproject says:

      Oh sure you can do it without filters. It’s just that it seems easier to use filters. Proofs which use open sets often contain auxiliary constructions — “now let’s construct this open cover, prove it’s a cover and take a finite subcover”. With filters it is easier to argue backwards, which means that proofs can be more easily turned into functions.

      Liked by 1 person

  2. Xi Wu says:

    There seems to be a typo after the lean definition of filter, it should be “G \le S” (order two filters,
    where G is a finer filter in the sense that S.sets \subset G.sets), implying “F \le S”?

    Liked by 1 person

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s