Contents

Idea

Nets are generalisations of sequences that are used especially in topology. They are also called Moore–Smith sequences and are equivalent (in a certain sense) to proper filters.

Definition

A net $\nu$ in a set $X$ is a directed set $A$ and a function $\nu :A\to X$; we say that $A$ indexes the net. The notation used is based on the special case of an infinite sequence; the value of the function $\nu$ at the index $i$ is written ${\nu }_i$. Indeed, an infinite sequence in $X$ is a net indexed by the natural numbers.

Although $A$, being a directed set, is equipped with a preorder, the net is not required to preserve this in any way. This forms an exception to the rule of thumb that a preordered set may be replaced by its quotient poset. You can get around this if you instead define a net in $X$ as a multi-valued function from a partially ordered directed set $A$ to $X$. Although there is not much point to doing this in general, it can make a difference if you put restrictions on the possibilities for $A$, in particular if you consider the definition of sequence. In some type-theoretic foundations of mathematics, you can get the same effect by defining a net to be an ‘operation’ (a prefunction, like a function but not required to preserve equality).

Subnet

Given a net $(x_{\alpha })$ with index set $A$, a subnet is a net $(y_{\beta })$ with an index set $B$ and a monotone function

such that

and which is cofinal: for every $\alpha \in A$ there is a $\beta \in B$ such that $f(\beta )\ge \alpha$.

Logic of nets

A property of elements of $X$ (given by a subset $S$ of $X$) can be applied to nets in $X$. We say that $\nu$ is eventually in $S$ if for some index $i$, ${\nu }_j\in S$ for every $j\ge i$. Dually, we say that $\nu$ is frequently in $S$ if for every index $i$, ${\nu }_j\in S$ for some $j\ge i$. Sometimes one says ‘infinitely often’ in place of ‘frequently’ and even ‘cofinitely often’ in place of ‘eventually’; these derive from the special case of sequences, where they may be taken literally.

Note that being eventually in $S$ is a weakening of being always in $S$ (given by Lawvere's universal quantifier ${\forall }_{\nu }$), while being frequently in $S$ is a strenghtening of being sometime in $S$ (given by the particular quantifier ${\exists }_{\nu }$). Indeed we can build a logic out of these. Use $ess\forall i,p[{\nu }_i]$ or $ess{\forall }_{\nu }p$ to mean that a predicate $p$ in $X$ is eventually true, and use $ess\exists i,p[{\nu }_i]$ or $ess{\exists }_{\nu }p$ to mean that $p$ is frequently true. Then we have:

and other analogues of theorems from predicate logic. Note that the last item listed requires excluded middle even though its analogue from ordinary predicate logic does not.

A similar logic is satisfied by ‘almost everywhere’ and its dual in measure spaces.

Nets and filters

A net $\nu$ in a set $X$ defines a proper filter of subsets of $X$, called the eventuality filter of the net. It consists simply of those subsets of $X$ that $\nu$ is eventually in. (Recall that a filter of subsets is a family of subsets that is closed under intersection and taking supersets; the filter is proper if each set in it is inhabited.)

Conversely, any filter $ℱ$ defines a net whose eventuality filter is $ℱ$. Let $A$ be the disjoint union of $ℱ$; that is, an element of $A$ is of the form $(U,x)$, where $x\in U\in ℱ$. Define $(U,x)\ge (V,y)$ iff $U\subseteq V$ (regardless of $x$ and $y$). Since $ℱ$ is a filter, one can show that $A$ is a directed set (one needs here that $ℱ$ is proper). Define $\nu (U,x)$ to be $x$; then $\nu$ is a net in $X$ whose eventuality filter is $ℱ$ again. (It is actually enough to use only a base of the filter when defining $A$.)

Nets are considered equivalent if they have the same eventuality filter; in particular, they define the same logical quantifiers and are therefore equivalent for the application to topology below. Of course, it is possible to distinguish them by using the standard logical quantifiers instead.

Nets in topological spaces

A net $\nu$ in a topological space converges to a point $x$ in the space if, given any neighbourhood $U$ of $x$, $\nu$ is eventually in $U$; $\nu$ clusters at $x$ if, for every neighbourhood $U$ of $x$, $\nu$ is frequently in $U$. One can in fact recover the topology on the set $X$ simply by knowing which nets converge to which points. It is possible to define elementary conditions on this convergence relation that characterise whether it is topological (that is whether it comes from a topology on $X$), although these are a bit complicated.

By keeping only the simple conditions, one gets the definition of a convergence space; this is a more general concept than a topological space and includes many non-topological situations where we want to say that a sequence converges to some value (such as convergence in measure). It is also very nice to describe compact and Hausdorff spaces in terms of the convergence relation.

Although nets are perhaps more familiar, due to their similarity to sequences, one gets a cleaner theory by talking about filters, since equivalent filters are equal and (as long as one is not a predicativist) the set of filters on a set $X$ is small (not a proper class).