Adjunctions · The Lumenary

Lens

MotivationH

The best approximation from either side

The inclusion of the integers into the real numbers has no inverse: $\pi$ is not an integer. But it has two best approximations. The floor $\lfloor x \rfloor$ is the best integer approximation from below and the ceiling $\lceil x \rceil$ the best from above, and "best" has a crisp meaning: for every integer $n$ ,

n \le \lfloor x \rfloor \iff n \le x, \qquad \lceil x \rceil \le n \iff x \le n .

The forgetful functor from groups to sets has no inverse either: most sets carry many group structures, or none in any canonical way. But it has a best approximation from one side: the free group $F(S)$ on a set $S$ , characterised by "a homomorphism $F(S) \to G$ is the same as a function $S \to G$ ".

The same shape appears when a function of two variables is curried into a function of one variable returning functions, when the image of a set under a map is compared with a preimage, when a quantifier $\exists x$ is compared with a free variable, and when a tensor product is compared with bilinear maps. In each case two constructions $F$ and $G$ point in opposite directions and

\Hom(F A, B) \;\cong\; \Hom(A, G B),

naturally in $A$ and $B$ . Daniel Kan named this relationship an adjunction in 1958. Saunders Mac Lane later summarised the experience of a generation: "adjoint functors arise everywhere".

IntuitionH

Galois connections first

A poset is a category with at most one arrow between two objects, so a hom-set is either empty or a single point and "naturally isomorphic hom-sets" just means "one inequality holds exactly when the other does". An adjunction between posets is therefore a pair of monotone maps $l : P \to Q$ and $u : Q \to P$ with

l(a) \le b \iff a \le u(b) \qquad \text{for all } a \in P,\ b \in Q,

a Galois connection. Floor and ceiling are the examples above, with the inclusion $\Z \to \R$ playing the role of $u$ for the ceiling and of $l$ for the floor: $\lceil - \rceil \dashv \iota \dashv \lfloor - \rfloor$ . The direct image and preimage under a map $f : X \to Y$ are another: $f(S) \subseteq T \iff S \subseteq f^{-1}(T)$ .

Two things are visible already here. First, adjoints are not inverses: $\lfloor \iota(n) \rfloor = n$ , but $\iota(\lfloor x \rfloor) \le x$ with equality only for integers. Second, a left adjoint is pinned down by its right adjoint: $\lceil x \rceil$ must be the least integer $n$ with $x \le n$ — there is no choice. Everything in this lesson is a categorified version of these two observations: the inequalities $a \le u(l(a))$ and $l(u(b)) \le b$ become the unit and counit, and "the least $n$ with…" becomes a universal property.

DefinitionsH

Definitions

Throughout, $\mathcal{C}$ and $\mathcal{D}$ are locally small categories and composition is written $g \circ f$ .

Definition— adjunction (hom-set form)

An adjunction between functors $F : \mathcal{C} \to \mathcal{D}$ and $G : \mathcal{D} \to \mathcal{C}$ is a family of bijections

\varphi_{A,B} : \Hom_{\mathcal{D}}(FA, B) \xrightarrow{\;\cong\;} \Hom_{\mathcal{C}}(A, GB),

natural in $A$ and $B$ : for $a : A' \to A$ in $\mathcal{C}$ , $b : B \to B'$ in $\mathcal{D}$ and $k : FA \to B$ ,

\varphi(b \circ k \circ Fa) = Gb \circ \varphi(k) \circ a .

$F$ is left adjoint to $G$ and $G$ right adjoint to $F$ , written $F \dashv G$ . The arrow $\varphi(k) : A \to GB$ is the transpose (or adjunct) of $k : FA \to B$ .

An adjunction

F \dashv G

F

is the left adjoint (it appears on the left of the hom-set,

\operatorname{Hom}(FA, B)

Definition— unit, counit and the triangle identities

Given $F \dashv G$ , the unit is the natural transformation $\eta : \mathrm{id}_{\mathcal{C}} \Rightarrow GF$ with $\eta_A = \varphi(\mathrm{id}_{FA})$ , and the counit is $\varepsilon : FG \Rightarrow \mathrm{id}_{\mathcal{D}}$ with $\varepsilon_B = \varphi^{-1}(\mathrm{id}_{GB})$ . They satisfy the triangle identities

\varepsilon_{FA} \circ F\eta_A = \mathrm{id}_{FA}, \qquad G\varepsilon_B \circ \eta_{GB} = \mathrm{id}_{GB},

written more compactly $\varepsilon F \circ F\eta = 1_F$ and $G\varepsilon \circ \eta G = 1_G$ .

The triangle identities.

Definition— Galois connection

A Galois connection between posets $P$ and $Q$ is a pair of maps $l : P \to Q$ , $u : Q \to P$ with $l(a) \le b \iff a \le u(b)$ for all $a, b$ — an adjunction $l \dashv u$ between the posets regarded as categories. (Both maps are then automatically monotone.) An antitone Galois connection is a Galois connection between $P$ and $Q^{\mathrm{op}}$ .

Definition— universal arrow

For a functor $G : \mathcal{D} \to \mathcal{C}$ and an object $A$ of $\mathcal{C}$ , a universal arrow from $A$ to $G$ is an object $FA$ of $\mathcal{D}$ with an arrow $\eta_A : A \to G(FA)$ such that every $f : A \to GB$ is $G(k) \circ \eta_A$ for a unique $k : FA \to B$ . (This is the definition of a free object, made general.)

Worked examplesH

Examples

Example— Free ⊣ forgetful

Let $U : \cat{Mon} \to \cat{Set}$ forget the multiplication and let $F(S)$ be the free monoid of finite words in $S$ . A monoid homomorphism $F(S) \to M$ is determined by, and can be chosen freely on, the generators: $\Hom_{\cat{Mon}}(FS, M) \cong \Hom_{\cat{Set}}(S, UM)$ , $k \mapsto k \circ \eta_S$ , where $\eta_S : S \to UFS$ sends $s$ to the one-letter word. The counit $\varepsilon_M : FUM \to M$ evaluates a word of elements of $M$ by multiplying it out. The same holds for free groups, free vector spaces ( $\Hom_k(k^{(S)}, V) \cong \Hom_{\cat{Set}}(S, V)$ : a linear map is determined freely by its values on a basis), free abelian groups, free modules and polynomial rings ( $\Hom_{\cat{CRing}}(\Z[x_s : s \in S], R) \cong R^S$ ). In each case the free functor is the left adjoint.

Example— Currying

In $\cat{Set}$ fix a set $B$ . Then $- \times B \dashv (-)^B$ , where $C^B$ is the set of functions $B \to C$ :

\Hom(A \times B, C) \cong \Hom(A, C^B), \qquad h \mapsto \big(a \mapsto (b \mapsto h(a, b))\big).

The unit $\eta_A : A \to (A \times B)^B$ is $a \mapsto (b \mapsto (a, b))$ and the counit $\varepsilon_C : C^B \times B \to C$ is evaluation, $(\varphi, b) \mapsto \varphi(b)$ . A category in which every $- \times B$ has a right adjoint is cartesian closed; $\cat{Set}$ , $\cat{Cat}$ and the category of compactly generated spaces are examples, and cartesian closed categories model the typed λ-calculus.

Example— Tensor and hom

For modules over a commutative ring $R$ and a fixed module $N$ : $- \otimes_R N \dashv \Hom_R(N, -)$ , i.e. $\Hom_R(M \otimes_R N, P) \cong \Hom_R(M, \Hom_R(N, P))$ — both sides are the $R$ -bilinear maps $M \times N \to P$ . This is currying for linear algebra.

Example— Images, preimages and quantifiers

For $f : X \to Y$ , regard the power sets as posets. Then

f_!(S) \subseteq T \iff S \subseteq f^{-1}(T) \qquad\text{and}\qquad f^{-1}(T) \subseteq S \iff T \subseteq f_*(S),

where $f_!(S) = f(S) = \{y : \exists x \in S,\ f(x) = y\}$ and $f_*(S) = \{y : \forall x,\ f(x) = y \Rightarrow x \in S\}$ . So $f_! \dashv f^{-1} \dashv f_*$ : the preimage has adjoints on both sides, an "existential" image and a "universal" image. For the projection $f : X \times Y \to Y$ these are the quantifiers $\exists x$ and $\forall x$ .

Example— Spaces, groups and pointed sets

$U : \cat{Top} \to \cat{Set}$ has a left adjoint (discrete topology) and a right adjoint (indiscrete topology): $\mathrm{Disc} \dashv U \dashv \mathrm{Indisc}$ .
The inclusion $\cat{Ab} \hookrightarrow \cat{Grp}$ has a left adjoint, abelianisation: $\Hom_{\cat{Grp}}(G, A) \cong \Hom_{\cat{Ab}}(G^{\mathrm{ab}}, A)$ for abelian $A$ .
The forgetful functor from pointed sets to sets has the left adjoint $X \mapsto X \sqcup \{\ast\}$ ("adjoin a base point").
The inclusion of compact Hausdorff spaces into $\cat{Top}$ has a left adjoint, the Stone–Čech compactification $\beta$ .
For a small category $\mathcal{J}$ , the diagonal functor $\Delta : \mathcal{C} \to [\mathcal{J}, \mathcal{C}]$ has $\operatorname{colim} \dashv \Delta \dashv \lim$ whenever these exist (see limits and colimits).

Example— Non-examples

The forgetful functor $U : \cat{Field} \to \cat{Set}$ has no left adjoint: there is no "free field". (Proof below: a left adjoint would send $\varnothing$ to an initial field.)
The functor $X \mapsto X \sqcup \{\ast\}$ on $\cat{Set}$ has neither a left nor a right adjoint — although it is a left adjoint when regarded as a functor to pointed sets. Which category a functor lands in matters.
$U : \cat{Grp} \to \cat{Set}$ has a left adjoint but no right adjoint (it does not preserve coproducts).

ProofH

Theorems and proofs

Theorem— Theorem 1 (hom-sets versus unit and counit)

(a) Given an adjunction $\varphi$ , the unit and counit defined above are natural and satisfy the triangle identities, and $\varphi(k) = Gk \circ \eta_A$ , $\varphi^{-1}(f) = \varepsilon_B \circ Ff$ .

(b) Conversely, natural transformations $\eta : \mathrm{id} \Rightarrow GF$ and $\varepsilon : FG \Rightarrow \mathrm{id}$ satisfying the triangle identities define an adjunction by $\varphi(k) = Gk \circ \eta_A$ , with inverse $f \mapsto \varepsilon_B \circ Ff$ .

Proof

(a) Naturality of $\varphi$ in $B$ with $a = \mathrm{id}$ gives $\varphi(k) = \varphi(k \circ \mathrm{id}_{FA}) = Gk \circ \varphi(\mathrm{id}_{FA}) = Gk \circ \eta_A$ ; dually $\varphi^{-1}(f) = \varepsilon_B \circ Ff$ . Naturality of $\eta$ : for $a : A' \to A$ , $GFa \circ \eta_{A'} = \varphi(Fa \circ \mathrm{id}_{FA'}) = \varphi(\mathrm{id}_{FA} \circ Fa) = \eta_A \circ a$ , using naturality of $\varphi$ in each variable. Naturality of $\varepsilon$ is dual. Triangle identities: $\varepsilon_{FA} \circ F\eta_A = \varphi^{-1}(\eta_A) = \varphi^{-1}(\varphi(\mathrm{id}_{FA})) = \mathrm{id}_{FA}$ , and $G\varepsilon_B \circ \eta_{GB} = \varphi(\varepsilon_B) = \varphi(\varphi^{-1}(\mathrm{id}_{GB})) = \mathrm{id}_{GB}$ .

(b) The two maps are mutually inverse: for $k : FA \to B$ ,

\varepsilon_B \circ F(Gk \circ \eta_A) = \varepsilon_B \circ FGk \circ F\eta_A = k \circ \varepsilon_{FA} \circ F\eta_A = k,

by naturality of $\varepsilon$ and the first triangle identity; symmetrically $G(\varepsilon_B \circ Ff) \circ \eta_A = G\varepsilon_B \circ \eta_{GB} \circ f = f$ by naturality of $\eta$ and the second identity. Naturality of $\varphi(k) = Gk \circ \eta_A$ : $G(b \circ k \circ Fa) \circ \eta_{A'} = Gb \circ Gk \circ GFa \circ \eta_{A'} = Gb \circ Gk \circ \eta_A \circ a$ .

∎

Equivalently, $F \dashv G$ means that each $\eta_A : A \to GFA$ is a universal arrow from $A$ to $G$ : every $f : A \to GB$ factors as $G(k) \circ \eta_A$ for a unique $k$ , namely $k = \varphi^{-1}(f)$ . Conversely, if every object $A$ has a universal arrow to $G$ , the choices assemble into a left adjoint $F$ (define $F$ on arrows by the uniqueness clause). That is how free objects become free functors.

Theorem— Theorem 2 (uniqueness of adjoints)

If $F \dashv G$ and $F' \dashv G$ , then $F \cong F'$ by a unique natural isomorphism compatible with the units. Dually, right adjoints are unique up to unique isomorphism.

Proof

For each $A$ , both $\eta_A : A \to GFA$ and $\eta'_A : A \to GF'A$ are universal arrows from $A$ to $G$ . Universal arrows are initial objects of the category whose objects are pairs $(B, f : A \to GB)$ and whose morphisms $(B, f) \to (B', f')$ are arrows $k : B \to B'$ with $Gk \circ f = f'$ . Initial objects are unique up to unique isomorphism, so there is a unique $\theta_A : FA \to F'A$ with $G\theta_A \circ \eta_A = \eta'_A$ , and it is an isomorphism. For $a : A_1 \to A_2$ , the arrows $\theta_{A_2} \circ Fa$ and $F'a \circ \theta_{A_1}$ both transpose (under $F \dashv G$ ) to $\eta'_{A_2} \circ a = GF'a \circ \eta'_{A_1}$ , so they are equal: $\theta$ is natural.

∎

For Galois connections uniqueness is visible directly: if $l \dashv u$ and $l \dashv u'$ , then for every $a$ , $a \le u(b) \iff l(a) \le b \iff a \le u'(b)$ , so $u(b) = u'(b)$ .

Theorem— Theorem 3 (right adjoints preserve limits)

If $F \dashv G$ , then $G$ preserves all limits that exist in $\mathcal{D}$ , and $F$ preserves all colimits that exist in $\mathcal{C}$ .

Proof

Let $(L, \pi)$ be a limit of $D : \mathcal{J} \to \mathcal{D}$ . We show that $(GL, G\pi)$ is a limit of $GD$ . Let $(X, \lambda)$ be a cone over $GD$ , so $\lambda_j : X \to GD(j)$ with $GD(u) \circ \lambda_i = \lambda_j$ . Transpose: $\varphi^{-1}(\lambda_j) : FX \to D(j)$ , and by naturality of $\varphi^{-1}$ in the second variable,

D(u) \circ \varphi^{-1}(\lambda_i) = \varphi^{-1}(GD(u) \circ \lambda_i) = \varphi^{-1}(\lambda_j),

so these form a cone over $D$ with apex $FX$ . It factors through $L$ by a unique $k : FX \to L$ with $\pi_j \circ k = \varphi^{-1}(\lambda_j)$ . Transposing back, $h = \varphi(k) : X \to GL$ satisfies $G\pi_j \circ h = \varphi(\pi_j \circ k) = \lambda_j$ . If also $G\pi_j \circ h' = \lambda_j$ for all $j$ , then $\pi_j \circ \varphi^{-1}(h') = \varphi^{-1}(\lambda_j)$ , so $\varphi^{-1}(h') = k$ and $h' = h$ . The statement about $F$ is the dual (apply the first part to $G^{\mathrm{op}} \dashv F^{\mathrm{op}}$ ).

∎

The proof is the slogan "maps into a limit are compatible families of maps", transported along the bijection $\varphi$ . Its main use is negative: to show that a functor has no left adjoint, find a limit it does not preserve.

Theorem— Corollary (functors without adjoints)

(a) $U : \cat{Field} \to \cat{Set}$ has no left adjoint. (b) $X \mapsto X \sqcup \{\ast\}$ on $\cat{Set}$ has neither a left nor a right adjoint. (c) $U : \cat{Grp} \to \cat{Set}$ has no right adjoint.

Proof

(a) A left adjoint $F$ preserves colimits, in particular initial objects: $F(\varnothing)$ would be an initial field. But a field has a characteristic, and ring homomorphisms between fields preserve it, so no field maps to fields of every characteristic. (b) A right adjoint preserves terminal objects, but $\{\ast\} \sqcup \{\ast\}$ has two elements and is not terminal; a left adjoint preserves initial objects, but $\varnothing \sqcup \{\ast\}$ is not empty. (c) A left adjoint preserves coproducts and the initial object, but $U(\Z * \Z) \neq U(\Z) \sqcup U(\Z)$ and the trivial group has a non-empty underlying set (see the previous lesson).

∎

Theorem— Theorem 4 (an adjunction restricts to an equivalence)

Let $F \dashv G$ . Let $\mathcal{C}_0 \subseteq \mathcal{C}$ be the full subcategory of objects $A$ with $\eta_A$ invertible and $\mathcal{D}_0 \subseteq \mathcal{D}$ the full subcategory of objects $B$ with $\varepsilon_B$ invertible. Then $F$ and $G$ restrict to an equivalence $\mathcal{C}_0 \simeq \mathcal{D}_0$ . In particular, $F \dashv G$ is an adjoint equivalence exactly when all components of $\eta$ and $\varepsilon$ are isomorphisms.

Proof

If $\eta_A$ is invertible, the first triangle identity $\varepsilon_{FA} \circ F\eta_A = \mathrm{id}$ shows $\varepsilon_{FA} = (F\eta_A)^{-1}$ is invertible, so $F$ maps $\mathcal{C}_0$ into $\mathcal{D}_0$ . Symmetrically, the second identity shows $G$ maps $\mathcal{D}_0$ into $\mathcal{C}_0$ . On these subcategories $\eta$ and $\varepsilon$ are natural isomorphisms $\mathrm{id} \cong GF$ and $FG \cong \mathrm{id}$ , which is the definition of an equivalence.

∎

For a Galois connection, $\mathcal{C}_0$ and $\mathcal{D}_0$ are the closed elements $\{a : a = u(l(a))\}$ and $\{b : b = l(u(b))\}$ , and Theorem 4 says $l$ and $u$ restrict to inverse order-isomorphisms between them. The fundamental theorem of Galois theory has exactly this shape (subgroups and intermediate fields are the closed elements of an antitone Galois connection), and so does the Nullstellensatz (see the geometry viewpoint). The second computation below shows it for a small relation.

Theorem— Theorem 5 (the adjoint functor theorem for complete lattices)

Let $u : Q \to P$ be a map between complete lattices. Then $u$ has a left adjoint if and only if it preserves all infima: $u(\bigwedge S) = \bigwedge u(S)$ for every $S \subseteq Q$ . The left adjoint is $l(a) = \bigwedge \{ b \in Q : a \le u(b) \}$ .

Proof

( $\Rightarrow$ ) Infima are limits in a poset, and right adjoints preserve limits (Theorem 3). Directly: $a \le u(\bigwedge S) \iff l(a) \le \bigwedge S \iff l(a) \le b$ for all $b \in S \iff a \le u(b)$ for all $b \in S \iff a \le \bigwedge u(S)$ .

( $\Leftarrow$ ) First, $u$ is monotone: if $b \le b'$ then $u(b) = u(b \wedge b') = u(b) \wedge u(b') \le u(b')$ . If $a \le u(b)$ , then $b$ belongs to the set defining $l(a)$ , so $l(a) \le b$ . Conversely $u(l(a)) = \bigwedge \{u(b) : a \le u(b)\} \ge a$ , so $l(a) \le b$ implies $a \le u(l(a)) \le u(b)$ .

∎

For categories, the analogue is Freyd's general adjoint functor theorem (1964): if $\mathcal{D}$ is complete and locally small and $G : \mathcal{D} \to \mathcal{C}$ preserves limits, then $G$ has a left adjoint provided a "solution set condition" holds (for each $A$ , a set of arrows $A \to GB_i$ through which every $A \to GB$ factors). The solution set condition replaces the infimum over the possibly proper class $\{b : a \le u(b)\}$ by a limit over a set of arrows. We do not prove the theorem here (see Mac Lane, Chapter V, or Riehl, Chapter 4); Mathlib has it, and we cite it in the formal section.

Theorem— Theorem 6 (every adjunction gives a monad)

If $F \dashv G$ with unit $\eta$ and counit $\varepsilon$ , then $T = GF$ with unit $\eta$ and multiplication $\mu = G\varepsilon F : GFGF \Rightarrow GF$ is a monad on $\mathcal{C}$ .

Proof

The unit laws $\mu \circ T\eta = 1 = \mu \circ \eta T$ are $G(\varepsilon_{FA} \circ F\eta_A) = \mathrm{id}$ and $G\varepsilon_{FA} \circ \eta_{GFA} = \mathrm{id}$ : the two triangle identities (whiskered). Associativity $\mu \circ T\mu = \mu \circ \mu T$ is $G$ applied to $\varepsilon_{FA} \circ FG\varepsilon_{FA} = \varepsilon_{FA} \circ \varepsilon_{FGFA}$ , which is naturality of $\varepsilon$ at the arrow $\varepsilon_{FA}$ .

∎

The free–forgetful adjunction for monoids gives the list monad; see monads for the converse — every monad comes from an adjunction.

Formal mathematicsF

Adjunctions in Lean and Mathlib

Currying with plain functions: the bijection, its naturality, the unit, the counit and the triangle identities — all hold by computation (rfl), exactly as in the hand calculation.

curryEquivLean 4Formally verified

/-- **Currying.** Functions of two arguments `A × B → C` correspond bijectively to functions
`A → (B → C)` returning functions: `h ↦ (a ↦ (b ↦ h (a, b)))`, with inverse "uncurrying". This is
the hom-set bijection `Hom(A × B, C) ≅ Hom(A, C^B)` of the adjunction `− × B ⊣ (−)^B`.
(Mathlib: `Equiv.curry`.) -/
def curryEquiv (A B C : Type u) : (A × B → C) ≃ (A → B → C) where
  toFun h a b := h (a, b)
  invFun k p := k p.1 p.2
  left_inv _ := rfl
  right_inv _ := rfl

Axioms used: No axiomsformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

curry_naturalLean 4Proved here from basic factsFormally verified

/-- **The currying bijection is natural in `A` and in `C`.** Precomposing with `u : A' → A` (on
`A × B`, with `u × id`) and postcomposing with `v : C → C'` before currying gives the same as
currying first and then precomposing with `u` and postcomposing with `v` pointwise. Both sides are
`a' ↦ b ↦ v (h (u a', b))`, so Lean accepts `rfl`. -/
theorem curry_natural (u : A' → A) (v : C → C') (h : A × B → C) :
    curryEquiv A' B C' (v ∘ h ∘ Prod.map u id) = fun a' => v ∘ curryEquiv A B C h (u a') :=
  rfl

Axioms used: Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

curryUnitLean 4Formally verified

/-- The **unit** of the currying adjunction, `η_A : A → (B → A × B)`, `a ↦ (b ↦ (a, b))`: the
curried form of the identity of `A × B`. -/
def curryUnit (A B : Type u) : A → B → A × B :=
  fun a b => (a, b)

Axioms used: No axiomsformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

curryCounitLean 4Formally verified

/-- The **counit** of the currying adjunction, `ε_C : (B → C) × B → C`, evaluation
`(φ, b) ↦ φ b`: the uncurried form of the identity of `B → C`. -/
def curryCounit (B C : Type u) : (B → C) × B → C :=
  fun p => p.1 p.2

Axioms used: No axiomsformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

curry_trianglesLean 4Proved here from basic factsFormally verified

/-- **The triangle identities for currying.**
1. `ε_{A × B} ∘ (η_A × id_B) = id`: pair `(a, b)` ↦ `(η a, b)` ↦ `η a b = (a, b)`.
2. `(ε_C)^B ∘ η_{C^B} = id`: `φ` ↦ `(b ↦ (φ, b))` ↦ `(b ↦ φ b) = φ`.
Both hold by computation. -/
theorem curry_triangles :
    (curryCounit B (A × B) ∘ Prod.map (curryUnit A B) id = id) ∧
      ((fun (k : B → (B → C) × B) => curryCounit B C ∘ k) ∘ curryUnit (B → C) B = id) :=
  ⟨rfl, rfl⟩

Axioms used: No axiomsformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

Free monoids. Mathlib's FreeMonoid.lift is the hom-set bijection; we prove the uniqueness half by induction on words, and that the unit is not an isomorphism.

free_monoid_liftLean 4Applies a library theoremFormally verified

/-- **Free monoid ⊣ forgetful.** Functions `α → M` into (the underlying set of) a monoid
correspond bijectively to monoid homomorphisms `FreeMonoid α →* M`, by extending a function to
words multiplicatively: `Hom_Mon(F α, M) ≅ Hom_Set(α, U M)`. This is Mathlib's `FreeMonoid.lift`,
and naturality in `M` is `FreeMonoid.comp_lift`. -/
theorem free_monoid_lift {N : Type u} [Monoid N] (g : M →* N) (f : α → M) :
    Function.Bijective (FreeMonoid.lift : (α → M) → (FreeMonoid α →* M)) ∧
      g.comp (FreeMonoid.lift f) = FreeMonoid.lift (g ∘ f) :=
  ⟨FreeMonoid.lift.bijective, FreeMonoid.comp_lift g f⟩

Axioms used: propext, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

free_hom_extLean 4Proved here from basic factsFormally verified

/-- **Uniqueness in the universal property of the free monoid.** Two homomorphisms out of
`FreeMonoid α` that agree on the generators `of x` agree everywhere: by induction on words, using
`f 1 = 1 = g 1` and `f (of x * w) = f (of x) * f w`. -/
theorem free_hom_ext {f g : FreeMonoid α →* M} (h : ∀ x, f (FreeMonoid.of x) = g (FreeMonoid.of x)) :
    f = g := by
  refine DFunLike.ext _ _ fun w => ?_
  induction w using FreeMonoid.inductionOn' with
  | one => rw [map_one, map_one]
  | of_mul x w ih => rw [map_mul, map_mul, h x, ih]

Axioms used: propext, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

unit_not_surjectiveLean 4Proved here from basic factsFormally verified

/-- **The unit of an adjunction need not be an isomorphism.** The unit of free ⊣ forgetful at a
set `α` is `of : α → FreeMonoid α`. It is never surjective: the empty word `1` is not a generator.
So this adjunction is not an equivalence. -/
theorem unit_not_surjective : ¬ Function.Surjective (FreeMonoid.of : α → FreeMonoid α) := by
  intro hs
  obtain ⟨x, hx⟩ := hs 1
  exact FreeMonoid.of_ne_one x hx

Axioms used: propext, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

Galois connections. Mathlib's GaloisConnection l u is literally ∀ a b, l a ≤ b ↔ a ≤ u b. Image ⊣ preimage and ceiling ⊣ inclusion ⊣ floor are in Mathlib; the preservation and uniqueness results, the non-existence argument and Theorem 5 are proved here.

image_preimageLean 4Applies a library theoremFormally verified

/-- **Image ⊣ preimage.** For `f : α → β`, `f '' S ⊆ T ↔ S ⊆ f ⁻¹' T`: direct image is left adjoint
to inverse image between the power-set lattices. This is Mathlib's `Set.image_preimage`. -/
theorem image_preimage {α β : Type u} (f : α → β) :
    GaloisConnection (Set.image f) (Set.preimage f) :=
  Set.image_preimage

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

floor_ceilLean 4Applies a library theoremFormally verified

/-- **Ceiling ⊣ inclusion ⊣ floor.** For the inclusion `ℤ → ℝ`: `⌈x⌉ ≤ n ↔ x ≤ n` and
`n ≤ ⌊x⌋ ↔ (n : ℝ) ≤ x`. The inclusion has a left adjoint (ceiling) and a right adjoint (floor).
These are Mathlib's `Int.gc_ceil_coe` and `Int.gc_coe_floor`. -/
theorem floor_ceil :
    GaloisConnection (Int.ceil : ℝ → ℤ) (fun n : ℤ => (n : ℝ)) ∧
      GaloisConnection (fun n : ℤ => (n : ℝ)) (Int.floor : ℝ → ℤ) :=
  ⟨Int.gc_ceil_coe, Int.gc_coe_floor⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

left_adjoint_supLean 4Proved here from basic factsFormally verified

/-- **Left adjoints preserve joins** (binary coproducts in a poset). If `l ⊣ u`, then
`l (a ⊔ b) = l a ⊔ l b`. (≤): `a ≤ u (l a ⊔ l b)` because `l a ≤ l a ⊔ l b`, likewise for `b`,
so `a ⊔ b ≤ u (l a ⊔ l b)`, i.e. `l (a ⊔ b) ≤ l a ⊔ l b`. (≥): `l` is monotone.
(Mathlib: `GaloisConnection.l_sup`.) -/
theorem left_adjoint_sup [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) (a b : α) : l (a ⊔ b) = l a ⊔ l b := by
  apply le_antisymm
  · rw [gc]
    exact sup_le ((gc _ _).1 le_sup_left) ((gc _ _).1 le_sup_right)
  · exact sup_le (gc.monotone_l le_sup_left) (gc.monotone_l le_sup_right)

Axioms used: propext, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

left_adjoint_botLean 4Proved here from basic factsFormally verified

/-- **Left adjoints preserve the least element** (the empty coproduct, an initial object):
`l ⊥ ≤ b ↔ ⊥ ≤ u b`, which is true for every `b`, so `l ⊥ ≤ ⊥`. -/
theorem left_adjoint_bot [PartialOrder α] [OrderBot α] [PartialOrder β] [OrderBot β] {l : α → β}
    {u : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥ :=
  le_antisymm ((gc _ _).2 bot_le) bot_le

Axioms used: No axiomsformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

right_adjoint_uniqueLean 4Proved here from basic factsFormally verified

/-- **Right adjoints are unique.** If `l ⊣ u` and `l ⊣ u'` between partial orders, then `u = u'`:
for every `b` and every `a`, `a ≤ u b ↔ l a ≤ b ↔ a ≤ u' b`, and an element is determined by its
lower set. (This is the poset case of uniqueness of adjoints up to unique isomorphism.) -/
theorem right_adjoint_unique [PartialOrder α] [Preorder β] {l : α → β} {u u' : β → α}
    (gc : GaloisConnection l u) (gc' : GaloisConnection l u') : u = u' := by
  funext b
  apply le_antisymm
  · exact (gc' _ _).1 ((gc _ _).2 le_rfl)
  · exact (gc _ _).1 ((gc' _ _).2 le_rfl)

Axioms used: Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

const_true_no_right_adjointLean 4Proved here from basic factsFormally verified

/-- **Using preservation to rule out an adjoint.** The constant map `Bool → Bool` with value
`true` is monotone, but it sends `⊥ = false` to `true ≠ ⊥`. Left adjoints preserve `⊥`
(`left_adjoint_bot`), so it has no right adjoint. -/
theorem const_true_no_right_adjoint : ¬ ∃ u : Bool → Bool, GaloisConnection (fun _ => true) u := by
  rintro ⟨u, gc⟩
  have h : true = false := left_adjoint_bot gc
  exact Bool.noConfusion h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

adjoint_functor_theorem_latticesLean 4Proved here from basic factsFormally verified

/-- **The adjoint functor theorem for complete lattices.** If `u : β → α` between complete
lattices preserves all infima (all limits of the poset), then `u` has a left adjoint, given by
the formula `l a = ⨅ { b | a ≤ u b }` (the "best approximation from above").
Proof: `u` is monotone (if `b ≤ b'` then `u b = u (⨅ {b, b'}) = u b ⊓ u b' ≤ u b'`). If
`a ≤ u b` then `b` belongs to the set, so `l a ≤ b`. Conversely `u (l a)` is the infimum of
the `u b` with `a ≤ u b`, all of which are `≥ a`; so `a ≤ u (l a) ≤ u b` whenever `l a ≤ b`. -/
theorem adjoint_functor_theorem_lattices [CompleteLattice α] [CompleteLattice β] (u : β → α)
    (hu : ∀ S : Set β, u (sInf S) = sInf (u '' S)) :
    GaloisConnection (fun a => sInf {b | a ≤ u b}) u := by
  have mono : Monotone u := by
    intro b b' h
    have hpair : u (sInf {b, b'}) = sInf (u '' {b, b'}) := hu {b, b'}
    rw [sInf_pair, inf_eq_left.mpr h, Set.image_pair, sInf_pair] at hpair
    rw [hpair]
    exact inf_le_right
  intro a b
  constructor
  · intro h
    refine le_trans ?_ (mono h)
    rw [hu]
    exact le_sInf (by rintro _ ⟨c, hc, rfl⟩; exact hc)
  · intro h
    exact sInf_le h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

General adjunctions. Mathlib's Adjunction F G (notation F ⊣ G) is defined by unit, counit and the triangle identities, with the hom-set bijection adj.homEquiv derived from them (Theorem 1). Uniqueness of adjoints, RAPL, the induced monad and Freyd's adjoint functor theorem are library theorems; the tensor–hom adjunction is TensorProduct.lift.equiv. In diagrammatic order, F.map (η.app X) ≫ ε.app (F.obj X) is $\varepsilon_{FX} \circ F\eta_X$ .

triangle_identitiesLean 4Applies a library theoremFormally verified

/-- **The triangle identities.** For an adjunction `F ⊣ G` with unit `η` and counit `ε`:
`ε_{F X} ∘ F(η_X) = id_{F X}` and `G(ε_Y) ∘ η_{G Y} = id_{G Y}` (written in diagrammatic order).
These are the fields `left_triangle_components` and `right_triangle_components` of Mathlib's
`Adjunction`. -/
theorem triangle_identities {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (X : C) (Y : D) :
    F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X) ∧
      adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y) :=
  ⟨adj.left_triangle_components X, adj.right_triangle_components Y⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

left_adjoint_uniqueLean 4Applies a library theoremFormally verified

/-- **Left adjoints are unique up to natural isomorphism**: if `F ⊣ G` and `F' ⊣ G` then
`F ≅ F'`. This applies Mathlib's `Adjunction.leftAdjointUniq` (the isomorphism is moreover
unique compatible with the units). -/
theorem left_adjoint_unique {F F' : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (adj' : F' ⊣ G) :
    Nonempty (F ≅ F') :=
  ⟨Adjunction.leftAdjointUniq adj adj'⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

right_adjoint_preserves_limitsLean 4Applies a library theoremFormally verified

/-- **Right adjoints preserve limits, left adjoints preserve colimits** (RAPL). This applies
Mathlib's `Adjunction.rightAdjoint_preservesLimits` and `Adjunction.leftAdjoint_preservesColimits`;
the lesson proves it from the hom-set bijection. -/
theorem right_adjoint_preserves_limits {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    PreservesLimitsOfSize.{v₂, u₂} G ∧ PreservesColimitsOfSize.{v₁, u₁} F :=
  ⟨adj.rightAdjoint_preservesLimits, adj.leftAdjoint_preservesColimits⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

adjunctionMonadLean 4Formally verified

/-- **Every adjunction induces a monad** `G ∘ F` on `C`, with unit `η` and multiplication
`G ε F : GFGF ⇒ GF`. This is Mathlib's `Adjunction.toMonad`; see the lesson on monads. -/
def adjunctionMonad {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : Monad C :=
  adj.toMonad

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

freyd_adjoint_functor_theoremLean 4Applies a library theoremFormally verified

/-- **Freyd's general adjoint functor theorem.** If `D` is complete (and locally small) and
`G : D ⥤ C` preserves limits and satisfies the *solution set condition* — for each object `A` of
`C`, a set of arrows `A ⟶ G Bᵢ` through which every arrow `A ⟶ G X` factors — then `G` has a
left adjoint. This applies Mathlib's `isRightAdjoint_of_preservesLimits_of_solutionSetCondition`;
`adjoint_functor_theorem_lattices` is the special case of complete lattices, where the solution
set can be taken to be everything. -/
theorem freyd_adjoint_functor_theorem {C : Type u₁} [Category.{v₁} C] {D : Type u₂}
    [Category.{v₁} D] [HasLimits D] (G : D ⥤ C) [PreservesLimits G]
    (hG : SolutionSetCondition.{v₁} G) : G.IsRightAdjoint :=
  isRightAdjoint_of_preservesLimits_of_solutionSetCondition G hG

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

tensorHomLean 4Formally verified

/-- **Tensor–hom adjunction** `− ⊗ N ⊣ Hom(N, −)` for modules over a commutative ring:
bilinear maps `M → N → P` (that is, linear maps `M → Hom(N, P)`) correspond to linear maps
`M ⊗ N → P`. This is Mathlib's `TensorProduct.lift.equiv`, the linear analogue of currying. -/
noncomputable def tensorHom (R M N P : Type u) [CommRing R] [AddCommGroup M] [AddCommGroup N]
    [AddCommGroup P] [Module R M] [Module R N] [Module R P] :
    (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] (TensorProduct R M N →ₗ[R] P) :=
  TensorProduct.lift.equiv (RingHom.id R) M N P

Axioms used: propext, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

Finally, part (b) of the Corollary, by the argument in the lesson: RAPL (and its dual) applied to the terminal and initial objects of the category of types.

option_no_left_adjointLean 4Proved here from basic factsFormally verified

/-- **"Adjoin a point" has no left adjoint on types.** Let `G X = Option X` (that is, `X ⊔ {∗}`).
If `F ⊣ G`, then `G` preserves limits (Mathlib's `rightAdjoint_preservesLimits`), in particular the
terminal object, so `Option PUnit` would be terminal. But there are two different maps
`PUnit → Option PUnit` (constant `none`, constant `some ()`), and a terminal object admits only
one map from each object. -/
theorem option_no_left_adjoint :
    ¬ ∃ F : Type u ⥤ Type u, Nonempty (F ⊣ ofTypeFunctor Option) := by
  rintro ⟨F, ⟨adj⟩⟩
  have := adj.rightAdjoint_preservesLimits
  have hT : IsTerminal ((ofTypeFunctor Option).obj PUnit) :=
    IsTerminal.isTerminalObj _ _ Types.isTerminalPUnit
  have h := hT.hom_ext (↾fun _ : PUnit => (none : Option PUnit))
    (↾fun _ : PUnit => (some PUnit.unit : Option PUnit))
  have h' := ConcreteCategory.congr_hom h PUnit.unit
  simp at h'

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

option_no_right_adjointLean 4Proved here from basic factsFormally verified

/-- **…and no right adjoint either.** A left adjoint preserves colimits, in particular the initial
object `PEmpty`. But `Option PEmpty` has an element (`none`), so there are two different maps from
it to a two-element type, and it is not initial. (Changing the target category repairs this:
`X ↦ X ⊔ {∗}` is left adjoint to the forgetful functor from *pointed* sets to sets.) -/
theorem option_no_right_adjoint :
    ¬ ∃ G : Type u ⥤ Type u, Nonempty (ofTypeFunctor Option ⊣ G) := by
  rintro ⟨G, ⟨adj⟩⟩
  have := adj.leftAdjoint_preservesColimits
  have hI : IsInitial ((ofTypeFunctor Option).obj PEmpty) :=
    IsInitial.isInitialObj _ _ Types.isInitialPEmpty
  have h := hI.hom_ext (↾fun _ : Option PEmpty => (ULift.up true : ULift.{u} Bool))
    (↾fun _ : Option PEmpty => (ULift.up false : ULift.{u} Bool))
  have h' := ConcreteCategory.congr_hom h (none : Option PEmpty.{u + 1})
  exact Bool.noConfusion (congrArg ULift.down h' : true = false)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Adjunctions.leanTry it in the Lean web editor

Not proved here, only cited or not formalised: Theorems 1–3 for general categories (Mathlib proves them; we cite Theorems 2 and 3 above), Freyd's theorem (cited above), Theorem 4 in general, and the non-existence of a free field.

ComputationC

Experiments: adjoints by exhaustion

The first experiment enumerates every monotone map between some small lattices and checks Theorem 5 in its finite form: a right adjoint exists exactly for the maps that preserve finite joins, and it is $u(b) = \max\{a : l(a) \le b\}$ . It then checks that currying is a natural bijection on small finite sets.

Galois connections on finite lattices and currying, exhaustivelyPythonExhaustive finite checkExact computationComputationally tested

"""When does a monotone map between finite lattices have a right adjoint?

A Galois connection l -| u between posets means l(a) <= b if and only if
a <= u(b). For finite lattices the adjoint functor theorem for posets says: a
monotone map l has a right adjoint exactly when it preserves all joins (binary
joins and the least element), and then u(b) = max{a : l(a) <= b}. We test
this on every monotone map between several small lattices. Part 2 checks the
currying adjunction - x B -| (-)^B on small finite sets: the bijection
Hom(A x B, C) -> Hom(A, C^B) and its naturality in A and C.
"""

from itertools import product

def chain(n):
    """The chain 0 < 1 < ... < n-1 as (elements, leq)."""
    return list(range(n)), lambda a, b: a <= b

def boolean_square():
    """Subsets of {0, 1} as bitmasks 0..3, ordered by inclusion."""
    return [0, 1, 2, 3], lambda a, b: a & b == a

def divisors(n):
    """Divisors of n ordered by divisibility."""
    return [d for d in range(1, n + 1) if n % d == 0], lambda a, b: b % a == 0

def join(P, leq, a, b):
    """Least upper bound in a finite lattice."""
    ub = [x for x in P if leq(a, x) and leq(b, x)]
    return next(x for x in ub if all(leq(x, y) for y in ub))

def bottom(P, leq):
    """Least element of a finite lattice."""
    return next(x for x in P if all(leq(x, y) for y in P))

def monotone_maps(L, M):
    """All monotone maps L -> M, as dicts."""
    (P, le_p), (Q, le_q) = L, M
    maps = (dict(zip(P, v)) for v in product(Q, repeat=len(P)))
    return [f for f in maps
            if all(le_q(f[a], f[b]) for a in P for b in P if le_p(a, b))]

def preserves_joins(f, L, M):
    """Does f preserve binary joins and the least element?"""
    (P, le_p), (Q, le_q) = L, M
    return f[bottom(P, le_p)] == bottom(Q, le_q) and all(
        f[join(P, le_p, a, b)] == join(Q, le_q, f[a], f[b]) for a in P for b in P)

def right_adjoint(f, L, M):
    """u with f(a) <= b iff a <= u(b), or None if there is none."""
    (P, le_p), (Q, le_q) = L, M
    u = {}
    for b in Q:
        below = [a for a in P if le_q(f[a], b)]
        top = [a for a in below if all(le_p(x, a) for x in below)]
        if not top:
            return None
        u[b] = top[0]
    ok = all(le_q(f[a], b) == le_p(a, u[b]) for a in P for b in Q)
    return u if ok else None

def curry(h, A, B):
    """Hom(A x B, C) -> Hom(A, C^B), with functions as dicts."""
    return {a: tuple(h[(a, b)] for b in B) for a in A}

def currying_report(A, B, C, A2, C2):
    """(is curry a bijection?, is it natural for all u : A2 -> A, v : C -> C2?)"""
    pairs = list(product(A, B))
    homs = [dict(zip(pairs, v)) for v in product(C, repeat=len(pairs))]
    images = {tuple(sorted(curry(h, A, B).items())) for h in homs}
    bijective = len(images) == len(homs) == (len(C) ** len(B)) ** len(A)
    natural = all(
        curry({(a, b): v[h[(u[a], b)]] for a in A2 for b in B}, A2, B)
        == {a: tuple(v[c] for c in curry(h, A, B)[u[a]]) for a in A2}
        for h in homs
        for u in (dict(zip(A2, w)) for w in product(A, repeat=len(A2)))
        for v in (dict(zip(C, w)) for w in product(C2, repeat=len(C))))
    return bijective, natural

def main():
    cases = [("B2", boolean_square(), "C3", chain(3)),
             ("C3", chain(3), "B2", boolean_square()),
             ("B2", boolean_square(), "B2", boolean_square()),
             ("D12", divisors(12), "C3", chain(3))]
    print("Monotone maps l : L -> M (C3 = chain 0 < 1 < 2, B2 = subsets of")
    print("{0, 1}, D12 = divisors of 12 under divisibility):")
    for name_l, L, name_m, M in cases:
        mono = monotone_maps(L, M)
        adj = [f for f in mono if right_adjoint(f, L, M) is not None]
        pres = [f for f in mono if preserves_joins(f, L, M)]
        print(f"  {name_l:>3} -> {name_m:<3} {len(mono):>3} monotone, {len(adj):>2} "
              f"with right adjoint, = join-preserving: {adj == pres}")
    L, M = chain(3), divisors(12)
    f = {0: 1, 1: 2, 2: 4}
    print(f"  e.g. l = {f} : C3 -> D12 has right adjoint")
    print(f"       u = {right_adjoint(f, L, M)}")
    print()
    print("Currying Hom(A x B, C) -> Hom(A, C^B):")
    for sizes in [(2, 2, 2), (1, 3, 2), (2, 3, 2)]:
        A, B, C = (list(range(k)) for k in sizes)
        bij, nat = currying_report(A, B, C, [0, 1], ["x", "y"])
        print(f"  |A|, |B|, |C| = {sizes}: bijection {bij}, natural in A and C "
              f"{nat}")
    print()
    print("Epistemic status: exhaustive checks over all monotone maps (and all")
    print("maps for currying) in these small examples. They are evidence for the")
    print("theorems; the lesson proves that left adjoints preserve joins and that")
    print("currying is a natural bijection for all sets.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second builds the antitone Galois connection of a relation ("number $n$ has property $p$ "), checks the defining equivalence for all pairs of subsets, and lists the closed sets on both sides — the bijection of Theorem 4, known in data analysis as the lattice of formal concepts.

Galois connections from a relation: closed sets on both sidesPythonExhaustive finite checkExact computationComputationally tested

"""A relation gives a Galois connection; its fixed points correspond exactly.

Any relation R between a set X of objects and a set Y of properties gives two
maps: up(S) = the properties shared by every object in S, and down(T) = the
objects having every property in T. They form an (order-reversing) Galois
connection: S <= down(T) if and only if T <= up(S). We verify this for every
pair of subsets, and then illustrate a general fact about adjunctions: the
connection restricts to a bijection between the closed sets on the two sides
(the fixed points of down o up and of up o down), here the "formal concepts".
"""

from itertools import combinations

OBJECTS = list(range(1, 9))
PROPERTIES = {
    "even": lambda n: n % 2 == 0,
    "odd": lambda n: n % 2 == 1,
    "prime": lambda n: n in (2, 3, 5, 7),
    "square": lambda n: n in (1, 4),
    "div12": lambda n: 12 % n == 0,
    ">4": lambda n: n > 4,
}

def subsets(items):
    """All subsets of a list, as frozensets."""
    return [frozenset(c) for k in range(len(items) + 1)
            for c in combinations(items, k)]

def up(S):
    """Properties shared by every object in S."""
    return frozenset(p for p, has in PROPERTIES.items() if all(has(n) for n in S))

def down(T):
    """Objects having every property in T."""
    return frozenset(n for n in OBJECTS if all(PROPERTIES[p](n) for p in T))

def galois_holds():
    """Number of pairs (S, T) checked, and whether S <= down(T) iff T <= up(S)."""
    xs, ys = subsets(OBJECTS), subsets(list(PROPERTIES))
    ok = all((S <= down(T)) == (T <= up(S)) for S in xs for T in ys)
    return len(xs) * len(ys), ok

def closed_objects():
    """Fixed points of down o up: the closed sets of objects."""
    return sorted({down(up(S)) for S in subsets(OBJECTS)}, key=sorted)

def main():
    pairs, ok = galois_holds()
    print(f"S <= down(T)  iff  T <= up(S): checked {pairs} pairs, holds: {ok}")
    closed = closed_objects()
    closed_props = {up(down(T)) for T in subsets(list(PROPERTIES))}
    print(f"closed sets of objects: {len(closed)}, closed sets of properties: "
          f"{len(closed_props)}")
    matches = {up(S) for S in closed} == closed_props
    inverse = all(down(up(S)) == S for S in closed)
    print(f"up maps one onto the other: {matches}; down inverts it: {inverse}")
    print("The formal concepts (closed objects <-> closed properties):")
    for S in sorted(closed, key=lambda c: (len(c), sorted(c))):
        objs = ",".join(map(str, sorted(S))) or "-"
        props = ", ".join(sorted(up(S))) or "-"
        print(f"  {{{objs}}} <-> {{{props}}}")
    print("Unit S <= down(up(S)) is not always equality: down(up({2, 4})) = "
          f"{sorted(down(up(frozenset({2, 4}))))}")
    print()
    print("Epistemic status: an exhaustive check for one small relation. That")
    print("every relation gives a Galois connection, and that every adjunction")
    print("restricts to an equivalence between its fixed points, is proved in")
    print("the lesson.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Explore

Explore: ceiling ⊣ inclusion ⊣ floor

Move the slider to choose an integer $n$ . The set of $x$ with $\lfloor x \rfloor \ge n$ is exactly the set with $x \ge n$ , and the set with $\lceil x \rceil \le n$ is exactly the set with $x \le n$ : read them off the staircase graphs. Notice the asymmetry: $\lfloor n \rfloor = \lceil n \rceil = n$ for integers, so one of the unit–counit inequalities of each adjunction is an equality; but $\lfloor x \rfloor \le x \le \lceil x \rceil$ are strict for non-integers, so the other one is not — an adjunction, not an inverse.

Best integer approximations from below and above

Move the sliders and trace along the curves to read off values.

⌊x⌋
⌈x⌉
y = x

nn = 1

Trace along xx = 1

⌊x⌋: y = 1
⌈x⌉: y = 1
y = x: y = 1

Exercises

1. Adjunctions

Warm-upHuman

For the free group functor $F : \cat{Set} \to \cat{Grp}$ and the forgetful functor $U : \cat{Grp} \to \cat{Set}$ , which statement is correct?

Choose one

F \dashv U

\Hom_{\cat{Grp}}(F S, G) \cong \Hom_{\cat{Set}}(S, U G)

U \dashv F

\Hom_{\cat{Set}}(U G, S) \cong \Hom_{\cat{Grp}}(G, F S)

F

and

U

are inverse equivalencesNeither is adjoint to the other

2. Adjunctions

Warm-upHuman

Let $|A| = 2$ , $|B| = 3$ and $|C| = 2$ . How many functions $A \to C^B$ are there (where $C^B$ is the set of functions $B \to C$ )? Check your answer against $|\Hom(A \times B, C)|$ .

3. Adjunctions

CoreHuman

On $(\Z, \le)$ let $l(n) = 2n$ . Its right adjoint $u$ satisfies $2n \le m \iff n \le u(m)$ for all integers $n, m$ . What is $u(7)$ ? (And what is $u(-7)$ , for yourself?)

4. Adjunctions

CoreHuman

Given an adjunction $\varphi : \Hom(FA, B) \cong \Hom(A, GB)$ , the unit is $\eta_A = \varphi(\mathrm{id}_{FA})$ . Which formula gives the counit $\varepsilon_B : FGB \to B$ ?

Choose one

\varepsilon_B = \varphi^{-1}(\mathrm{id}_{GB})

\varepsilon_B = \varphi(\mathrm{id}_{B})

\varepsilon_B = G(\eta_B)

\varepsilon_B = \eta_{GB}^{-1}

5. Adjunctions

CoreHuman

Why does the forgetful functor $U : \cat{Field} \to \cat{Set}$ have no left adjoint?

Choose one

A left adjoint would preserve the initial object, so it would send

\varnothing

to an initial field, and

\cat{Field}

has no initial objectBecause

U

is not faithfulBecause fields are infiniteBecause

U

does not reflect isomorphisms

6. Adjunctions

StretchHuman

Abelianisation $G \mapsto G^{\mathrm{ab}}$ is left adjoint to the inclusion $\iota : \cat{Ab} \hookrightarrow \cat{Grp}$ . Which statements follow from “right adjoints preserve limits, left adjoints preserve colimits”? Select all that apply.

Choose all that apply

A product of abelian groups, computed in

\cat{Grp}

, is abelian (and is the product in

\cat{Ab}

(G * H)^{\mathrm{ab}} \cong G^{\mathrm{ab}} \oplus H^{\mathrm{ab}}

.The inclusion

\iota

preserves coproducts:

\Z \oplus \Z

is the coproduct of

\Z

and

\Z

\cat{Grp}

.Abelianisation preserves all products:

(\prod_i G_i)^{\mathrm{ab}} \cong \prod_i G_i^{\mathrm{ab}}

for every family of groups.

7. Adjunctions

StretchHuman

In proving that unit and counit with the triangle identities give an adjunction, we show $\varepsilon_B \circ F(Gk \circ \eta_A) = k$ for $k : FA \to B$ . The computation is $\varepsilon_B \circ FGk \circ F\eta_A = k \circ \varepsilon_{FA} \circ F\eta_A = k$ . Which facts justify the two equalities, in order?

Choose one

Naturality of

\varepsilon

k

; then the first triangle identityNaturality of

\eta

; then the second triangle identityFunctoriality of

F

twiceThe hom-set bijection, applied twice

8. Adjunctions

CoreFormal

Mathlib defines GaloisConnection l u for maps l : α → β and u : β → α between preorders. Which proposition is it?

Choose one

∀ a b, l a ≤ b ↔ a ≤ u b∀ a, u (l a) = a∀ a b, a ≤ b ↔ l a ≤ l b∀ a b, l a ≤ b → a ≤ u b

9. Adjunctions

CoreComputational

Write right_adjoint(l, P, Q, le_p, le_q) for a monotone map l (a dict) from a finite poset P to a finite poset Q. Return the dict u with l[a] ≤ b ⟺ a ≤ u[b] if it exists, using u[b] = max{a : l[a] ≤ b}, and None otherwise (including when that maximum does not exist).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Every functor has an adjoint." Most do not. A right adjoint must preserve all limits and a left adjoint all colimits, which rules out, for example, a free field ( $\cat{Field}$ has no initial object), any adjoint of $X \mapsto X \sqcup \{\ast\}$ on $\cat{Set}$ , and a right adjoint of the forgetful functor $\cat{Grp} \to \cat{Set}$ .

Misconception

Mixing up left and right. In a free–forgetful adjunction the free functor is the left adjoint: maps out of a free object are easy ( $\Hom(FS, M) \cong \Hom(S, UM)$ ). A useful check: the left adjoint is the one written on the left inside $\Hom$ , it preserves colimits (the free group on a disjoint union is a free product), and its unit $A \to GFA$ ("insert generators") goes from the original object.

Misconception

"An adjunction is an equivalence." Its unit and counit need not be isomorphisms. The unit $S \to UF(S)$ of the free monoid adjunction is never surjective (the empty word is missing), and $\iota(\lfloor x \rfloor) \le x$ is strict for non-integers. By Theorem 4, an adjunction is an equivalence exactly on the objects where unit and counit are invertible.

Misconception

"Adjoint" in category theory means the same as in linear algebra. For an operator on an inner product space, $\langle T v, w \rangle = \langle v, T^* w \rangle$ is formally similar to $\Hom(FA, B) \cong \Hom(A, GB)$ — and the categorical name was chosen with this analogy in mind — but it is only an analogy: the linear adjoint is an equation between numbers, the categorical one a natural bijection between sets of arrows.

ViewpointsH

Viewpoints

Logic— Quantifiers and implication are adjoints

Order formulas with free variables in a context by entailment. Weakening a formula $\psi(y)$ to a context with an extra variable $x$ is a monotone map $w$ , and the quantifiers are its adjoints: $\exists x\,\varphi \vdash \psi$ iff $\varphi \vdash w(\psi)$ , and $w(\psi) \vdash \varphi$ iff $\psi \vdash \forall x\,\varphi$ (for $x$ not free in $\psi$ ). So $\exists \dashv w \dashv \forall$ — Lawvere's observation (1969), and exactly the image–preimage triple $f_! \dashv f^{-1} \dashv f_*$ for a projection. Similarly, implication is right adjoint to conjunction: $\chi \wedge \varphi \vdash \psi$ iff $\chi \vdash \varphi \Rightarrow \psi$ . A lattice in which every $- \wedge a$ has a right adjoint is a Heyting algebra, the algebra of intuitionistic logic, and this is the propositional shadow of currying. See categorical logic.

Topology— Compactifications, mapping spaces and loops

The Stone–Čech compactification $\beta X$ is the left adjoint of the inclusion of compact Hausdorff spaces into all spaces: every continuous map from $X$ to a compact Hausdorff space extends uniquely over $\beta X$ . For a locally compact Hausdorff space $Y$ , the compact-open topology makes $- \times Y \dashv C(Y, -)$ : continuous maps $X \times Y \to Z$ correspond to continuous maps $X \to C(Y, Z)$ — currying for spaces, and the reason homotopies $X \times [0,1] \to Z$ are paths in mapping spaces. In pointed spaces, reduced suspension is left adjoint to the loop space: $[\Sigma X, Y]_\ast \cong [X, \Omega Y]_\ast$ . This adjunction underlies the definition of homotopy groups ( $\pi_{n+1}(Y) \cong \pi_n(\Omega Y)$ ) and of spectra in stable homotopy theory. See homotopy theory.

Algebra— Free objects, scalars and Frobenius reciprocity

Every variety of algebras (groups, rings, modules, lattices…) has free objects, and "free ⊣ forgetful" is the categorical form of "a homomorphism is determined freely by its values on generators". For a ring homomorphism $R \to S$ , extension of scalars $S \otimes_R -$ , restriction of scalars, and coextension $\Hom_R(S, -)$ form an adjoint triple. For a subgroup $H \le G$ of a finite group, induction and restriction of representations are adjoint — Frobenius reciprocity, $\Hom_G(\mathrm{Ind}_H^G W, V) \cong \Hom_H(W, \mathrm{Res}_H^G V)$ — which in character theory becomes the equality of inner products $\langle \mathrm{Ind}\,\chi, \psi \rangle_G = \langle \chi, \mathrm{Res}\,\psi \rangle_H$ . See representation theory.

Geometry— Ideals and varieties

Let $k$ be a field and $X = k^n$ . Sending a set of polynomials $T \subseteq k[x_1, \dots, x_n]$ to its zero set $V(T) \subseteq X$ , and a set of points $S$ to the ideal $I(S)$ of polynomials vanishing on it, gives an antitone Galois connection: $S \subseteq V(T) \iff T \subseteq I(S)$ . By Theorem 4 it restricts to a bijection between the closed sets on the two sides. On the geometric side the closed sets are the algebraic sets (Zariski-closed sets). When $k$ is algebraically closed, Hilbert's Nullstellensatz identifies the closed sets on the algebraic side as the radical ideals, giving the dictionary between algebra and geometry on which algebraic geometry is built. Over $\R$ it fails: $x^2 + 1$ generates a radical ideal with empty zero set.

Analysis— Completion as a best approximation

Every metric space $X$ has a completion $\widehat{X}$ , and every uniformly continuous map from $X$ to a complete metric space extends uniquely to $\widehat{X}$ . That is a universal arrow, so completion is left adjoint to the inclusion of complete metric spaces into metric spaces with uniformly continuous maps; $\R$ is the completion of $\Q$ , and the unit $\Q \to \R$ is not surjective. The adjunction explains why limits computed in $\Q$ and in $\R$ can differ, and why every construction "by continuity" (extending $x \mapsto 2^x$ from $\Q$ to $\R$ , defining integrals from step functions, $L^p$ from continuous functions) is well defined. On the order side, floor and ceiling are the simplest analytic adjunctions: $\lfloor x \rfloor \le x \le \lceil x \rceil$ are counit and unit, and an estimate such as $\lfloor x \rfloor > x - 1$ is the universal property in disguise (if $\lfloor x \rfloor + 1 \le x$ , then $\lfloor x \rfloor + 1 \le \lfloor x \rfloor$ ).

Computation— Currying and closed categories

In typed functional programming, curry : ((a, b) -> c) -> (a -> b -> c) and uncurry are the two directions of the adjunction $- \times B \dashv (-)^B$ ; its counit is function application and its unit is pairing. Cartesian closed categories, where these adjoints exist for all objects, are the models of the simply typed λ-calculus (Lambek, 1980), and monads arising from adjunctions describe computational effects. See the λ-calculus.

Wonder Trails

Wonder Trail · Optional · never gradedThe product, by its mapsCan you describe the set of pairs

A \times B

without ever looking inside it — only by how functions go into it?Follow the trail

History & global context

History and global context

Galois connections are named after Évariste Galois, whose correspondence between subgroups and fields (1830s) is the classical example. The abstract order-theoretic notion was isolated by Garrett Birkhoff (polarities, 1940) and Øystein Ore, who named "Galois connexions" in 1944.
Daniel Kan's paper "Adjoint functors" (1958), written while he was developing simplicial homotopy theory, introduced the notion together with limits and colimits in general categories; the relation between tensor products and hom-groups of abelian groups was a guiding example.
Peter Freyd proved the general adjoint functor theorem (1964). F. William Lawvere showed that the quantifiers and many logical and set-theoretic constructions are adjoints ("Adjointness in foundations", 1969). Eduard Čech and Marshall Stone (1937) constructed the compactification now seen as a left adjoint; Ferdinand Georg Frobenius found his reciprocity law for characters in 1898.

The best approximation from either side

Galois connections first

Definitions

Examples

Theorems and proofs

Adjunctions in Lean and Mathlib

Experiments: adjoints by exhaustion

Explore: ceiling ⊣ inclusion ⊣ floor

Exercises

Common misconceptions

Viewpoints

Wonder Trails

History and global context

Further reading