What is a filter? How some computer scientists think about limits.

This is post 1 of 2 posts both of which are attempts to explain some basic mathematical definitions which I have never seen covered in a mathematics course. This one is on filters, and the next one will be on uniform spaces. I will be brief — I just want to say enough so that people who are interested in understanding how Lean does limits (this post) and completions (the next post) can actually attempt to engage with the Lean code in mathlib about these ideas, without being completely intimidated.

OK so let’s start with limits. Guillermo Barajas Ayuso was trying to figure out where exactly in mathlib it said that a sequence of real numbers was Cauchy iff it converged. This is a pretty fundamental fact about the real numbers, but if you dig far enough then you discover that the definition of tendsto is in mathlib’s order/filter.lean and it says


/-- `tendsto` is the generic "limit of a function" predicate.
  `tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
  the `f`-preimage of `a` is an `l₁` neighborhood. -/
def tendsto (f : α → β) (l₁ : filter α) (l₂ : filter β) := l₁.map f ≤ l₂

Gaargh. Whatever does that mean? Why doesn’t it say that for all $\epsilon$ there exists an $N$ such that something or other?

What is happening here is that when you are building maths from nothing, it’s important to isolate key concepts and set them up in the correct generality, which is the maximal generality for which they make sense. We are trying to understand limits here. As a maths undergraduate I was introduced to the notion of a sequence tending to a limit three times. Firstly I was told what it meant for a sequence of real or complex numbers to tend to a limit. Then I was told what it meant for a sequence of elements of a metric space to tend to a limit. And finally I was told what it meant for a sequence of elements of a topological space to tend to a limit. Each of these definitions is more general than the one before. The real numbers are a metric space, and every metric space is a topological space. And of course, each new definition specialises to the one before. Note also that each time we generalised, we introduced a new mathematical concept — first metric spaces, and then topological spaces.

Well, it turns out that there are even more general definitions of what it means for something to tend to something, and before I can explain the next level of generality I need to introduce a new concept — that of a filter on a set (or, if you’re doing this in Lean, on a type).

What is a filter?

The relevant bit of Wikipedia is here:

Filter on a set

In Lean it looks like this:


structure filter (α : Type u) :=
(sets            : set (set α))
(exists_mem_sets : ∃x, x ∈ sets)
(upwards_sets    : ∀{x y}, x ∈ sets → x ⊆ y → y ∈ sets)
(directed_sets   : directed_on (⊆) sets)

So, like a topology on a set, a filter on a set $X$ is a collection of subsets of $X$ with some properties. The easiest way to think of the properties is to think of the sets in the filter as the “big” sets. The axioms for a filter then say: (1) there’s a big set. (2) Any set containing a big set is big and (3) the intersection of two big sets is big (I don’t quite know why mathlib chooses to express this third fact in such a fancy way, but there you go).

Note that (1) and (2) together imply that $X$ is big. I guess the smallest filter on $X$ would be the filter just containing $X$ and the largest would be the one containing every subset of $X$ , but I don’t think that either of these filters are particularly interesting. Here are some more interesting ones.

1) Principal filters. Choose $x\in X$ and let $F$ be the filter defined by $U\in F$ (i.e. $U$ is big) iff $x\in U$ . In other words, we regard $x$ as “the big element of $X$ ” and everything else as having size zero. Easy exercise: check this is a filter.

2) The cofinite filter. Let $X$ be an infinite set, and say that a subset $U \subseteq X$ is big iff it only misses finitely many elements of $X$ , i.e. $X\backslash U$ is finite. Such a $U$ is called cofinite (“complement is finite”) and it’s again an easy exercise to check that this is a filter.

Filters in action part I

I remember when I was a first year undergraduate being slightly annoyed by the following definitions.
Let $x_0,x_1,x_2,\ldots,x_n,\ldots$ be a sequence of real numbers.

Definition 1. Say $\ell\in\mathbb{R}.$ We say $(x_n)\to \ell$ (pronounced $(x_n)$ tends to $\ell$ ) if for all $\epsilon>0$ there exists $N=N(\epsilon)$ such that $n\geq N\implies |x_n-\ell|<\epsilon$ .

Definition 2. We say $(x_n)\to+\infty$ if for all $B\in\mathbb{R}$ there exists $N=N(B)$ such that $n\geq N\implies x_n>B$ .

It used to irk me a bit that there was no one definition which could specialise to these two cases, given that we were using the same notation and everything. Well, Mr my old first year analysis lecturer, you could have put me out of my misery by using filters!

Definition (neighbourhood filter of $\ell$ ). If $\ell\in\mathbb{R}$ then define the filter of neighbourhoods of $\ell$ by saying that a subset $U\subseteq\mathbb{R}$ is big iff there exists $\epsilon>0$ such that $(\ell-\epsilon,\ell+\epsilon)\subseteq U$ . If you’re happy with the lingo, you could say $U$ is big iff $\ell$ is in its interior. Easy check: this is a filter.

Definition (neighbourhood filter of $+\infty$ ). Define the filter of neighbourhoods of $+\infty$ by saying that a subset $U\subseteq\mathbb{R}$ is big iff there exists $B\in\mathbb{R}$ such that $(B,\infty)\subseteq U$ . If you know how to compactify the reals by adding $\pm\infty$ you’ll see that we’re just looking at the filter of neighbourhoods of $+\infty$ in this compactified space and then removing $\pm\infty$ again.

Definition (unifying two definitions in first year analysis). Let $\ell$ be either a real number or $+\infty$ . We say a sequence $(x_n)$ of reals tends to $\ell$ iff for every $U$ in the neighbourhood filter of $\ell$ there exists some $N=N(U)$ such that $n\geq N$ implies $x_n\in U$ .

The world is now a tidier place — the definitions have been unified using this notion of a filter.

If you’re happy with the lingo, you can see that if $X$ is a general metric or topological space then we can define the neighbourhood filter of $x\in X$ to be all the subsets $U$ such that $x$ is in the interior of $U$ , and the same definition works: $(x_n)\to x$ in the traditional sense taught to 2nd year undergraduates iff for every $U$ in the filter, there exists $N=N(U)$ such that $n\geq N\implies x_n\in U$ .

If you’ve not seen this before, you might think this is already pretty neat. But it gets even neater!

Filters in action Part II

Remember the cofinite filter on an infinite set? Let’s look at the cofinite filter on the naturals. Here a subset is big iff it is only missing finitely many naturals. Put it another way — a subset $U$ is big iff there exists $N=N(U)$ such that the only elements missing are less than $N$ . Put another way: $U$ is big iff there exists $N=N(U)$ such that $n\geq N\implies n\in U$ . This kind of looks familiar — in fact I wrote that phrase about four times above. We should be able to use this somehow. Say $(x_n)$ is a sequence of real numbers. We can think of the sequence as a map $f : \mathbb{N}\to\mathbb{R}$ sending $n$ to $x_n$ .

Definition Say $\ell\in\mathbb{R}$ or $\ell=+\infty$ . We say that $(x_n)\to\ell$ if for all $U$ in the neighbourhood filter of $\ell$ , $f^{-1}(U):=\{n\in\mathbb{N}\ |\ f(n)\in U\}$ is in the cofinite filter on $\mathbb{N}$ .

This is just the same definition as before, rephrased using filters on both the source and the target of $f$ . It says that the pullback of the neighbourhood filter of $\ell$ is contained in the cofinite filter on $\mathbb{N}$ . Now compare with this code in mathlib’s order/filter.lean:


lemma tendsto_def {f : α → β} {l₁ : filter α} {l₂ : filter β} :
  tendsto f l₁ l₂ ↔ ∀ s ∈ l₂.sets, f ⁻¹' s ∈ l₁.sets := iff.rfl

This lemma says that whilst the definition of tendsto above was a bit obscure involving map and perhaps a slightly subtle use of $\leq$ , at the end of the day, for $f : X\to Y$ a function, and filters $L_1$ on $X$ and $L_2$ on $Y$ , we have tendsto f L₁ L₂ if and only if $f^{-1}(U_2)\in L_1$ for all $U_2\in L_2$ . Thinking about the case where $L_2$ is a neighbourhood filter and $L_1$ a cofinite filter keeps us grounded in sanity, but this is an extremely general definition of something tending to something and when you’re involved in building something like mathlib, the more general you can go, the better. The philosophy is that each definition or lemma should be made or proved in the maximum generality for which it makes sense or is true, and we are seeing that here.

4 Responses to What is a filter? How some computer scientists think about limits.

Pingback: What is a uniform space? How some computer scientists think about completions. | Xena
Scott Morrison says:

August 5, 2018 at 10:39 pm

I’m actually not entirely on board with the philosophy as stated at the end. I think in an ideal mathematical library, we will have all of the definitions, at different levels of generality, stated separately, along with the theorems explaining the specialisations. Eventually it just becomes too cumbersome having to speak the most general language when you’re doing something easy, that could be said in a more specific language.

This means there is more work building the library (and even more work engineering smooth transitions between levels of generality when needed). Perhaps it won’t get done at first (e.g. here and now) but I hope we don’t forget the aspiration.

LikeLike

Scott Morrison says:

August 5, 2018 at 10:41 pm

As an example, in my category theory library, it would be a disaster if anytime you wanted to speak about the kernel of a map, you had to remember the words to use that allow you to think of kernels as special cases of limits. And it’s not hard to come up with more and more ridiculous examples!

(That all said, I appreciate the motivation for this post.)

LikeLike

Pingback: Formalising Mathematics : workshop 5 — filters | Xena