A study of adjunctions: Galois connections
Continuing 0015, here we look at what the isomorphisms give us in the important special case of preorder categories (whose objects are elements of a preorder and whose morphisms represent inequalities). The universal property of products specialises to the usual two-clause definition of greatest lower bounds: given elements $x$ and $y$ of a preorder, an element $x \sqcap y$ is a greatest lower bound of $x$ and $y$ exactly when
- $x \sqcap y$ is a lower bound of $x$ and $y$, that is, $x \sqcap y \leq x$ and $x \sqcap y \leq y$, and
- any lower bound of $x$ and $y$ is below $x \sqcap y$, that is, $z \leq x$ and $z \leq y$ implies $z \leq x \sqcap y$.
Categorically, the first clause assembles the object $x \sqcap y$ and the two morphisms $x \sqcap y \leq x$ and $x \sqcap y \leq y$ into a span object of a (derived) span category where we consider only lower bounds of $x$ and $y$ and the preorder restricted to these lower bounds, and the second clause says that this particular span is terminal, that is, $x \sqcap y$ is the greatest element in this derived preorder of lower bounds. On the other hand, the family of product isomorphisms specialises to
$$ \forall z.\ z \leq x \mathrel\wedge z \leq y ~\Leftrightarrow~ z \leq x \sqcap y $$
If $x \sqcap y$ exists for all $x$ and $y$, then we can make $(\sqcap)$ a function, and the above statement should hold for all $x$ and $y$:
$$ \forall x, y, z.\ z \leq x \mathrel\wedge z \leq y ~\Leftrightarrow~ z \leq x \sqcap y $$
Being equivalent to the universal property, this statement fixes $(\sqcap)$ up to isomorphism, so if the preorder is in fact a partial order (where isomorphism implies equality), this statement will serve as a definition of $(\sqcap)$. Being able to read and write such ‘isomorphisms’ intuitively can save us a lot of time. In this case, the function being defined is $(\sqcap)$, which is supposed to compute the greatest lower bound, an optimisation (greatest) with respect to a property (lower bound). The property is written on the left-hand side: $z \leq x \mathrel\wedge z \leq y$ says $z$ is a lower bound of $x$ and $y$. And since we want to find the greatest element satisfying the property, on the right-hand side we put the thing being defined, namely $x \sqcap y$, on the larger side of the inequality. Then the left-to-right implication says that any lower bound $z$ is below $x \sqcap y$, and by substituting $x \sqcap y$ for $z$, the right-to-left implication tells us that $x \sqcap y$ is a lower bound (since $(\leq)$ is reflexive).
It would be strange if whatever statement that looks like the one above always properly defined a function — we could have written some nonsense after all, in which case we couldn’t have defined anything. To make sure that we’re writing a sensible definition, we should ensure that the statement has the form
$$ \forall x : P, y : Q.\ f\ x \leq_Q y ~\Leftrightarrow~ x \leq_P g\ y $$
for some preorders $P$ and $Q$ and order-preserving functions $f : P \to Q$ and $g : Q \to P$; if $f$ satisfies certain conditions (which we will see in a later post), then $g$ will be properly defined. This specialises the general form of isomorphisms we caught a glimpse of at the end of 0015 to preorder categories, and is called a Galois connection.
Again, together with the technique of indirect reasoning, which specialises for partial orders to
$$ x = y \quad\Leftrightarrow\quad \forall z.\ z \leq x \Leftrightarrow z \leq y $$
we can reason about order-theoretic optimising definitions very easily. For example, reasoning about the floor function can be a pain without the help of the right Galois connection. In Section 3.2 of Graham, Knuth, and Patashnik’s Concrete Mathematics they use
$$ \left\lfloor \sqrt{\lfloor r \rfloor} \right\rfloor = \left\lfloor \sqrt{r} \right\rfloor \qquad\text{for real } r \geq 0 $$
as a first non-trivial property about floors. But if we characterise the floor function as finding the greatest integer below a real number,
$$ \forall n : \mathbb Z^{0+}, r : \mathbb R^{0+}. \mathsf{inj}\ n \leq_{\mathbb R^{0+}} r ~\Leftrightarrow~ n \leq_{\mathbb Z^{0+}} \lfloor r \rfloor $$
where $\mathsf{inj} : \mathbb Z^{0+} \to \mathbb R^{0+}$ promotes a non-negative integer to a non-negative real number (and will be omitted in the reasoning below), then the property becomes very easy to prove:
\begin{align*} & n \leq_{\mathbb Z^{0+}} \left\lfloor \sqrt{\lfloor r \rfloor} \right\rfloor \\ \Leftrightarrow~& \reason{Galois connection for floors} \\ & n \leq_{\mathbb R^{0+}} \sqrt{\lfloor r \rfloor} \\ \Leftrightarrow~& \reason{square root} \\ & n^2 \leq_{\mathbb R^{0+}} \lfloor r \rfloor \\ \Leftrightarrow~& \reason{both sides are integers} \\ & n^2 \leq_{\mathbb Z^{0+}} \lfloor r \rfloor \\ \Leftrightarrow~& \reason{Galois connection for floors} \\ & n^2 \leq_{\mathbb R^{0+}} r \\ \Leftrightarrow~& \reason{square root} \\ & n \leq_{\mathbb R^{0+}} \sqrt{r} \\ \Leftrightarrow~& \reason{Galois connection for floors} \\ & n \leq_{\mathbb Z^{0+}} \left\lfloor \sqrt{r} \right\rfloor \end{align*}
Similar to what we did with the commutativity of products in 0015, the crux of this reasoning is using the Galois connection to switch to the more liberal domain of real numbers to deal with the square root.
Next: 0017 (A study of adjunctions: Universality and natural isomorphism)
