Ultrafilter functor (source code)

= Ultrafilter functor
{title2=$\mathcal U$}

The ultrafilter functor sends a set $A$ to its set $\mathcal U(A)$ of ultrafilters. A function $f:A\to B$ acts by pushforward,
$$
f_*U=\{C\subseteq B:f^{-1}(C)\in U\}.
$$
It preserves finite coproducts: an ultrafilter on $A\sqcup B$ contains exactly one summand and is uniquely induced by an ultrafilter on that summand.