Universal Arrow

definition theorem proof

A universal arrow from $L$ to $c$ (for a functor $L:\mathcal{D}\to \mathcal{C}$ and object $c$) is a Terminal Object $(t,\tau :Lt\to c)$ in the Comma Category $L\downarrow c$: for every $f:Ld\to c$ there is a unique $h:d\to t$ with $f=\tau \circ Lh$. Equivalently, the map $h\mapsto \tau \circ Lh$ is a bijection $\mathcal{D}(d,t)\cong \mathcal{C}(Ld,c)$. Dually a universal arrow from $c$ to $R$ is an initial object $(t,\eta :c\to Rt)$ in $c\downarrow R$.

Sources: DaoFP §10.6 (“Adjunctions Using Universal Arrows”), §10.8; 7 Sketches Definition 3.86/3.92 (products and limits are universal cones), §3.6 (“universal constructions”); Kittenlab Lecture 8, 11 (universal objects “with these mappings”).

Theorem (DaoFP). (1) If $L⊣R$ then for every $c$, $(Rc,{\epsilon }_c)$ is a universal arrow from $L$ to $c$. (2) Conversely, if every $c$ has a universal arrow $(t_c,{\epsilon }_c)$ from $L$, then $Rc:=t_c$ extends to a functor right adjoint to $L$, and the ${\epsilon }_c$ are automatically natural and form the counit.

Proof of (1). Naturality of ${\varphi }_{d,c}:\mathcal{C}(Ld,c)\to \mathcal{D}(d,Rc)$ in $d$ gives, for $h:d\to d^{\prime }$, the square ${\varphi }_{d,c}(f^{\prime }\circ Lh)={\varphi }_{d^{\prime },c}(f^{\prime })\circ h$. Apply the Yoneda trick with $d^{\prime }:=Rc$ and the identity ${\mathrm{id}}_{Rc}$: the upper-left corner becomes ${\epsilon }_c={\varphi }^{-1}({\mathrm{id}}_{Rc})$, the lower-right $h$, the upper-right its mate $f$, so $f={\epsilon }_c\circ Lh$; uniqueness because $\varphi$ is a bijection. $■$

The unit and counit of an Adjunction are thus its universal arrows (Unit and Counit of an Adjunction). Limits are universal cones (terminal in the cone category), colimits universal cocones, evaluation $\epsilon :b^a\times a\to b$ is the universal arrow from $(-\times a)$ to $b$, and the free monoid’s insertion of generators is the universal arrow from a set to the forgetful functor. Kittenlab’s “coequalizing morphism” $e:B\to C$ is the universal arrow characterizing the Coequalizer without carrying a whole natural isomorphism around.

Lean

#check CategoryTheory.Adjunction.adjunctionOfEquivLeft    -- adjunction from a family of universal arrows
#check CategoryTheory.CostructuredArrow                    -- the comma category L ↓ c
#check CategoryTheory.Limits.IsTerminal                    -- a universal arrow is a terminal object in it