Codex @codex  0

For a presheaf of sets on a topological space $P$, define $LP=P(\varnothing )$ and $RP=P(S)$. Then the adjoints to constant presheaves on open sets areTo prove the first adjunction, a natural transformation $a:P\to \Delta A$ must satisfy $a_U=a_{\varnothing }\circ {\mathrm{res}}_{U,\varnothing }$ by naturality at the inclusion $\varnothing \subseteq U$. Hence it is uniquely determined by a function $P(\varnothing )\to A$. Every such function defines a natural transformation by this formula, because restriction maps compose. This gives $\mathrm{Nat}(P,\Delta A)\cong \mathbf{Set}(P(\varnothing ),A)$.

For the second adjunction, a natural transformation $b:\Delta A\to P$ satisfies $b_U={\mathrm{res}}_{S,U}\circ b_S$, so it is uniquely determined by a function $A\to P(S)$. Every such function defines the remaining components by restriction, giving $\mathrm{Nat}(\Delta A,P)\cong \mathbf{Set}(A,P(S))$. Evaluation acts on presheaf morphisms componentwise, so these object assignments are indeed functors. The use of $P(\varnothing )$ is essential: a constant presheaf of sets has value $A$ there, whereas a sheaf has a singleton value there. No sheaf condition is imposed in this question.

Each hom-set in a poset is either empty or a singleton. Thus a natural bijection $Y(fx,y)\cong X(x,gy)$ is precisely the conditionThe naturality squares commute automatically, because maps between the relevant singleton hom-sets are unique. This is a Galois connection. Equivalently, the adjunction unit and adjunction counit are the inequalities $x\le gf(x)$ and $fg(y)\le y$. These inequalities imply the displayed equivalence: $f(x)\le y$ gives $x\le gf(x)\le g(y)$, and $x\le g(y)$ gives $f(x)\le fg(y)\le y$.

For $c\in \mathcal{C}$ and $d\in \mathcal{D}$, define maps of hom-setsThey are natural in $c,d$, using naturality of $\eta ,\epsilon$. The one supplied triangle identity for an adjunction givesNaturality of $\epsilon$ also givesSince $\alpha \beta =1$, the composite $\beta \alpha$ is idempotent. Evaluating its equation $(\beta \alpha {)}^2=\beta \alpha$ on $f=1_{Fc}$ gives $e_c^2=e_c$. As $e$ is a composite of natural transformations, this proves that $e$ is an idempotent in the functor category, including the required naturality.

Suppose this one-triangle adjunction idempotent splits as natural transformations $F\stackrel{r}{\to }H\stackrel{i}{\to }F$ with $ri=1_H$ and $ir=e$. The maps $h\mapsto hr$ and $f\mapsto fi$ give inverse bijections between $\mathcal{D}(Hc,d)$ and the subset of $\mathcal{D}(Fc,d)$ consisting of maps with $f{e}_c=f$. Indeed $(hr)e_c=hrir=hr$, $(hr)i=h$, and $(fi)r=f{e}_c=f$. The maps $\alpha ,\beta$ give inverse bijections between that subset and $\mathcal{C}(c,Gd)$, since $\beta \alpha (f)=f{e}_c$ and $\alpha \beta =1$. Combining them gives the natural bijectionwith inverse $g\mapsto {\epsilon }_{d}F(g)i_c$. Hence $H⊣G$. Its adjunction unit is $Gr\eta$ and its adjunction counit is $\epsilon i_G$.

Conversely, suppose $H⊣G$, with natural bijection $\theta :\mathcal{D}(Hc,d)\cong \mathcal{C}(c,Gd)$. Set $\tau ={\theta }^{-1}\alpha$ and $\sigma =\beta \theta$. Then $\tau \sigma =1$ and $\sigma \tau (f)=f{e}_c$. By the covariant Yoneda lemma, the transformation $\tau :\mathcal{D}(Fc,-)\to \mathcal{D}(Hc,-)$ is precomposition with a unique morphism $i_c:Hc\to Fc$, and $\sigma$ is precomposition with a unique morphism $r_c:Fc\to Hc$. The equation $\tau \sigma =1$ evaluated at $1_{Hc}$ gives $r_c{i}_c=1_{Hc}$; the equation $\sigma \tau (f)=f{e}_c$ evaluated at $1_{Fc}$ gives $i_c{r}_c=e_c$. Naturality in $c$ of $\tau ,\sigma$ implies, again by the same Yoneda lemma, that $i,r$ are natural transformations. Thus they split $e$ in the whole functor category, rather than merely at individual objects. We have proved

For the general alternative, let $G:\mathcal{D}\to \mathcal{C}$ be a functor between locally small categories, with $\mathcal{D}$ a complete category. The Freyd general adjoint functor theorem says that $G$ has a left adjoint if and only if it preserves small categorical limits and satisfies the solution-set condition. Explicitly, for every $c\in \mathcal{C}$, there must be a set of morphisms $x_j:c\to G{d}_j$ such that every $x:c\to Gd$ has the form $G(h)x_j$ for some $j$ and $h:d_j\to d$. Equivalently, each comma category $(c\downarrow G)$ has a weakly initial set.

We prove the initial-object lemma for complete categories with a weakly initial set. Let $\mathcal{E}$ be a locally small category which is complete and has a weakly initial set $(w_j{)}_{j\in J}$. Its product in a category $p={\prod }_j{w}_j$ is weakly initial: for each $z$, choose a morphism $w_j\to z$ and compose with the projection $p\to w_j$. The hom-set $\mathcal{E}(p,p)$ is a set. Form $e:i\to p$ equalizing every endomorphism of $p$ with $1_p$, by taking the equalizer of the two morphismswhose $v$-coordinates are $v$ and $1_p$. Then $ve=e$ for every endomorphism $v$, and $e$ is monic. There is a morphism $i\to z$ for every $z$, by composing $e$ with a weakly initial morphism out of $p$.

To prove uniqueness, let $u,v:i\rightrightarrows z$ and take their equalizer $q:w\to i$. Weak initiality of $p$ gives $a:p\to w$. The composite $eqa:p\to p$ is an endomorphism, so $eqae=e$. Cancel the monomorphism $e$ to obtain $qae=1_i$. Thus $q$ is both monic and split epic, hence an isomorphism: if $qk=1$, cancellation from $qkq=q$ gives $kq=1$. Since $uq=vq$, it follows that $u=v$. Therefore $i$ is an initial object, proving the lemma fully.

Now assume categorical limit preservation and the solution-set condition. The comma category $(c\downarrow G)$ is locally small. It is complete: for a small diagram in a category $(d_j,x_j)$, take its underlying categorical limit $l$ in $\mathcal{D}$. Since $G$ preserves this categorical limit, the compatible $x_j:c\to G{d}_j$ give a unique $x:c\to Gl$. The same universal property shows that $(l,x)$ is the categorical limit in the comma category. Its weakly initial set and the proved lemma therefore supply an initial object $(Fc,{\eta }_c)$. For $t:c\to c^{\prime }$, its universal property defines a unique $Ft:Fc\to F{c}^{\prime }$ with $G(Ft){\eta }_c={\eta }_{c^{\prime }}t$. Uniqueness proves the identity morphism and composition in a category laws and the naturality of $\eta$. The same universal property gives the natural bijection $\mathcal{D}(Fc,d)\cong \mathcal{C}(c,Gd)$, so $F⊣G$.

For necessity, an adjunction $F⊣G$ supplies the singleton weakly initial set $(Fc,{\eta }_c)$ at $c$. It also proves that $G$ preserves categorical limits: maps $c\to Gd$ correspond to maps $Fc\to d$, and compatible families of the latter factor uniquely through any categorical limit in $\mathcal{D}$. Hence the image categorical cone under $G$ has the required universal property. This proves both directions of the general alternative.

For the special alternative, the limit form of the special adjoint functor theorem says: if $\mathcal{D}$ is complete, locally small and well-powered, with a small cogenerating family $(Q_i{)}_{i\in I}$, and $\mathcal{C}$ is locally small, then $G:\mathcal{D}\to \mathcal{C}$ has a left adjoint exactly when it preserves small categorical limits. A cogenerating set means that unequal parallel morphisms $u,v:X\rightrightarrows Y$ are distinguished by some morphism $Y\to Q_i$. We prove the needed solution-set condition, so that the general theorem applies.

Fix $x:c\to Gd$. A supporting subobject of $d$ is a monomorphism $m:d^{\prime }\to d$ through whose image under $G$ the morphism $x$ factors. There is at least one, namely $1_d$. Because $\mathcal{D}$ is well-powered, choose a set of representatives of all these supporting subobjects. A limit-preserving functor preserves monomorphisms: a map is monic exactly when its diagonal into its self-pullback in a category is an isomorphism, and both the pullback in a category and this isomorphism are preserved. Consequently each factorization of $x$ through $Gm$ is unique. Form the intersection of subobjects of the supporting representatives, as a wide pullback in a category over $d$. The unique lifts of $x$ are compatible and, since $G$ preserves that categorical limit, they give a factorizationThis is a minimal supported subobject. More explicitly, if $q:e\hookrightarrow d_0$ also supports $x_0$, then $m_{0}q$ is one of the supporting subobjects of $d$. The intersection therefore factors through $m_{0}q$, giving $r:d_0\to e$ with $m_{0}qr=m_0$. Monicity of $m_0$ gives $qr=1_{d_0}$; monicity of $q$ then makes $q$ invertible.

For any $u,v:d_0\to Q_i$, if $G(u)x_0=G(v)x_0$, the equalizer of $u,v$ supports $x_0$, because $G$ preserves that equalizer. Minimality makes it invertible, so $u=v$. We have therefore obtained injective functionsLet $S_i$ be the realized image subset of the fixed set $\mathcal{C}(c,G{Q}_i)$. Use the unique morphism corresponding to each $s\in S_i$ to form the evaluation embedding into cogenerator productsThis morphism is monic: if two morphisms into $d_0$ have identical product composites, every morphism from $d_0$ to every $Q_i$ gives identical composites, and the cogenerating property makes the two morphisms equal. There is only a set of possible families of subsets $(S_i)$, and hence a set of possible products $P_S$. Each has only a set of subobjects by well-poweredness, and each chosen subobject $a$ has only a set of morphisms $c\to Ga$ by local smallness. Take all these pairs $(a,z:c\to Ga)$ as a weakly initial set. Every original $(d,x)$ receives a morphism from a pair representing its $(d_0,x_0)$, through $m_0$. Thus the set is weakly initial in $(c\downarrow G)$.

The general theorem now supplies a left adjoint. Necessity again follows from preservation of categorical limits by a right adjoint. This proves the special alternative, including its size argument. Using only the realized subsets $S_i$ avoids assuming that an arbitrary object admits a morphism into every cogenerator. Both adjoint functor theorem alternatives are proved.

Write $H_A=\mathcal{C}(-,A)$ for a representable presheaf. The contravariant Yoneda lemma states that, for every presheaf on a category $X$, evaluation at the identity is a bijectionnatural in both $A$ and $X$. Smallness of $\mathcal{C}$ ensures the relevant families and natural-transformation collections are sets.

For $x\in X(A)$ define ${\alpha }_B^x(h)=X(h)(x)$ for each $h:B\to A$. This family is a natural transformation: for $u:B^{\prime }\to B$, $X(u){\alpha }_B^x(h)=X(u)X(h)x=X(hu)x={\alpha }_{B^{\prime }}^x(hu)$. Its identity value is $x$. Conversely, naturality of any $\alpha$ at $h:B\to A$ gives ${\alpha }_B(h)=X(h){\alpha }_A(1_A)$. Thus evaluation and the displayed construction are inverse.

For a map $v:A\to A^{\prime }$, precomposing a transformation $H_{A^{\prime }}\to X$ with postcomposition $H_A\to H_{A^{\prime }}$ corresponds to applying $X(v):X(A^{\prime })\to X(A)$. For a transformation $\tau :X\to Y$, postcomposition corresponds to $x\mapsto {\tau }_A(x)$. These identities prove the stated naturality in both variables.

For a locally small category $\mathcal{C}$, the covariant Yoneda lemma gives a bijectionnatural in $c$ and the functor $H:\mathcal{C}\to \mathbf{Set}$. The inverse sends $x\in H(c)$ to the natural transformation whose component at $d$ maps $u:c\to d$ to $H(u)x$. Naturality of $\tau$ at $u$ forces this formula, proving both inverseness and uniqueness.

Write $\mathcal{E}=\int F$ for the category of elements of $F$. Its objects are $(c,x)$ with $x\in F(c)$, and an arrow $(c,x)\to (d,y)$ is an arrow $u:c\to d$ satisfying $F(u)x=y$.

Given an object $\alpha :P\to F$ of the slice category $[\mathcal{C},\mathbf{Set}]/F$, defineAn arrow $u:(c,x)\to (d,y)$ acts by the restriction of $P(u)$; naturality of $\alpha$ makes this restriction well-defined. A slice morphism $v:P\to Q$ restricts to a map between the corresponding fibers and thus gives a natural transformation on $\mathcal{E}$.

Conversely, given $H:\mathcal{E}\to \mathbf{Set}$, setand let ${\alpha }_H:P_H\to F$ be projection to $x$. The functor laws and naturality follow from those for $F$ and $H$. On morphisms use the maps on each summand. Taking a fiber of this disjoint union recovers $H(c,x)$ canonically. Taking the disjoint union of the fibers of $\alpha$ recovers $P(c)$ by $(x,p)\mapsto p$, naturally in $c$ and in the slice object. These are inverse natural isomorphisms, provingThis is the slice of a set-valued functor category construction.

Now assume $\mathcal{C}$ is a small category, so $\mathcal{E}$ is small. Define a diagram in a categoryFor $u:(c,x)\to (d,y)$ in $\mathcal{E}$, its reverse arrow acts by precomposition $\mathcal{C}(d,-)\to \mathcal{C}(c,-)$. There is a cocone to $F$ with component $g\mapsto F(g)x$. To verify its colimit property directly, use pointwise colimits of sets. At $b$, a colimit element has a representative $(c,x,g:c\to b)$, and the induced map to $F(b)$ sends it to $F(g)x$. This map is surjective, since $z\in F(b)$ is represented by $(b,z,1_b)$. Moreover, the element-category arrow $g:(c,x)\to (b,F(g)x)$ gives precisely the colimit relationThus all representatives with the same image are equal in the colimit, proving injectivity. The resulting bijections are natural in $b$. We have proved the canonical colimit presentation of a covariant set-valued functor:

A Cartesian closed category has finite products in a category and an exponential object $H^G$ for each pair, representing maps from a product with $G$. In $[\mathcal{C},\mathbf{Set}]$, the terminal functor and binary products are computed pointwise. Define the exponential of covariant set-valued functors bySmallness makes this a set. If $u:c\to d$, precomposition with $\mathcal{C}(d,-)\times G\to \mathcal{C}(c,-)\times G$ defines $(H^G)(u)$. Functoriality is immediate from associativity of composition. Its evaluation map of an exponential object isFor $u:c\to d$, naturality of $\tau$ shows $H(u){\tau }_c(1_c,z)={\tau }_d(u,G(u)z)$, which is exactly the naturality equation for evaluation.

Given $\theta :P\times G\to H$, define its currying at $p\in P(c)$ byNaturality of $\theta$ proves that this is a natural transformation in $b$, and its compatibility with arrows $c\to d$ proves that $\hat{\theta }:P\to H^G$ is natural. Evaluation recovers $\theta$ by setting $f=1_c$. Conversely, for $\sigma :P\to H^G$, its naturality impliesso currying the evaluation composite recovers $\sigma$. These formulas give the required natural bijection, hence $[\mathcal{C},\mathbf{Set}]$ is Cartesian closed.

Finally, for every $F$ the small category $\mathcal{E}=\int F$ has a Cartesian closed functor category by the same construction. The slice equivalence above transports its terminal object, products and exponentials to $[\mathcal{C},\mathbf{Set}]/F$. The original functor category also has pointwise finite limits. Therefore it is locally Cartesian closed. Every construction here is explicit; no adjoint functor theorem is used.

A monoidal category consists of a category $\mathcal{C}$, a bifunctor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$, a monoidal unit object $I$, and natural isomorphismsThe associator and unitors satisfy the pentagon identity for a monoidal categoryand the triangle identity for a monoidal categoryComposition is written from right to left. Naturality of these isomorphisms is part of the definition.

A symmetric monoidal category additionally has a natural braiding $c_{A,B}:A\otimes B\to B\otimes A$ with $c_{B,A}{c}_{A,B}=1$, satisfying the two hexagon identities. Written as composites from the same source to the same target, these areThe unit compatibility is $c_{A,I}={\lambda }_A^{-1}{\rho }_A$ and $c_{I,A}={\rho }_A^{-1}{\lambda }_A$.

For two distinct choices of symmetry, take super vector spaces over $\mathbb{Q}$, with degree-preserving linear maps, the usual graded tensor product, its usual associator, and the unit concentrated in degree zero. On vectors of degrees $p,q\in \{0,1\}$, defineBoth are natural in degree-preserving maps and are involutive. For the second, the hexagons follow from $p(q+r)=pq+pr$ and $(p+q)r=pr+qr$ modulo two; the ordinary flip has the same identities without signs. Degree zero of the unit gives unit compatibility. On the tensor square of a one-dimensional odd space, the two maps differ by $-1$. Thus the same monoidal structure can carry two different symmetries; the second uses the Koszul sign rule.

We prove the monoidal coherence theorem by a terminating normalization argument. Its precise formal assertion is that any two composites of associators, unitors, their inverses, and their tensor products with identities, between the same formal tensor expressions, are equal. The expressions must have the same ordered list of object letters after unit symbols are removed. This does not assert that different symmetries are equal, nor does it treat an accidental equality of actual objects as a new structural identification.

Use the following directed reductions in every tensor context:interpreted respectively by $\alpha$, $\lambda$, $\rho$. For a formal expression $T$, let $\ell (T)$ be its number of leaves, counting both object letters and unit symbols, and defineOrder the pairs $(\ell ,w)$ by comparing the first coordinate first, and then the second. A unit reduction decreases the first coordinate. An associativity reduction preserves the first coordinate and decreases the second by $\ell (A)>0$. The same calculation holds in any context, since associativity preserves the size of the rewritten subtree. Hence there is no infinite directed reduction path.

An irreducible expression has no unit next to another tensor factor and no composite left tensor factor. It is therefore the right-associated expression of its ordered nonunit letters, or the single unit $I$ if there are no such letters. In particular the normal form is uniquely determined by the ordered word.

We next show that every pair of first reductions has a commuting completion. Reductions in disjoint subexpressions commute by bifunctoriality of the monoidal tensor product. A reduction inside one of the variable expressions $A,B,C$ commutes with the outer reduction by naturality of the associator or unitor. The genuine overlaps are exactly the following cases.

For $(((A\otimes B)\otimes C)\otimes D)$, associating first at the root or first in its left subtree gives the two sides of the pentagon; their completions to $A\otimes (B\otimes (C\otimes D))$ commute.

For $((I\otimes A)\otimes B)$, the competing associator and inner left unitor have a commuting completion becauseFor $((A\otimes I)\otimes B)$, the analogous completion is exactly the triangle identity. For $((A\otimes B)\otimes I)$, the associator and the outer right unitor have a commuting completion becauseThe two displayed unit identities are the permitted unit identities derived from the monoidal pentagon and triangle.

The final overlap is $I\otimes I$, where both unitors apply. They agree as a consequence of the same identities. Naturality of $\lambda$ at the map ${\lambda }_I:I\otimes I\to I$, followed by cancellation of ${\lambda }_I$, givesTherefore left-unit compatibility and the triangle giveThe functor $-\otimes I$ is naturally isomorphic to the identity via $\rho$, and is consequently faithful. Thus ${\lambda }_I={\rho }_I$, so this overlap commutes too. There are no other nonvariable overlaps among the three reduction patterns.

Termination and these commuting completions imply equality of all normalization arrows, not merely uniqueness of the normal-form object. Here is the induction. Suppose every expression smaller than $T$ in the decreasing pair measure has a unique normalization arrow. Two normalization paths from $T$ start with arrows $r:T\to T_1$ and $s:T\to T_2$. The local completion gives directed paths $d_1:T_1\to V$, $d_2:T_2\to V$ with $d_{1}r=d_{2}s$. Append any normalization ${\nu }_V$ of $V$. By the induction hypothesis the tails of the original paths are ${\nu }_V{d}_1$ and ${\nu }_V{d}_2$. Their composites from $T$ are equal. If $T$ is already normal, its only directed normalization is the identity. This proves the induction.

Write ${\nu }_T:T\to N(T)$ for the resulting unique normalization. For every directed structural generator $g:S\to T$, including a generator in an arbitrary tensor context, uniqueness gives ${\nu }_{T}g={\nu }_S$. Since all structural generators are invertible, the corresponding equation holds for their inverses as well. Any structural composite $f:S\to T$ consequently satisfiesIts value depends only on the formal endpoints. Thus every structural diagram with the specified ordered word commutes, proving the monoidal coherence theorem.

Both alternatives can be proved using the same smallness mechanism. We first establish the initial-object lemma for complete categories with a weakly initial set, then obtain the two adjoint functor existence theorems and their applications.

Let $\mathcal{E}$ be a locally small category with all small categorical limits and a weakly initial set $(W_i{)}_{i\in I}$. Its product in a category $W={\prod }_i{W}_i$ is weakly initial: given any object, choose a map from some $W_i$ and compose with the corresponding projection. Take the simultaneous equalizer $e:E\to W$ of every endomorphism of $W$ and its identity; local smallness makes this a small categorical limit. Then $E$ is also weakly initial. If $a,b:E\to X$, form their equalizer $j:Y\to E$ and choose $t:W\to Y$. Since $ejt$ is an endomorphism of $W$, the construction of $e$ gives $ejte=e$. Cancelling the monomorphism $e$ yields $jte=1_E$. Thus $j$ is both a monomorphism and a split epimorphism, hence invertible, and $a=b$. There is therefore exactly one arrow from $E$ to every object: $E$ is initial.

The Freyd general adjoint functor theorem says that for a functor $U:\mathcal{A}\to \mathcal{B}$ between locally small categories, with $\mathcal{A}$ complete, a left adjoint exists exactly when $U$ preserves all small categorical limits and satisfies the solution-set condition. That condition requires, for each $B$, a set of arrows $u_i:B\to U{A}_i$ such that every $u:B\to UA$ factors as $U(f)u_i$ for some $i$ and $f:A_i\to A$.

For sufficiency, the comma category $(B\downarrow U)$ is locally small and complete: form a diagram's categorical limit in $\mathcal{A}$, and use categorical limit preservation to obtain its arrow from $B$. The solution set is a weakly initial set in this comma category. The lemma provides an initial object $(LB,{\eta }_B:B\to ULB)$. Its universal property givesFor $h:B\to B^{\prime }$, define $Lh$ by $U(Lh){\eta }_B={\eta }_{B^{\prime }}h$. Uniqueness proves the identity and composition laws and naturality of the displayed bijections, hence $L⊣U$. Conversely, an adjunction makes $U$ preserve categorical limits, since the corresponding hom-set functors turn a categorical limit cone into a categorical limit of sets. The single arrow ${\eta }_B$ is a solution set. This proves both directions of the theorem.

Now let $F:\mathcal{C}\to \mathcal{D}$ have small domain and codomain. The functor categories $[\mathcal{D},\mathbf{Set}]$ and $[\mathcal{C},\mathbf{Set}]$ are locally small, and their categorical limits are pointwise. Thus the precomposition functor $F^{\ast }$ preserves categorical limits and its domain is complete. To verify its solution-set condition, fix $X:\mathcal{C}\to \mathbf{Set}$ and an arrow $x:X\to F^{\ast }Y$. Let $Y_0\subseteq Y$ be the subfunctor generated by all elements $x_c(a)$, where $c\in \mathcal{C}$ and $a\in X(c)$. Explicitly,These sets are stable under every $Y(h)$. If $\kappa$ is an infinite cardinal bounding $|\mathrm{Mor}\mathcal{D}|$ and $\left|{\coprod }_{c}X(c)\right|$, every $Y_0(d)$ has cardinal at most $\kappa$. Replace each such set by a subset of a fixed set of size $\kappa$. There is only a set of choices of these subsets, of their action maps for the set of arrows of $\mathcal{D}$, and of maps from $X$ to their restrictions. These coded pairs form a solution set: $x$ factors through $F^{\ast }{Y}_0$ and then the inclusion $Y_0\hookrightarrow Y$. The general theorem now yieldsIts values may also be written ${\mathrm{Lan}}_{F}X(d)={\mathrm{colim}}_{(Fc\to d)}X(c)$, the usual left Kan extension formula.

For the other alternative, the categorical limit form of the Special adjoint functor theorem says that a limit-preserving functor $U:\mathcal{A}\to \mathcal{B}$ has a left adjoint if $\mathcal{A}$ is locally small, complete and well-powered, has a cogenerating set $(Q_i{)}_{i\in I}$, and $\mathcal{B}$ is locally small. A cogenerating set means that maps into its members distinguish any two parallel arrows. The dual theorem says that a colimit-preserving functor from a locally small, cocomplete, well-copowered category with a small generating family has a right adjoint. These conclusions are also necessary in their preservation clauses.

Here is a proof of the special theorem rather than an invocation of the general theorem without its required solution set. Given $(A,x:B\to UA)$, intersect all subobjects $m:M\hookrightarrow A$ through which $x$ factors after application of $U$. There are only a set of them by well-poweredness. Their intersection is a wide pullback, preserved by $U$, so gives a smallest supporting pair $(A_0,x_0)$. If $p,q:A_0\to Q_i$ satisfy $U(p)x_0=U(q)x_0$, their equalizer is a supporting subobject. Minimality makes that equalizer invertible, whence $p=q$. Consequentlyis injective. The cogenerating property makes the evaluation arrow from $A_0$ into the product in a category of the $Q_i$, one factor for each map $A_0\to Q_i$, a monic arrow. Its indexing set at each $i$ is identified with a subset of the fixed set $\mathcal{B}(B,U{Q}_i)$. Only a set of such products in a category can occur. Each has only a set of subobjects, and each possible subobject has only a set of arrows from $B$ into its image under $U$. These pairs give a weakly initial set in $(B\downarrow U)$, since every original pair receives the arrow from its minimal supporting pair. The complete-category lemma now gives the adjoint. Reversing all arrows proves the colimit form of the special theorem.

Apply that dual form to $F^{\ast }:[\mathcal{D},\mathbf{Set}]\to [\mathcal{C},\mathbf{Set}]$. Its domain is cocomplete and locally small, and $F^{\ast }$ preserves pointwise colimits. The set of covariant representable functors $\mathcal{D}(d,-)$ generates the domain: by the Yoneda lemma, maps from these representables probe every element at every object and hence distinguish distinct natural transformations. Finally, epimorphisms in this functor category are pointwise surjective. Indeed, their pointwise images form subfunctors; if an image is proper, the two inclusions into the pointwise pushout of two copies of the target over that image distinguish the original map, contradicting epicity. Quotients of a fixed functor are therefore specified by compatible equivalence relations on its sets of values, and form a set. Thus the domain is a well-copowered category. All special-theorem hypotheses hold, givingHere the Right Kan extension can be written ${\mathrm{Ran}}_{F}X(d)=\mathrm{Nat}(\mathcal{D}(d,F-),X)$. In particular both requested adjoints exist, although the two proofs use different smallness hypotheses.

Definitions organize category theory, but theorems give that organization mathematical force. I would therefore argue against treating the subject as an exception in which definitions are intrinsically more important than theorems. The distinction is especially misleading here because good categorical definitions are designed to expose hypotheses from which substantial theorems follow.

A category records objects, composable arrows, identities and associative composition. A functor preserves that structure. This language allows one to compare otherwise different mathematical settings, but it does not itself say which constructions exist. For example, the definition of a product in a category is not a recipe for forming a Cartesian product of underlying sets: it requires a universal factorization of pairs of arrows. If two products in a category $(P,p_1,p_2)$ and $(Q,q_1,q_2)$ exist, the universal properties give unique arrows $f:P\to Q$ and $g:Q\to P$ respecting projections. The composites $gf$ and $fg$ respect the same projections as the identities, so uniqueness forces them to be identities. Thus a definition yields a genuine theorem: products in a category are unique up to unique compatible isomorphism. The proof matters because it licenses replacing a construction by any other realization of the same property.

The Yoneda lemma is a more substantial example. For a covariant representable functor $\mathcal{C}(A,-)$ and $X:\mathcal{C}\to \mathbf{Set}$, a natural transformation $t:\mathcal{C}(A,-)\to X$ is determined by $a=t_A(1_A)$. Naturality forcesConversely this formula defines a natural transformation for every $a\in X(A)$. Hence $\mathrm{Nat}(\mathcal{C}(A,-),X)\cong X(A)$. The definition of naturality is indispensable, but the theorem identifies every possible transformation, proves representables detect arrows, and explains why universal objects can be studied through hom-sets. Merely knowing the definition does not supply this conclusion.

Similarly, an adjunction is defined by natural hom-set bijections. The construction of a free abelian group gives $\mathbf{Ab}({\mathbb{Z}}^{(S)},A)\cong \mathbf{Set}(S,UA)$, because a group homomorphism is determined uniquely by its values on the basis. This makes a universal extension problem transparent. But the Freyd general adjoint functor theorem goes further: it turns categorical limit preservation and a solution set into an actual adjoint. Its smallness hypotheses cannot be discarded as bookkeeping. For instance, the underlying-set functor from finite groups to finite sets has no left adjoint at a singleton. A putative universal finite group with universal element of order $m$ could not map that element to a generator of a finite cyclic group of order greater than $m$. The theorem's hypotheses separate existence from attractive notation.

The monoidal coherence theorem offers another example. A monoidal category has associativity and unit isomorphisms satisfying the pentagon identity for a monoidal category and triangle identity for a monoidal category. Coherence proves that every formal reassociation and unit insertion produces the same structural map. This is what justifies calculating without displaying all parentheses; it is not true merely because one has named an associator. Nor does it identify arbitrary additional maps, such as distinct braidings.

Finally, the opposite category construction shows how a definition can economize on proofs: reversing arrows takes products in a category to coproducts in a category, initial objects to terminal objects and monads to comonads. Yet this economy works because theorems and their proofs are invariant under the reversal. The subject is powerful precisely when definitions isolate reusable structure and theorems establish its consequences. Separating their importance obscures that partnership.

Write the monad identities asIf ${\mu }_A$ is invertible, its two right inverses agree, so ${\eta }_{TA}=T{\eta }_A$. Conversely, suppose ${\eta }_T=T\eta$. Naturality of $\eta$ at ${\mu }_A$, followed by that equality at $TA$, givesTogether with ${\mu }_A{\eta }_{TA}=1_{TA}$ this provesThis is the equivalence defining an idempotent monad.

For the equalizer submonad of a monad, let ${\beta }_A:RA\to TA$ equalize ${\eta }_{TA}$ and $T{\eta }_A$. If $f:A\to B$, naturality of these two transformations shows that $Tf{\beta }_A$ equalizes the corresponding pair at $B$. There is therefore a unique $Rf$ satisfyingUniqueness gives $R1=1$ and $R(gf)=RgRf$, so $R$ is a functor and $\beta :R\Rightarrow T$ is a natural transformation.

Take the stipulated factorizations ${\alpha }_A$ and ${\theta }_A$. Naturality of $\beta$ at ${\beta }_A$ rewrites their defining equations asThe composites on the right are natural in $A$; cancellation of the monic arrow ${\beta }_A$ therefore makes $\alpha$ and $\theta$ natural. We now verify every monad law, rather than assuming that restricting the structure automatically preserves them.

For the two unit laws, naturality and the unit laws of $T$ giveCancelling ${\beta }_A$ proves ${\theta }_A{\alpha }_{RA}=1_{RA}={\theta }_{A}R{\alpha }_A$. For associativity, the same naturality equations giveThese are equal by associativity of $\mu$; cancelling ${\beta }_A$ proves associativity of $\theta$. Thus

The remaining claims use two split equalizers associated with a monad. First, ${\eta }_{TA}:TA\to TTA$ is a split equalizer of ${\eta }_{TTA},T{\eta }_{TA}$. Its retraction is ${\mu }_A$, and the splitting of the parallel pair is $T{\mu }_A$, sinceThe equalizing equation follows from naturality of $\eta$. In general, identities $re=1$, $sf=er$, $sg=1$ and $fe=ge$ prove that $e$ is an equalizer: if $fh=gh$, then $h=erh$, with unique factorization $rh$. Hence ${\eta }_{TA}$ and ${\beta }_{TA}$ are two equalizers of the same pair. Their comparison is ${\alpha }_{TA}$, and its inverse is ${\mu }_A{\beta }_{TA}$. In particular

Second, $e_A=T{\eta }_A:TA\to TTA$ is a split equalizer of $TT{\eta }_A,T{\eta }_{TA}$, with retraction ${\mu }_A$ and splitting ${\mu }_{TA}$. Indeed,This is precisely the parallel pair in the PDF's diagram after $T{\beta }_A$. The map $T{\beta }_A$ equalizes that pair, because applying $T$ to the defining equalizer equation gives their equality on $T{\beta }_A$. PutThe split-equalizer factorization and ${\beta }_A{\alpha }_A={\eta }_A$ giveIf $T{\alpha }_A$ is invertible, then $T{\beta }_A=e_A(T{\alpha }_A{)}^{-1}$ is a monic arrow. Conversely, if $T{\beta }_A$ is a monic arrow, the equationforces $T{\alpha }_A{h}_A=1_{TRA}$, so $h_A$ is the inverse of $T{\alpha }_A$. ThereforeNotice that, under either condition, $T{\beta }_A$ is actually a split monomorphism, with retraction $T{\alpha }_A{\mu }_A$. Thus $TT{\beta }_A$ is a monic arrow too, since a functor preserves split monomorphisms. We have not assumed that $T$ preserves arbitrary monomorphisms.

Now prove the specified naturality square is a pullback in a category. Let $x:X\to TRA$ and $y:X\to RTA$ satisfy $T{\beta }_{A}x={\beta }_{TA}y$. Naturality of $\eta$, followed by the equalizer equation for ${\beta }_{TA}$, givesCancel the monic arrow $TT{\beta }_A$. Thus $x$ equalizes ${\eta }_{TRA},T{\eta }_{RA}$ and factors uniquely as $x={\beta }_{RA}z$ with $z:X\to RRA$. Naturality of $\beta$ then givesCancel ${\beta }_{TA}$ to obtain $R{\beta }_{A}z=y$. This is exactly existence and uniqueness in the pullback universal property.

Because the square is a pullback and $T{\beta }_A$ is a monic arrow, $R{\beta }_A$ is a monic arrow. Naturality of $\alpha$ and the formula for $\theta$ now giveCancelling $R{\beta }_A$ proves ${\alpha }_{RA}{\theta }_A=1_{RRA}$. The other composite is already one of the unit laws. Hence ${\theta }_A$ is invertible. If the equivalent monicity conditions hold for every $A$, we conclude