nLab
net

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.

Definitions

A net ν\nu in a set XX is a directed set AA and a function ν:AX\nu: A \to X; we say that AA 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 ii is written ν i\nu_i. Indeed, an infinite sequence in XX is a net indexed by the natural numbers.

Although AA, 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 XX as a multi-valued function from a partially ordered directed set AA to XX. Although there is not much point to doing this in general, it can make a difference if you put restrictions on the possibilities for AA, 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).

Subnets

There are several different definitions of ‘subnet’ in the literature, all of which intend to generalise subsequences. We give them in order of increasing generality. Note that it is Definition 3 which is correct in that it corresponds precisely to refinement of filters. However, the other two definitions are sufficient (in a sense to be made precise at the end of this section) and may be easier to work with.

Given a net (x α)(x_{\alpha}) with index set AA, and a net (y β)(y_{\beta}) with an index set BB, we say that yy is a subnet of xx if:

Definition

(Willard, 1970).

We have a function f:BAf\colon B \to A such that

  • ff maps xx to yy (that is, for every βB\beta \in B, y β=x f(β)y_{\beta} = x_{f(\beta)});
  • ff is monotone (that is, for every β 1β 2B\beta_1 \geq \beta_2 \in B, f(β 1)f(β 2)f(\beta_1) \geq f(\beta_2));
  • ff is cofinal (that is, for every αA\alpha \in A there is a βB\beta \in B such that f(β)αf(\beta) \geq \alpha).
Definition

(Kelley, 1955).

We have a function f:BAf\colon B \to A such that

  • ff maps xx to yy (that is, for every βB\beta \in B, y β=x f(β)y_{\beta} = x_{f(\beta)});
  • ff is strongly cofinal (that is, for every αA\alpha \in A there is a βB\beta \in B such that, for every β 1βB\beta_1 \geq \beta \in B, f(β 1)αf(\beta_1) \geq \alpha).
Definition

(Smiley, 1957; Årnes & Andenæs, 1972).

The eventuality filter of yy (see below) refines the eventuality filter of xx. (Explicitly, for every αA\alpha \in A there is a βB\beta \in B such that, for every β 1βB\beta_1 \geq \beta \in B there is an α 1αA\alpha_1 \geq \alpha \in A such that y β 1=x α 1y_{\beta_1} = x_{\alpha_1}.)

The equivalence between these is as follows:

Theorem

(Schechter, 1996).

  1. If yy is a (1)-subnet of xx, then yy is also a (2)-subnet of xx, using the same function ff.
  2. If yy is a (2)-subnet of xx, then yy is also a (3)-subnet of xx.
  3. If yy is a (3)-subnet of xx, then there is some net zz such that
    • zz is equivalent to yy in the sense that yy and zz are (3)-subnets of each other, and
    • zz is a (1)-subnet of xx, using some function.

So from the perspective of definition (3), there are enough (1)-subnets and (2)-subnets, up to equivalence.

Logic of nets

A property of elements of XX (given by a subset SS of XX) can be applied to nets in XX.

Definition

We say that ν\nu is eventually in SS if for some index ii, ν jS\nu_j \in S for every jij \ge i. Dually, we say that ν\nu is frequently in SS if for every index ii, ν jS\nu_j \in S for some jij \ge i.

Remark

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.

Being eventually in SS, def. 4, is a weakening of being always in SS (given by Lawvere's universal quantifier ν\forall_\nu), while being frequently in SS is a strengthening of being sometime in SS (given by the particular quantifier ν\exists_\nu). Indeed we can build a formal logic out of these. Use essi,p[ν i]\ess\forall i, p[\nu_i] or ess νp\ess\forall_\nu p to mean that a predicate pp in XX is eventually true, and use essi,p[ν i]\ess\exists i, p[\nu_i] or ess νp\ess\exists_\nu p to mean that pp is frequently true. Then we have:

νpess νpess νp νp\forall_\nu p \;\Rightarrow\; \ess\forall_\nu p \;\Rightarrow\; \ess\exists_\nu p \;\Rightarrow\; \exists_\nu p
ess ν(pq)ess νpess νq\ess\forall_\nu (p \wedge q) \;\Leftrightarrow\; \ess\forall_\nu p \wedge \ess\forall_\nu q
ess ν(pq)ess νpess νq\ess\exists_\nu (p \wedge q) \;\Rightarrow\; \ess\exists_\nu p \wedge \ess\exists_\nu q
ess ν(pq)ess νpess νq\ess\forall_\nu (p \vee q) \;\Leftarrow\; \ess\forall_\nu p \wedge \ess\forall_\nu q
ess ν(pq)ess νpess νq\ess\exists_\nu (p \vee q) \;\Leftrightarrow\; \ess\exists_\nu p \vee \ess\exists_\nu q
ess ν¬p¬ess νp\ess\forall_\nu \neg{p} \;\Leftrightarrow\; \neg\ess\exists_\nu p

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 (‘not almost nowhere’ or ‘somewhere significant’) in measure spaces.

Nets and filters

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

Conversely, any filter \mathcal{F} defines a net whose eventuality filter is \mathcal{F}. Let AA be the disjoint union of \mathcal{F}; that is, an element of AA is of the form (U,x)(U,x), where xUx \in U \in \mathcal{F}. Define (U,x)(V,y)(U,x) \geq (V,y) iff UVU \subseteq V (regardless of xx and yy). Since \mathcal{F} is a filter, one can show that AA is a directed set (one needs here that \mathcal{F} is proper). Define ν(U,x)\nu(U,x) to be xx; then ν\nu is a net in XX whose eventuality filter is \mathcal{F} again. (It is actually enough to use only a base of the filter when defining AA.)

Nets are considered equivalent if they have the same eventuality filter; in other words, they are both subnets of each other. 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 xx in the space if, given any neighbourhood UU of xx, ν\nu is eventually in UU (def. 4); ν\nu clusters at xx if, for every neighbourhood UU of xx, ν\nu is frequently in UU (also def. 4). One can in fact recover the topology on the set XX 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 XX), 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 XX is small (not a proper class).

References

  • HAF, Sections 7.14–7.21

Revised on July 18, 2014 01:06:05 by Toby Bartels (98.16.169.210)