9
$\begingroup$

Recall that a filter on a set $X$ is a nonempty collection $\mathcal{F}$ of subsets of $X$ such that

(i) $U\subseteq V\subseteq X$ and $U\in\mathcal{F}$ implies $V\in\mathcal{F}$, and

(ii) $U,V\in\mathcal{F}$ implies $U\cap V\in\mathcal{F}$.

As far as I know, this definition was introduced by Bourbaki in "Topologie Generale", chapter 1 section 6 (the section is called "Filtres", and they furthermore demand that $\mathcal{F}$ does not contain the empty set, which I think nowadays some authors allow and some do not).

I'm giving a talk about filters to some 1st year undergraduates tomorrow, explaining how several distinct notions they've learnt in their course on sequences, series and continuity this term are special cases of the concept of a filter tending to a filter along a map. Let me explain this simple concept first, and then give examples of how it's used in the course.

If $\mathcal{F}$ is a filter on $X$ and $\mathcal{G}$ is a filter on $Y$, and $\phi:X\to Y$ is a map, then let's write $\mathcal{F}\rightarrow^\phi\mathcal{G}$ if for all $U\in\mathcal{G}$, we have $\phi^{-1}(U)\in\mathcal{F}$.

Examples:

1) if $C$ is the cofinite filter on $\mathbb{N}$ consisting of all sets with finite complement, if $\ell\in\mathbb{R}$ and $N(\ell)$ is the neighbourhood filter on $\mathbb{R}$, consisting of all sets whose interior contains $\ell$, and if $a:\mathbb{N}\to\mathbb{R}$ is a sequence, then the limit as $n\to\infty$ of $a(n)$ is $\ell$ iff $C\to^aN(\ell)$.

2) If $C$ is as above, and $N(\infty)$ is the filter on $\mathbb{R}$ is the filter of subsets containing $[B,\infty)$ for some $B\in\mathbb{R}$, then $a(n)\to\infty$ iff $C\to^aN(\infty)$.

3) If $f:\mathbb{R}\to\mathbb{R}$ then $N(x)\to^fN(f(x))$ iff $f$ is continuous at $x$.

So there's a proof that this is clearly a useful and standard idea. Ok now here's the stupid thing. I made up that notation $\mathcal{F}\to^\phi\mathcal{G}$ just now, because I actually learnt about this concept from the maths library of the Lean theorem prover , where it is called tendsto φ ℱ 𝒢. This is very computer-sciency notation, so I went to the maths literature to find out what Bourbaki call this notion -- and I couldn't find it in there. Bourbaki talk about a filter tending to a limit on a topologcal space but this is a more specialised notion. I looked at some more topology books and couldn't find it there either. So then I asked the computer scientists who wrote this part of the maths library where it came from, and they told me that basically they made it up themselves, and they presumed it was in the maths literature but they didn't know where. They wanted to make pairs $(X,\mathcal{F})$ the objects of a category, and this is what they came up with for the morphisms.

The earliest reference I have to the concept is the definition from the Isabelle theorem prover, written by Johannes Hoelzl in November 2012.

This is surely a standard notion in the mathematical literature, but I can't find it. Where is it, and what is the notation we use for it?

Improve this question
$\endgroup$
1
  • $\begingroup$ I suppose I am mentioning something you know very well, but I will just point out that the cases where $\mathcal F$ is the system of all neighborhoods of a given point (your examples 1 and 2) are simply convergence of the function $\phi$ w.r.t. the filter $\mathcal G$. You can find a bit more here: Where has this common generalization of nets and filters been written down? $\endgroup$
    – Martin Sleziak
    Commented Mar 24, 2019 at 16:54

1 Answer 1

Reset to default
5
$\begingroup$

The category that you are referring to is the category $\mathcal{F}$ in the paper 1.

The paper 1 also introduces another category $\mathcal{G}$ which is the quotient category $\mathcal{F}/\simeq$ category of $\mathcal{F}$ where if $f,g:(X,F)\rightarrow (Y,G)$ are morphisms in $\mathcal{F}$, then $f\simeq g$ precisely when $\{x\in X\mid f(x)=g(x)\}\in F$.

The category $\mathcal{G}$ is a more satisfactory notion of what should be meant as the category of filters since the category $\mathcal{G}$ is precisely the full subcategory of $\mathbf{Pro-Set}$ (the pro-completion of the category of all sets) consisting of all inverse systems with injective transitional mappings.

Two closed categories of filters. Andreas Blass. Fundamenta Mathematicae (1977) Volume: 94, Issue: 2, page 129-143. ISSN: 0016-2736

Improve this answer
$\endgroup$
6
  • $\begingroup$ Yes, this is the one! In the definition in the original Lean code there is $\le$ and in the paper there is $\supseteq$, but these are the same thing because the partial order on filters is defined this way (the more sets there are, the smaller the "limit" is). Unfortunately I still don't see notation, because Blass defines the category and then just refers to the arrows as morphisms or $\mathcal{F}$-morphisms :-) $\endgroup$
    – Kevin Buzzard
    Commented Mar 11, 2019 at 22:52
  • 2
    $\begingroup$ And I still don't have a good name for these morphisms. What does exist, though I apparently didn't know about it when I wrote that paper, is a standard terminology for "there exists a morphism from $F$ to $G$"; this is the Katetov ordering of filters, written $F\geq_KG$. (Its specialization to ultrafilters is called the Rudin-Keisler ordering.) So one could express "tendsto $\phi F G$" by "$\phi$ witnesses that $F\geq_KG$"; I would not, however, recommend expressing it this way, especially in an introductory talk. $\endgroup$
    – Andreas Blass
    Commented Mar 11, 2019 at 23:44
  • $\begingroup$ This reference still doesn't seem to cover the main use of this idea, because it doesn't fix the underlying set. Say you want to prove that limits compose (limits of sequences, of function at a point, at infinity, from the left or right, all in one proof...). With Kevin notations, it means for all $f: X\to Y$, $g : Y \to Z$, and filters $F$, $G$, $H$ on $X$, $Y$ and $Z$, $F\to^f G$ and $G \to^g H$ implies $F \to^{g\circ f} H$. Here you need that $X \mapsto Filter(X)$ is a functor from $\mathbf{Set}$ to the category of posets. I'd like to know a reference for this observation. $\endgroup$
    – Patrick Massot
    Commented Mar 12, 2019 at 7:45
  • $\begingroup$ @PatrickMassot If you mean a reference for the filter functor: this has been known essentially forever, but here is one (which characterizes the algebras of the filter monad as continuous lattices): books.google.com/… $\endgroup$
    – Todd Trimble
    Commented Mar 12, 2019 at 13:28
  • $\begingroup$ @ToddTrimble this is an interesting paper, but it makes to reference to limits. I'm looking for a source which explicitly says: you can compose many kinds of limits using the filter functor. $\endgroup$
    – Patrick Massot
    Commented Mar 13, 2019 at 21:46

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .