Solution (source code)

= Solution

The <Freyd general adjoint functor theorem> is as follows. Let $G:\mathcal D\to\mathcal C$, with $\mathcal D$ a <complete category> which is <locally small>. Then $G$ has a <left adjoint> if and only if it preserves all small <categorical limits> and satisfies the <solution-set condition>: for each $c\in\mathcal C$, there is a set-indexed family
$$
u_i:c\to Gd_i
$$
such that every $u:c\to Gd$ can be written $u=G(h)u_i$ for some $i$ and some $h:d_i\to d$. The target <category> need not be complete. We prove all the existence steps.

First establish the <initial-object lemma for complete categories with a weakly initial set>. Let $\mathcal E$ be <locally small> and complete, with a <weakly initial set> $\{w_i\}$, meaning every object receives a map from at least one $w_i$. Its <categorical product> $w=\prod_iw_i$ is weakly initial: compose a <categorical product> projection with the map from the appropriate $w_i$. Local smallness makes $\mathcal E(w,w)$ a <set>. Let $e:v\to w$ be the simultaneous <equaliser> of every <endomorphism> of $w$ and the identity. Explicitly it is the <equaliser> of the two arrows
$$
w\rightrightarrows\prod_{k\in\mathcal E(w,w)}w
$$
with components $k$ and $1_w$. Thus $ke=e$ for every <endomorphism> $k$, and $e$ is monic.

Every object $x$ receives a <morphism> from $v$, by composing $e$ with a map $w\to x$. To prove uniqueness, take parallel maps $a,b:v\to x$ and their <equaliser> $m:y\to v$. Weak initiality of $w$ gives $t:w\to y$. The composite $emt$ is an <endomorphism> of $w$, so $(emt)e=e$. Cancelling the <monomorphism> $e$ gives $mte=1_v$. Hence $m$ is both monic and a <split epimorphism>, and is therefore invertible. Since $am=bm$, this forces $a=b$. We have proved $v$ is initial, without using a class-sized <categorical product> or <equaliser>.

For sufficiency in the theorem, fix $c$ and consider the <comma category> $(c\downarrow G)$. Its objects are pairs $(d,u:c\to Gd)$; a <morphism> $h:(d,u)\to(d',u')$ satisfies $G(h)u=u'$. This <category> is <locally small> because each <hom-set> is a subset of $\mathcal D(d,d')$. It is complete: for a small diagram of such pairs, take the underlying <categorical limit> $d$ in $\mathcal D$. The arrows from $c$ form a cone to its image under $G$, and preservation of the <categorical limit> gives a unique $u:c\to Gd$ inducing them. The same <universal property> gives all mediators in the <comma category>. The solution-set family is a <weakly initial set> in this <comma category>, so the lemma supplies an initial pair
$$
(Fc,\eta_c:c\to GFc).
$$
For $f:c\to c'$, initiality defines a unique $Ff:Fc\to Fc'$ satisfying $G(Ff)\eta_c=\eta_{c'}f$. Uniqueness proves the identity and composition laws, making $F$ a <functor>. Initiality also gives <bijections>
$$
\boxed{\mathcal D(Fc,d)\cong\mathcal C(c,Gd),\qquad h\longmapsto G(h)\eta_c.}
$$
The definition of $Ff$ proves <naturality> in $c$, and postcomposition proves <naturality> in $d$. These <bijections> are the required <adjunction> $F\dashv G$.

For necessity, if $F\dashv G$, the single arrow $\eta_c:c\to GFc$ is a solution <set>: the transpose of any $u:c\to Gd$ gives its factorization through $\eta_c$. If $d$ is a limiting cone vertex of a small diagram $D_j$ in $\mathcal D$, then, naturally in $c$,
$$
\mathcal C(c,Gd)\cong\mathcal D(Fc,d)
\cong\lim_j\mathcal D(Fc,D_j)
\cong\lim_j\mathcal C(c,GD_j).
$$
These are the canonical cone-factorization <bijections>, so $Gd$ with its image projections is a <categorical limit> of $GD_j$. Thus $G$ preserves all small <categorical limits>, completing both directions of the theorem.