Adjunction

definition example theorem proof

Let $L:\mathcal{C}\to \mathcal{D}$ and $R:\mathcal{D}\to \mathcal{C}$ be functors. $L$ is left adjoint to $R$ (and $R$ right adjoint to $L$), written $L⊣R$, if for all $c\in \mathcal{C}$, $d\in \mathcal{D}$ there is an isomorphism of hom-sets

$${\alpha }_{c,d}:\mathcal{C}(c,R(d))\stackrel{\cong }{\to }\mathcal{D}(L(c),d)$$

natural in $c$ and $d$ (as functors ${\mathcal{C}}^{\mathrm{op}}\times \mathcal{D}\to \mathbf{Set}$: for $f:c^{\prime }\to c$, $h:c\to Rd$ and $g:d\to d^{\prime }$, ${\alpha }_{c^{\prime },d^{\prime }}(f;h;Rg)=Lf;{\alpha }_{c,d}(h);g$). The image ${\alpha }_{c,d}(h)$ of $h:c\to Rd$ is its mate (DaoFP: transpose), and vice versa. The turnstile $⊣$ always points from the left adjoint to the right adjoint.

Intuition (Category Theory for Scientists §5.1): adjoint functors are dictionaries between categories that are not on the same conceptual level, like a baby’s repeatable noises and an adult’s meaningful words. The left adjoint promotes every noise to a word of unknown meaning (“I wonder what she means by Ronnon”), the right adjoint forgets the meaning of words and hears them as noises. The hom-set bijection says: a way to interpret the freely-promoted words in our lexicon is the same as a way for the baby to emulate our sounds.

Sources: 7 Sketches §3.4.2 (Definition 3.70, Examples 3.71–3.74, Exercise 3.73), §3.4.3; DaoFP Chapter 10 (§10.1–10.11), §15 (monads from adjunctions); CTfS §5.1 (Definition 5.1.1.1, Proposition 5.1.1.2, Examples 5.1.1.4–5.1.1.7, §5.1.1.10 quantifiers, §5.1.2–5.1.4); Kittenlab (implicitly: Lecture 5 discrete/codiscrete, Lecture 7 free monoid unit). Preorder case: Galois Connection (“Galois connections and adjunctions between the corresponding categories are exactly the same thing”, Example 3.71: hom-sets with one or zero elements).

Examples

• Currying (Example 3.72, DaoFP §10.1): $(-\times B)⊣(-{)}^B$ on $\mathbf{Set}$, $\mathbf{Set}(A\times B,C)\cong \mathbf{Set}(A,C^B)$; “if you give me just $a$, I’ll return a function $B\to C$ waiting for the $B$ input”. Defines the Exponential Object and cartesian closed categories; $\mathbf{Cat}$ is one too, with $[\mathcal{D},\mathcal{E}]$ (7S Exercise 3.73: on morphisms $f\times B$ and $f^B=(-;f)$; currying $+$ gives $p(3)=(n\mapsto n+3)$).
• Sum and product (DaoFP §10.2): $(+)⊣\Delta ⊣(\times )$ with the Diagonal Functor; more generally $\mathrm{Colim}⊣\Delta ⊣\mathrm{Lim}$ (§10.4).
• Free/forgetful (Example 3.74, DaoFP §10.9): free group, monoid, ring, vector space $⊣$ underlying set; free category and free preorder on a graph $⊣$ underlying graph; discrete $⊣$ underlying $⊣$ codiscrete (preorders, graphs, categories, topological spaces); abelianization $⊣$ inclusion $\mathbf{Ab}\hookrightarrow \mathbf{Grp}$; Preorder Reflection $⊣$ inclusion. See Free-Forgetful Adjunction.
• Data migration (§3.4.3): ${\Sigma }_F⊣{\Delta }_F⊣{\Pi }_F$ (Data Migration Functor); Kan extensions generalize.
• ${\Sigma }_f$ $⊣f^{\ast }⊣$ ${\Pi }_f$ (DaoFP Ch. 11), ${\exists }_f⊣f^{\ast }⊣{\forall }_f$ for subsets; $(-\otimes a)⊣\underline{\mathrm{Hom}}(a,-)$ in a Monoidal Closed Category.
• Not every adjunction is symmetric (CTfS Example 5.1.1.4): $\mathrm{List}⊣U$ for $U:\mathbf{Mon}\to \mathbf{Set}$, but $\mathrm{List}$ is not right adjoint to $U$: the trivial monoid $1$ is initial, so $\mathbf{Mon}(1,\mathrm{List}\{a,b\})$ has one element while $\mathbf{Set}(U1,\{a,b\})$ has two.
• Some functors have adjoints on both sides (CTfS Examples 5.1.1.5–5.1.1.7, CTfS Exercise 5.1.1.6): discrete $⊣$ underlying set $⊣$ indiscrete for preorders; for graphs, the vertex-set functor has left adjoint “no arrows” and right adjoint “one arrow between every ordered pair”; $\mathrm{Disc}⊣\mathrm{Ob}⊣\mathrm{Ind}$ for $\mathbf{Cat}$, and ${\pi }_0⊣\mathrm{Disc}$ (connected components, CTfS Exercise 5.1.1.9).
• Every adjunction gives a Monad $RL$ and a Comonad $LR$ (DaoFP Ch. 15–16); every monad arises this way (Eilenberg-Moore Category, Kleisli Category).

Equivalent formulations (DaoFP §10.5–10.6)

• Unit and counit: $\eta :\mathrm{Id}\Rightarrow RL$ with ${\eta }_c:={\alpha }^{-1}({\mathrm{id}}_{Lc})$, and $\epsilon :LR\Rightarrow \mathrm{Id}$ with ${\epsilon }_d:=\alpha ({\mathrm{id}}_{Rd})$ (the Yoneda trick), satisfying the triangle identities $(\epsilon \circ L)\cdot (L\circ \eta )={\mathrm{id}}_L$ and $(R\circ \epsilon )\cdot (\eta \circ R)={\mathrm{id}}_R$. Conversely such $\eta ,\epsilon$ give the hom-set bijection: $f:c\to Rd\mapsto {\epsilon }_d\circ Lf$ and $g:Lc\to d\mapsto Rg\circ {\eta }_c$ (DaoFP Exercise 10.5.2). This definition works in any 2-Category. See Unit and Counit of an Adjunction.
• Universal arrows: $L⊣R$ iff for every $d$ there is a terminal object $(Rd,{\epsilon }_d)$ in the Comma Category $L\downarrow d$ — a Universal Arrow from $L$ to $d$; dually initial objects $(Lc,{\eta }_c)$ in $c\downarrow R$. An adjunction is a “half-equivalence”: if $\eta ,\epsilon$ are isomorphisms it is an Equivalence of Categories.

Properties

• Right Adjoints Preserve Limits and left adjoints preserve colimits (DaoFP §10.7; preorder version Right Adjoints Preserve Meets). Hence e.g. distributivity $(b+c)\times a\cong b\times a+c\times a$, since $(-\times a)$ is a left adjoint.
• Adjoints are unique up to natural isomorphism (7S Exercise 1.110 for preorders).
• Adjunctions compose: $L^{\prime }⊣R^{\prime }$ and $L⊣R$ give $(L^{\prime }\circ L)⊣(R\circ R^{\prime })$; categories and adjunctions form $\mathbf{Adj}(\mathbf{Cat})$ (DaoFP §10.10).
• Existence: the Adjoint Functor Theorem (Freyd) — a limit-preserving functor from a complete category with a solution set has a left adjoint; preorder case Adjoint Functor Theorem for Preorders; programming instance: Defunctionalization.
• $Lx$ represents the co-presheaf $y\mapsto \mathcal{C}(x,Ry)$ and $Ry$ represents the presheaf $x\mapsto \mathcal{D}(Lx,y)$ (DaoFP Exercise 10.3.2, DaoFP Exercise 10.3.3).

“Universal constructions are one of the most important themes of category theory: one gives some specified shape and says ‘find me the best solution!’; category theory asks ‘approximate from the left or the right?‘” (7 Sketches §3.6). “A sculptor subtracts irrelevant stone until a sculpture emerges” (DaoFP Ch. 10).

JuliaLeanHaskell

Docs: FinCats · C-set morphisms · Data migration · ACSets API · Graphs

# Catlab: adjunctions appear as Σ ⊣ Δ ⊣ Π data migrations and as free/forgetful constructions
# (checked with Catlab 0.16.20)
using Catlab
@present SchDDS(FreeSchema) begin State::Ob; next::Hom(State, State) end
@acset_type DDS(SchDDS)
F = FinFunctor(Dict(:V => :State, :E => :State), Dict(:src => id(SchDDS[:State]), :tgt => :next),
               FinCat(SchGraph), FinCat(SchDDS))
Δ = DeltaMigration(F); Σ = SigmaMigrationFunctor(F, Graph, DDS)
G = cycle_graph(Graph, 3)          # Σ(G) is the free DDS on G: here the 3-cycle
I = @acset DDS begin State = 3; next = [2, 3, 1] end
# the adjunction Σ ⊣ Δ:  Hom(Σ G, I) ≅ Hom(G, Δ I)
length(homomorphisms(Σ(G), I)) == length(homomorphisms(G, migrate(Graph, I, Δ)))  # true (3 = 3)
# (on path_graph(Graph, 3) the free DDS is infinite — the last state needs a fresh `next` — and the chase does not terminate)

#check CategoryTheory.Adjunction          -- structure: homEquiv, unit, counit, triangle laws; notation F ⊣ G
#check CategoryTheory.Adjunction.mkOfHomEquiv
#check CategoryTheory.Adjunction.mkOfUnitCounit
#check CategoryTheory.Adjunction.leftAdjointPreservesColimits
#check CategoryTheory.Adjunction.rightAdjointPreservesLimits
#check CategoryTheory.Adjunction.comp     -- composition of adjunctions
#check CategoryTheory.Adjunction.toMonad
-- currying: (- × B) ⊣ (B ⟶ -) in a cartesian closed category
#check CategoryTheory.exp.adjunction

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
-- DaoFP §10.3/§10.5: an adjunction between endofunctors, hom-set form and unit/counit form
class (Functor left, Functor right) => Adjunction left right | left -> right, right -> left where
  ltor   :: (left x -> y) -> (x -> right y)
  rtol   :: (x -> right y) -> (left x -> y)
  unit   :: x -> right (left x)
  counit :: left (right x) -> x
  ltor g = fmap g . unit
  rtol f = counit . fmap f
 
-- the currying adjunction (- , r) ⊣ (r -> -)
data L r x = L (x, r) deriving Functor
data R r x = R (r -> x) deriving Functor
instance Adjunction (L r) (R r) where
  unit x = R (\r -> L (x, r))
  counit (L (R f, r)) = f r
 
-- triangle identities (should be identities):
triangle  :: L r x -> L r x
triangle  = counit . fmap unit
triangle' :: R r x -> R r x
triangle' = fmap counit . unit