Solution (source code)

= Solution

The <general adjoint functor theorem> says that, for a <functor> $U:\mathcal C\to\mathcal D$ with $\mathcal C$ a <complete category> and both categories <locally small>, $U$ has a <left adjoint> exactly when it preserves small <categorical limits> and satisfies the <solution-set condition>. The latter means that for each $D\in\mathcal D$ there is a set of arrows $f_i:D\to U(C_i)$ such that every $f:D\to U(C)$ factors as
$$
f=U(h)f_i\quad\text{for some }i\text{ and }h:C_i\to C.
$$
Equivalently, $(D\downarrow U)$ has a <weakly initial set>.

The <limit form of the special adjoint functor theorem> says that, if in addition $\mathcal C$ is <well-powered> and has a <small cogenerating family>, then \b[$U$ has a left adjoint exactly when it preserves small limits]. These are the limit/left-adjoint forms; their duals interchange limits with <colimits>, left with <right adjoints>, and cogenerators with generators.

For the first route, let $\mathcal E$ be a <complete category> that is <locally small> and has a <weakly initial set> $(W_i)$. Put $P=\prod_iW_i$. It is weakly initial: for any $X$, choose an arrow $W_i\to X$ and precompose with the corresponding product projection. The <set> $\mathcal E(P,P)$ indexes a simultaneous <equalizer>
$$
e:E\longrightarrow P,\qquad ue=e\quad\text{for every }u:P\to P.
$$
It exists by completeness, for example as the equalizer of the two maps $P\rightrightarrows\prod_{u:P\to P}P$ with components $u$ and $1_P$. Since $E\to P\to X$ exists for each $X$, $E$ is also weakly initial.

Choose $r:P\to E$. Applying the defining equation to $er:P\to P$ gives $ere=e$, whence $re=1_E$ because $e$ is a <monomorphism>. If $v:E\to E$ is any endomorphism, apply it to $evr:P\to P$ to obtain $evre=e$, hence $ev=e$ and $v=1_E$. Thus $E$ has only its identity endomorphism.

For two arrows $a,b:E\rightrightarrows X$, take their <equalizer> $j:Y\to E$. Weak initiality of $E$ gives $t:E\to Y$. Since $jt$ is an endomorphism of $E$, $jt=1_E$. The monic arrow $j$ with this right inverse is invertible; therefore $a=b$. Existence of an arrow $E\to X$ and this uniqueness show that \b[$E$ is initial].

For the <general adjoint functor theorem>, limit preservation makes each <comma category> $(D\downarrow U)$ complete, and the <solution-set condition> makes it weakly initially generated by a set. The lemma provides an <initial object> $(FD,\eta_D)$. For $v:D\to D'$, the <universal property> uniquely defines $Fv:FD\to FD'$ by
$$
U(Fv)\eta_D=\eta_{D'}v.
$$
Uniqueness gives the <functor> laws. The same property gives natural <bijections>
$$
\mathcal C(FD,C)\cong\mathcal D(D,UC),
$$
so $F\dashv U$. Conversely a <right adjoint> preserves limits, by applying its <hom-set> bijections to cones, and its unit $(FD,\eta_D)$ is already an initial object of each comma category, hence a singleton solution set. This proves necessity as well as sufficiency.

For the second route, assume the <general adjoint functor theorem> and the additional hypotheses of the <Special adjoint functor theorem>. Let $(Q_i)_{i\in I}$ be a <small cogenerating family>. Fix $D\in\mathcal D$ and an arrow $f:D\to UC$. A limit-preserving <functor> preserves <monomorphisms>, by the self-pullback criterion. Intersect the set of all <subobjects> $B\hookrightarrow C$ supporting $f$. Preservation of this <categorical limit> gives a minimal supporting pair $(C_0,f_0:D\to UC_0)$ and a monomorphism $m_0:C_0\to C$ with $U(m_0)f_0=f$.

If $g,h:C_0\rightrightarrows Q_i$ have $Ug f_0=Uh f_0$, their <equalizer> supports $f_0$ and must be invertible by minimality. Thus
$$
\mathcal C(C_0,Q_i)\hookrightarrow\mathcal D(D,UQ_i),\qquad
h\longmapsto Uh f_0.
$$
The evaluation map into the product of all these cogenerator targets is monic, because the family coseparates arrows. Its coordinates inject into the fixed set
$$
B_D=\coprod_{i\in I}\mathcal D(D,UQ_i).
$$
For every subset $J\subseteq B_D$, form the product $P_J$ whose coordinate $(i,z)$ has target $Q_i$. Each minimal $C_0$ is isomorphic to a <subobject> of one such product, using precisely its realized coordinates. There is a set of subsets $J$; the <well-powered category> condition gives a set of representative subobjects of each product. For each representative $B$, include every arrow $D\to UB$, a set by local smallness of $\mathcal D$.

This is a <solution-set condition>: the minimal pair is isomorphic to one of these representatives, and its inclusion into $C$ supplies the required factorization of $f$. The <general adjoint functor theorem> now gives the <left adjoint>. This is the <cogenerator bound for comma-category solution sets> proof of the special theorem. Necessity follows again because a <right adjoint> preserves limits. Both alternative proof routes are therefore supplied.