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 there exists an
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:
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 is a collection of subsets of
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 is big. I guess the smallest filter on
would be the filter just containing
and the largest would be the one containing every subset of
, but I don’t think that either of these filters are particularly interesting. Here are some more interesting ones.
1) Principal filters. Choose and let
be the filter defined by
(i.e.
is big) iff
. In other words, we regard
as “the big element of
” and everything else as having size zero. Easy exercise: check this is a filter.
2) The cofinite filter. Let be an infinite set, and say that a subset
is big iff it only misses finitely many elements of
, i.e.
is finite. Such a
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 be a sequence of real numbers.
Definition 1. Say We say
(pronounced
tends to
) if for all
there exists
such that
.
Definition 2. We say if for all
there exists
such that
.
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 ). If
then define the filter of neighbourhoods of
by saying that a subset
is big iff there exists
such that
. If you’re happy with the lingo, you could say
is big iff
is in its interior. Easy check: this is a filter.
Definition (neighbourhood filter of ). Define the filter of neighbourhoods of
by saying that a subset
is big iff there exists
such that
. If you know how to compactify the reals by adding
you’ll see that we’re just looking at the filter of neighbourhoods of
in this compactified space and then removing
again.
Definition (unifying two definitions in first year analysis). Let be either a real number or
. We say a sequence
of reals tends to
iff for every
in the neighbourhood filter of
there exists some
such that
implies
.
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 is a general metric or topological space then we can define the neighbourhood filter of
to be all the subsets
such that
is in the interior of
, and the same definition works:
in the traditional sense taught to 2nd year undergraduates iff for every
in the filter, there exists
such that
.
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 is big iff there exists
such that the only elements missing are less than
. Put another way:
is big iff there exists
such that
. This kind of looks familiar — in fact I wrote that phrase about four times above. We should be able to use this somehow. Say
is a sequence of real numbers. We can think of the sequence as a map
sending
to
.
Definition Say or
. We say that
if for all
in the neighbourhood filter of
,
is in the cofinite filter on
.
This is just the same definition as before, rephrased using filters on both the source and the target of . It says that the pullback of the neighbourhood filter of
is contained in the cofinite filter on
. 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 , at the end of the day, for
a function, and filters
on
and
on
, we have
tendsto f L₁ L₂
if and only if for all
. Thinking about the case where
is a neighbourhood filter and
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.
Pingback: What is a uniform space? How some computer scientists think about completions. | Xena
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
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