Galois Connection

definition example theorem proof

A Galois connection between preorders $P$ and $Q$ is a pair of monotone maps $f:P\to Q$ and $g:Q\to P$ such that

$$f(p)\le q\text{if and only if}p\le g(q)(1.96)$$

for all $p\in P$, $q\in Q$. We say $f$ is the left adjoint and $g$ the right adjoint, and write $f⊣g$. Galois connections were first considered by Galois (field extensions vs. automorphism groups); they are the preorder case of adjunctions, and a “relaxed version” of isomorphisms.

Sources: 7 Sketches §1.4, Definition 1.95, Examples 1.97, 1.113, 1.117, 1.122, Propositions 1.107, 1.111, Theorem 1.115, Exercises 1.98–1.101, 1.109, 1.110, 1.114, 1.119, 1.125; Remark 1.100; DaoFP §10.8 (“Freyd’s theorem in a preorder”).

Examples

• Example 1.97. $\lceil -/3\rceil :\mathbb{R}\to \mathbb{Z}$ is left adjoint to $(3\times -):\mathbb{Z}\to \mathbb{R}$, since $\lceil x/3\rceil \le y$ iff $x\le 3y$. The right adjoint of $(3\times -)$ is $\lfloor -/3\rfloor$ (7S Exercise 1.98); $\lceil -/3\rceil$ has no left adjoint (7S Exercise 1.101).
• Between total orders drawn with bending arrows, $f⊣g$ iff the arrows do not cross (Remark 1.100, 7S Exercise 1.99).
• Pushforward and Pullback of Partitions: any function $g:S\to T$ gives $g_{!}⊣g^{\ast }$ between $\mathrm{Prt}(S)$ and $\mathrm{Prt}(T)$.
• Direct Image, Preimage, and Dual Image: $f_{!}⊣f^{\ast }⊣f_{\ast }$ between power sets (Example 1.117).
• Closure operators $j$ give $j⊣\iota$ between $P$ and ${\mathrm{fix}}_j$ (Example 1.122).
• Reflexive Transitive Closure: $\mathrm{Cl}⊣U$ between relations and preorders on a set (§1.4.5).
• Example 1.113 shows right adjoints need not preserve joins (7S Exercise 1.114).
• Monoidal closed preorders: $(-\otimes a)⊣(a⊸-)$.

Proposition 1.107 (unit/counit characterization)

For monotone $f:P\to Q$, $g:Q\to P$ the following are equivalent: (a) $f⊣g$; (b) for all $p,q$: $p\le g(f(p))$ and $f(g(q))\le q$. $(1.108)$

Proof. Suppose $f⊣g$. For $p\in P$ put $q:=f(p)$; reflexivity $f(p)\le q$ gives $p\le g(q)=g(f(p))$. Similarly $f(g(q))\le q$ (7S Exercise 1.109). Conversely assume (1.108). If $f(p)\le q$ then by monotonicity $g(f(p))\le g(q)$, and $p\le g(f(p))$, so $p\le g(q)$. The other direction is similar. $■$

Replacing $\le$ by $\cong$ in (1.108) recovers isomorphism. The inequalities are the preorder versions of the unit and counit.

Basic theory

• Uniqueness: a right (or left) adjoint, if it exists, is unique up to equivalence: $g(q)\cong g^{\prime }(q)$ for all $q$ (7S Exercise 1.110; proof: $g(q)\le g^{\prime }(f(g(q)))\le g^{\prime }(q)$).
• Right Adjoints Preserve Meets, left adjoints preserve joins (Proposition 1.111). Hence left adjoints have no Generative Effect.
• Adjoint Functor Theorem for Preorders (Theorem 1.115): if $Q$ has all meets, $g:Q\to P$ is a right adjoint iff it preserves meets; dually for joins. DaoFP §10.8 presents the same fact as Freyd’s adjoint functor theorem in a preorder.
• The composite $f;g:P\to P$ is a Closure Operator, and $g;f$ an Interior Operator (7S Exercise 1.119).
• Galois connections relate different models of computation states in program analysis (abstract interpretation, [NNH99]).

JuliaLeanHaskell

Docs: Vignette: meets

Builds on: Natural Numbers (UsualOrder) — run that note’s Julia code first.

# check the adjunction condition on finite preorders
is_galois(pP, pQ, f, g, ps, qs) =
  all(leq(pQ, f(p), q) == leq(pP, p, g(q)) for p in ps, q in qs)
 
# Example 1.97 restricted to a finite window: ⌈-/3⌉ ⊣ (3×-)
f(x) = ceil(Int, x / 3); g(y) = 3y
is_galois(UsualOrder(), UsualOrder(), f, g, -10:10, -4:4)   # true
 
# Catlab: Galois connections appear as adjunctions between thin categories;
# e.g. the closure/underlying adjunction between relations and preorders (see [[Reflexive Transitive Closure]])

-- Mathlib: `GaloisConnection l u : ∀ a b, l a ≤ b ↔ a ≤ u b`
#check @GaloisConnection
example : GaloisConnection (fun n : ℕ => n + 1) (fun m : ℕ => m - 1) := by
  intro a b; constructor <;> omega   -- (in ℕ with truncated subtraction, b ≥ 1 needed; illustrative)
#check @GaloisConnection.le_u_l          -- p ≤ g (f p)   (unit)
#check @GaloisConnection.l_u_le          -- f (g q) ≤ q   (counit)
#check @GaloisConnection.u_iInf          -- right adjoints preserve meets
#check @GaloisConnection.l_iSup          -- left adjoints preserve joins
#check @GaloisConnection.compose
-- Example 1.97: Int.ceil ⊣ cast, cast ⊣ Int.floor
#check @Int.gc_ceil_coe                  -- GaloisConnection Int.ceil (↑)
#check @Int.gc_coe_floor                 -- GaloisConnection (↑) Int.floor

-- a Galois connection between preorders (laws unenforced)
data Galois a b = Galois { leftAdj :: a -> b, rightAdj :: b -> a }
-- law: leq (leftAdj p) q == leq p (rightAdj q)
 
-- Example 1.97 on Double/Integer
ex197 :: Galois Double Integer
ex197 = Galois (\x -> ceiling (x / 3)) (\y -> 3 * fromInteger y)
 
checkGalois :: (Preorder a, Preorder b) => Galois a b -> [a] -> [b] -> Bool
checkGalois (Galois f g) ps qs = and [ leq (f p) q == leq p (g q) | p <- ps, q <- qs ]