Adjoint Functor Theorem for Preorders

theorem proof

Theorem 1.115. Suppose $Q$ is a Preorder that has all meets and let $P$ be any preorder. A Monotone Map $g:Q\to P$ preserves meets if and only if it is a right adjoint (of a Galois Connection). Similarly, if $P$ has all joins and $Q$ is any preorder, a monotone $f:P\to Q$ preserves joins iff it is a left adjoint.

Sources: 7 Sketches Theorem 1.115; DaoFP §10.8 (“Freyd’s theorem in a preorder”, “Solution set condition”); general version: Adjoint Functor Theorem.

Proof (meets). One direction is Right Adjoints Preserve Meets. Conversely suppose $g$ preserves meets. Define the candidate left adjoint by

$$f(p):=\bigwedge \{q\in Q\mid p\le g(q)\},(1.116)$$

which exists because $Q$ has all meets. Monotone: if $p\le p^{\prime }$ then $\{q^{\prime }\mid p^{\prime }\le g(q^{\prime })\}\subseteq \{q\mid p\le g(q)\}$, so by Proposition 1.91 (Meet) $f(p)\le f(p^{\prime })$. By Proposition 1.107 it suffices to show $p_0\le g(f(p_0))$ and $f(g(q_0))\le q_0$. For the first,

$$p_0\le \bigwedge \{g(q)\mid p_0\le g(q)\}\cong g(\bigwedge \{q\mid p_0\le g(q)\})=g(f(p_0)),$$

where the inequality holds because $p_0$ is below every element of the set, and the isomorphism is meet-preservation. For the second, $\{q_0\}\subseteq \{q\mid g(q_0)\le g(q)\}$, so

$$f(g(q_0))=\bigwedge \{q\mid g(q_0)\le g(q)\}\le \bigwedge \{q_0\}=q_0.■$$

DaoFP’s view (§10.8). In a preorder a left adjoint $f$ to $g$ must satisfy $f(p)=\bigwedge \{q\mid p\le g(q)\}$ — the limit of the comma category $p\downarrow g$. Freyd’s theorem says that for general categories the same formula works provided $\mathcal{C}$ is complete, $g$ preserves limits, and a solution set condition holds guaranteeing the limit is over a small diagram; in a preorder with all meets the condition is automatic. Applied to Defunctionalization: DaoFP uses the theorem to explain why arbitrary functions can be replaced by a “solution set” of data.

The theorem explains the slogan: a monotone map does not have generative effects iff it is a left adjoint.

LeanHaskell

-- Mathlib: complete lattices, Galois connections and the ingredients of (1.116)
#check @GaloisConnection
#check @GaloisConnection.u_sInf     -- right adjoints preserve all meets
#check @sInf_le                     -- used to show f(g q₀) ≤ q₀
-- The candidate left adjoint (1.116):
def leftAdjCandidate {P Q : Type} [Preorder P] [CompleteLattice Q] (g : Q → P) (p : P) : Q :=
  sInf {q | p ≤ g q}

-- (1.116) on finite preorders: build the left adjoint from a meet-preserving g
leftAdjoint :: (Preorder p, Preorder q) => [q] -> (q -> p) -> p -> Maybe q
leftAdjoint qs g p = meet qs [q | q <- qs, leq p (g q)]