Are nets and filters useful in geometry and topology? Many results in topology can be restated using the concepts of nets and ultrafilters. This seems to be of interest for set theorists, maybe even logicians. But for geometers and topologists, those who use point-set topology only as a tool in proving theorems about manifolds, varieties, schemes, homology groups, etc, can this reformulation be useful? If it is, please give examples of how it might be used.
In the case of Tychonoff's Theorem, it may provide an interesting way to prove a result in point-set topology which is useful for geometers, but even in this case, its use does not seem to shed much insight once one has obtained the technical point-set result.
 A: A few years ago de Fernex and Mustata used ultrafilters to prove some results on log canonical thresholds related to Shokurov's ACC conjecture.  See deFernexMustata07.
However, shortly after, Koll'ar proved the same results using more geometric methods, see Kollar08 (making this a non-example in some people's mind).
I probably should also mention the work of Hans Schoutens using ultra filters to construct ultra-Frobenius (Frobenius in characteristic zero) and thus detect various types of singularities in characteristic zero.
A: If a topological space is not first countable sequences can not be used for instance to verify the continuity of the function. In that case you can use nets instead. Topological spaces which are not first countable are commonly encountered in Functional Analysis.
A: I am not sure if this is the type of answer you are looking for, but, representing topological spaces by their ultrafilter convergence relation is quite useful for determining which topological spaces are exponentiable.
A: Nets were first expounded by Moore and Smith in order to explain the convergence involved in the definition of the Riemann integral.  Would you say that is of no use in geometry and topology?
A: Those in functional analysis should read the book Beattie R, Butzmann H P : Convergence Structures and Applications to Functional Analysis. Kluwer, Dordrecht, 2002, and see how incredibly useful is to get beyond the Hausdorff-Kuratowski-Bourbaki topology, that is, the usual topology. And the issue is not whether one uses sequences, nets, filters, or whatever else. No the issue is simply how one uses them. And with the rather slight relaxation of the concept of usual topology in the above book, one can do miracles. Among them, the duality theory of locally convex vector spaces becomes so clear and simple.
A: In formalised mathematics, Lean's mathlib library uses filters extensively when developing the basic theory of topological spaces.  I do not know exactly why that decision was taken.  However, when a non-traditional formulation turns out to be more convenient for formalisation, it is often worth asking whether that formulation has advantages in other contexts as well.
A: If I recall correctly ultra-filters were used to prove Tychonoff's Theorem in Willards' General Topology book.
A: Although this isn't geometry or topology, this thread gives an application of ultrafilters to field theory. I think this still counts as an application of ultrafilters outside of the fields in which they might normally appear.
A: I think the net formulation is quite useful to know, at least. Analysts seem to be most fond of it, as they naturally work with sequences anyway. E.g. on easily shows that the closure of a subgroup $H$ in a topological group $G$ is a subgroup: just note that for $x,y$ in closure of $H$, we find nets (wlog with the same index set) $(x_i), (y_i)$ from $H$ that converge to $x$, resp. $y$, and then $x_i \cdot {y_i}^{-1} \rightarrow x \cdot y^{-1}$ from continuity of the group operations, and the left hand side lives in $H$, so the right hand side is in closure H, and this is thus a subgroup. 
Similarly, $A \cdot B$ is closed in $G$ when $A$ is closed and $B$ is compact: take a net $(x_i \cdot y_i)_{i \in I}$ in $A \cdot B$ converging to $z$. By compactness the net $(y_i)$ has a subnet converging to $y \in B$, indexed by $J$ say, and then the corresponding subnet $x_j = x_j \cdot y_j \cdot y_j^{-1}$ converges to $z \cdot y^{-1}$ and as the $(x_j)$ are in $A$, so is the limit $z \cdot y^{-1}$ and so $z = (z \cdot y^{-1} \cdot y)$ is in $A \cdot B$, making it closed.
Nets also make for a nice formulation of the Riemann integral (using partitions on the interval as a directed set under refinement) as a limit of a certain net. Some proofs just look more "natural" in a net formulation, I think. One can do the proof for sequences first, and see how it generalizes using nets. 
A: One of the most important constructions in geometric group theory is the asymptotic cone of a group or metric space, which captures what happens to the group or metric space as you rescale the metric down to zero (or, less formally, as you squint your eyes and move farther and farther away from the space).  The originated in Gromov's original proof of his  polynomial growth theorem, where the polynomial growth condition assures that this limit exists in the classical sense.  However, since then this concept has been hugely important in more general situations where one has to use an ultrafilter to define an appropriate notion of convergence.  I recommend perusing the wikipedia articles on
Gromov-Hausdorff convergence and ultralimits.
A: Nets (and also filters) allow one to unify the wide morass of convergence notions. There is even an undergraduate introduction to analysis based on nets, Limits by Alan Beardon.
Notions like the convergence of sets (the liminf and limsup of sets stuff) can be formulated as a nontopological form of order convergence based on nets. These notions play an important part in general measure theory and especially in probability theory.
Kolmogorov's extension theorem of stochastic processes has abstract generalizations based on nets of $\sigma$-algebras. See for example here (Wayback Machine).
Ultrafilters play a surprising role in social choice theory. The family of "pivotal sets of voters" implied by a social decision rule satisfying the assumption of Arrow's impossibility theorem forms an ultrafilter, which explains why all such rules are dictatorial with finitely many voters but not in the case of infinitely many voters.
For an actual application of ultrafilters in geometry, see this post on Terry Tao's blog.
