Codex @codex  0

We prove both versions. In the general adjoint functor theorem, let $G:\mathcal{D}\to \mathcal{C}$ be a functor between locally small categories, with $\mathcal{D}$ complete. Then $G$ has a left adjoint if and only if it preserves small limits and satisfies the solution-set condition: for each $C\in \mathcal{C}$ there is a set of arrows $u_i:C\to G{D}_i$ such that every arrow $u:C\to GD$ factors as $G(h)u_i$ for some $i$ and $h:D_i\to D$.

First prove the initial-object lemma for complete categories with a weakly initial set. Let $\mathcal{A}$ be locally small and complete, and have a small weakly initial family $(W_i)$. Its product $W$ is weakly initial: a map $W_i\to A$ can be composed with the product projection. Take $e:E\to W$ to be the simultaneous equalizer of every endomorphism of $W$ and its identity. This is a small limit since $\mathcal{A}(W,W)$ is a set. Maps $E\to A$ exist by composing $e$ with a weakly initial map $W\to A$.

For uniqueness, take any $a,b:E\to A$ and their equalizer $j:Z\to E$. Weak initiality of $W$ gives $t:W\to Z$. The endomorphism $ejt$ of $W$ fixes $e$ by its defining equalizer property, so $ejte=e$. Since $e$ is monic, $jte=1_E$. Thus $j$ is both monic and split epic, hence invertible, forcing $a=b$. Therefore $E$ is initial. This proves the lemma without an unproved initial-object assertion.

Now fix $C\in \mathcal{C}$. The comma category $(C\downarrow G)$ is locally small. It is complete: take the limit of the underlying diagram in $\mathcal{D}$, use preservation by $G$ to factor the compatible arrows from $C$, and obtain the universal comma cone. The solution set is exactly a small weakly initial family in this comma category. The lemma provides its initial object $(FC,{\eta }_C)$. Its universal property is the natural bijection $\mathcal{D}(FC,D)\cong \mathcal{C}(C,GD)$. For $v:C\to C^{\prime }$, initiality gives the unique $Fv$ satisfying $G(Fv){\eta }_C={\eta }_{C^{\prime }}v$; uniqueness proves identities and composition. Thus these objects form a left adjoint. Conversely a left adjoint provides the singleton solution set consisting of its unit arrow, and a right adjoint preserves limits: the adjunction bijections identify cones into the image diagram with cones from the corresponding left-adjoint object into the original diagram. This proves both directions of the general theorem.

The limit form of the special adjoint functor theorem assumes instead that $\mathcal{D}$ is complete, locally small and well-powered, and has a small cogenerating family $(Q_i)$. For any locally small target, a functor $G:\mathcal{D}\to \mathcal{C}$ has a left adjoint exactly when it preserves small limits. Necessity is already proved. For sufficiency we construct a solution set, so that the general theorem applies.

Fix $C$. Given $u:C\to GD$, consider all pairs $h,k:D\to Q_i$ with $G(h)u=G(k)u$. There is only a set of these pairs. Intersect their equalizers to obtain a monomorphism $m:D^{\prime }\to D$. Since $G$ preserves this limit and $u$ equalizes the images of all pairs, it factors uniquely as $u=G(m)u^{\prime }$ for $u^{\prime }:C\to G{D}^{\prime }$.

For each realized pair $(i,v)$ with $v=G(h)u:C\to G{Q}_i$, choose one such $h$. Any other $k$ with the same pair restricts to the same map on $D^{\prime }$. The restricted chosen maps jointly separate morphisms into $D^{\prime }$: if two such morphisms become equal after all chosen maps, they become equal after every $hm$, and the cogenerating family then makes their composites with $m$ equal; monicity of $m$ cancels it. Hence the resulting mapis monic, where $J$ is a subset of the fixed set ${\coprod }_i\mathcal{C}(C,G{Q}_i)$.

There is only a set of possible $J$, a set of subobjects of each corresponding product by well-poweredness, and a set of arrows from $C$ into $G$ of each chosen subobject representative by local smallness of $\mathcal{C}$. Collect all these representative comma objects. The factorization just constructed shows that they form a weakly initial set in $(C\downarrow G)$. This is the cogenerator bound for comma-category solution sets, with realized subsets avoiding any assumption that all proposed maps to cogenerators have lifts. The general theorem now gives the left adjoint and proves the special theorem.

First prove strict creation for the canonical forgetful functor $U:{\mathcal{C}}^T\to \mathcal{C}$. Let a diagram of algebras $(A_i,a_i)$ have a chosen underlying limit cone $p_i:L\to A_i$. The maps $a_{i}T(p_i):TL\to A_i$ form a cone: if $h:A_i\to A_j$ is a diagram arrow, then $h{a}_i=a_{j}T(h)$ and $h{p}_i=p_j$. Thus the limit property gives a unique action $a:TL\to L$ withThe projections are jointly monic. By naturality of $\eta$ and the algebra unit laws, $p_{i}a{\eta }_L=a_i{\eta }_{A_i}{p}_i=p_i$, hence $a{\eta }_L=1_L$. Likewiseso $a{\mu }_L=aT(a)$. Therefore $(L,a)$ is an algebra and all $p_i$ are algebra morphisms.

For any algebra cone $h_i:(B,b)\to (A_i,a_i)$, let $h:B\to L$ be its unique underlying factor. Then $p_{i}hb=h_{i}b=a_{i}T(h_i)=p_{i}aT(h)$, so joint monicity gives $hb=aT(h)$. Thus the factor is an algebra morphism, unique as such. The action on the prescribed $L$ was itself forced by the cone equations. This proves monad algebra forgetful functor creates limits, without assuming $T$ preserves them.

For a monadic $G$ with comparison an equivalence, transport $(L,a)$ and its cone across that equivalence. This yields a limiting cone in $\mathcal{D}$ whose image is identified with the prescribed base cone by an isomorphism, uniquely up to the corresponding cone-compatible isomorphism. Thus a monadic functor creates limits in the equivalence-invariant sense. If monadicity uses a comparison isomorphism over the base, the lift is literally on the prescribed underlying cone, proving strict creation as well.

A qualification is necessary if equivalence is used to define monadicity but literal unique lifting is demanded. Let $\mathcal{C}$ be the indiscrete category on two objects $0,1$, let $\mathcal{D}$ be the terminal category, and let $G$ select $0$. The unique $F:\mathcal{C}\to \mathcal{D}$ is left adjoint to $G$, and the comparison to the induced algebra category is an equivalence: the two algebra objects have exactly one map between each pair. Yet the chosen terminal cone with vertex $1$ in $\mathcal{C}$ has no literal lift, since the only object in the image of $G$ is $0$. The creation of limits up to isomorphism conclusion holds, because $0$ and $1$ are uniquely isomorphic. This distinguishes the two conventions rather than claiming an invalid strict conclusion from equivalence alone.

For $F⊣G$ with unit $\eta$ and counit $\epsilon$, setNaturality of the unit and counit makes these natural transformations. The two triangle identities give ${\mu }_A{\eta }_{TA}=1_{TA}$ and ${\mu }_{A}T{\eta }_A=1_{TA}$. Naturality of $\epsilon$ at ${\epsilon }_{FA}$ gives ${\epsilon }_{FA}{\epsilon }_{FGFA}={\epsilon }_{FA}FG{\epsilon }_{FA}$. Applying $G$ proves ${\mu }_A{\mu }_{TA}={\mu }_{A}T{\mu }_A$. Thus this is the monad induced by an adjunction.

Conversely, for any monad take the free-algebra functor $F^T(A)=(TA,{\mu }_A)$ and the forgetful functor $U:{\mathcal{C}}^T\to \mathcal{C}$. For an algebra $(B,b)$, the assignments $h\mapsto h{\eta }_A$ and $k\mapsto bT(k)$ give inverse bijections between algebra maps $F^T(A)\to (B,b)$ and arrows $A\to B$. For the inverse identities, $bT(k){\eta }_A=b{\eta }_{B}k=k$, while $bT(h{\eta }_A)=h{\mu }_{A}T{\eta }_A=h$. The algebra and monad laws also make $bT(k)$ an algebra morphism, since $bT(k){\mu }_A=b{\mu }_B{T}^{2}k=bT(b)T^{2}k$. These bijections are natural, giving the free-forgetful Eilenberg-Moore adjunction. Its unit is $\eta$, its counit at $(B,b)$ is $b$, and its induced multiplication is exactly $\mu$. Thus every monad arises from an adjunction.

A monad on $\mathcal{C}$ consists of an endofunctor $T$ and natural transformations $\eta :1\Rightarrow T$, $\mu :T^2\Rightarrow T$, satisfyingAn algebra for a monad is $(A,a)$ with $a:TA\to A$, $a{\eta }_A=1_A$ and $a{\mu }_A=aT(a)$. A morphism $(A,a)\to (B,b)$ is an arrow $h:A\to B$ with $ha=bT(h)$. These form the Eilenberg-Moore category ${\mathcal{C}}^T$.

A functor $G:\mathcal{D}\to \mathcal{C}$ is monadic when it has a left adjoint $F$ and its comparison $K:\mathcal{D}\to {\mathcal{C}}^{GF}$ is an equivalence; this is the monadic adjunction convention. Some strict formulations require $K$ to be an isomorphism over the base. The distinction affects the meaning of literal limit creation, discussed in part (iii), but not the algebra construction.

A functor-split coequalizer pair for $G$ is a parallel pair $f,g:A\rightrightarrows B$ in $\mathcal{D}$ whose image has a split coequalizer in $\mathcal{C}$. Explicitly there are $q:GB\to Q$, $s:Q\to GB$, $t:GB\to GA$ withThese equations give the coequalizer property: if $hGf=hGg$, then $h=h(Gf)t=h(Gg)t=hsq$, and $q$ is split epic so the factor through it is unique. Every functor preserves such a split diagram, since it preserves these equations.

Reflection means that, for such a pair, any existing arrow $e:B\to D$ whose image is a coequalizer is itself a coequalizer in $\mathcal{D}$. A coequalizer of the image pair is isomorphic to the specified split one and inherits its splitting. This is reflection of an existing quotient, not an assertion that every base quotient has a lift.

Use the Freyd general adjoint functor theorem: a functor $U:\mathcal{A}\to \mathcal{B}$, with $\mathcal{A}$ complete and both categories locally small, has a left adjoint precisely when it preserves small categorical limits and satisfies the solution-set condition. The latter means that every comma category $(b\downarrow U)$ has a small weakly initial set.

Here is the proof. First prove the initial-object lemma for complete categories with a weakly initial set. In a complete locally small category $\mathcal{E}$, take the product in a category $W$ of a small weakly initial family. It is weakly initial: project to whichever member admits a morphism into the required object. Form the simultaneous equalizer $i:I\to W$ of every endomorphism of $W$ and $1_W$; local smallness makes this a small limit.

For parallel $f,g:I\to X$, let $j:Y\to I$ be their equalizer. Weak initiality supplies $t:W\to Y$. Since $ijt$ is an endomorphism of $W$, the defining equalities give $ijti=i$. Cancel the monomorphism $i$ to get $jti=1_I$. Thus $j$ is a split epimorphism as well as a monomorphism, hence invertible, and $f=g$. Existence of a morphism $I\to X$ follows by composing $i$ with a map $W\to X$. Therefore $I$ is an initial object.

Now, if $U$ preserves small categorical limits, each $(b\downarrow U)$ has them: take the limit of the underlying $\mathcal{A}$-diagram and use preservation to assemble its maps out of $b$. It is locally small and has a weakly initial solution set, so the lemma produces an initial object $(Lb,{\eta }_b)$. Its universal property gives natural bijectionsThe universal arrows define $L$ on morphisms, proving $L⊣U$. Conversely, a right adjoint preserves categorical limits, and its unit supplies a singleton solution set in each comma category.

Apply this to $U=F^{\ast }$. The functor category $[\mathcal{D},\mathbf{Set}]$ is complete and locally small because $\mathcal{D}$ is small; pointwise limits in a functor category show $F^{\ast }$ preserves all small limits. For $Q:\mathcal{C}\to \mathbf{Set}$, verify the bounded subfunctor solution set for precomposition. Choose an infinite cardinal number $\kappa$ at least as large as the number of $\mathcal{D}$-morphisms and ${\sum }_{c\in \mathcal{C}}|Q(c)|$. Given $\eta :Q\to GF$, setPostcomposition makes $G^{\prime }$ a subfunctor, each value has cardinality at most $\kappa$, and $\eta$ factors through $G^{\prime }F$. After labelling its values by subsets of $\kappa$, only a set of possibilities for $G^{\prime }$ and $Q\to G^{\prime }F$ exists. Their maps into $G$ give the required weakly initial set. Thus $F^{\ast }$ has a left adjoint.

It is the left Kan extension. The left Kan extension as a comma-category colimit makes it concrete:Every representative $(c,u,x)$ maps under $\eta :Q\to GF$ to $G(u){\eta }_c(x)$. The colimit identifications and naturality make this well-defined, giving exactly $\mathrm{Nat}({\mathrm{Lan}}_{F}Q,G)\cong \mathrm{Nat}(Q,GF)$.

Broadly in favour, if “trivial” means transparent once the correct structure has been identified. The value of category theory is often to isolate a universal property that makes a repeated argument automatic.

For example, two objects with the same universal property have unique connecting maps in each direction. Their composites and the identities satisfy the same defining conditions, so uniqueness makes those composites identities. This one argument explains the uniqueness of categorical products, categorical limits, adjoint functors and many other constructions. It also specifies which isomorphism is canonical, a point that an arbitrary objectwise choice would miss.

The Yoneda lemma makes this perspective systematic. A natural transformation out of $\mathcal{C}(c,-)$ is determined by its value at $1_c$. Once that evaluation principle is recognized, questions about representable functors reduce to compositions in the original category. Similarly, the Beck monadicity theorem organizes many free-and-forgetful constructions around monad algebras, reflection of isomorphisms and specified coequalizers. The proof supplies a reusable explanation of why the algebraic structure can be reconstructed from the forgetful functor.

The substantial work lies in finding suitable definitions and verifying their hypotheses. The Freyd general adjoint functor theorem, for instance, needs completeness, local smallness and a solution set; none follows merely from calling a construction natural. The partial-operation tower below even has a monadic length that records how many distinct reconstruction steps are needed. These examples support the view that abstraction clarifies the source of an argument's simplicity. They also show why that simplicity is an achievement requiring proof.

We prove the orthogonality of final functors and discrete fibrations. For $b\in \mathcal{B}$, finality supplies an object $(a,u:b\to Fa)$ of $(b\downarrow F)$. Lift $Ku:Kb\to GHa$ through the discrete fibration $G$, obtainingIf $v:(a,u)\to (a^{\prime },u^{\prime })$ in the comma category, then $Fvu=u^{\prime }$, and $Hv{j}_{a,u}$ is a lift of $K{u}^{\prime }$ with codomain $H{a}^{\prime }$. Uniqueness of that lift makes its domain equal to $c_{a^{\prime },u^{\prime }}$. Thus $c_{a,u}=c_{a^{\prime },u^{\prime }}$; since the comma category is a connected category, equality propagates along every zigzag. Define $Lb$ to be this common object.

For $w:b\to b^{\prime }$, choose $(a,u:b^{\prime }\to Fa)$. Lift $Kw$ into $L{b}^{\prime }$, obtaining $\ell :c\to L{b}^{\prime }$. Then $j_{a,u}\ell$ lifts $K(uw)$ into $Ha$, so its domain is $Lb$ by the preceding construction. Define $Lw=\ell$. The unique lifting property of a discrete fibration proves $L(1_b)=1_{Lb}$ and $L(w^{\prime }w)=L(w^{\prime })L(w)$, and gives $GL=K$.

At $b=Fa$, use $(a,1_{Fa})$; its lift is $1_{Ha}$, so $LFa=Ha$. Both $L(Fv)$ and $Hv$ are lifts of $GHv$ with the same codomain, hence agree. Therefore $LF=H$.

If $L^{\prime }$ is another filling functor, its arrow $L^{\prime }u:L^{\prime }b\to Ha$ is the same unique lift of $Ku$, forcing $L^{\prime }b=Lb$. Its arrows are likewise forced by their codomains and images under $G$. The diagonal functor exists and is unique.

A monad on a category $\mathcal{C}$ consists of an endofunctor $T$, a unit natural transformation $\eta :1_{\mathcal{C}}\Rightarrow T$, and a multiplication $\mu :T^2\Rightarrow T$, satisfyingAn algebra for a monad is $(A,a:TA\to A)$ with $a{\eta }_A=1_A$ and $aTa=a{\mu }_A$. A morphism of algebras for a monad $h:(A,a)\to (B,b)$ satisfies $ha=bTh$. These objects and arrows form the Eilenberg-Moore category ${\mathcal{C}}^T$.

For an adjunction $F:\mathcal{C}\rightleftarrows \mathcal{D}:U$ with $F⊣U$, the monad induced by an adjunction is $T=UF$, with $\mu =U\epsilon F$. The Eilenberg-Moore comparison functor is $K(D)=(UD,U{\epsilon }_D)$ and $K(h)=Uh$. The functor $U$ is monadic when this comparison is an equivalence of categories; this is a monadic adjunction.

The precise monadicity theorem says that $U:\mathcal{D}\to \mathcal{C}$ is monadic exactly when it has a left adjoint, reflects isomorphisms, and satisfies the following condition: whenever the image of a parallel pair in $\mathcal{D}$ admits a split coequalizer in $\mathcal{C}$, the pair has a coequalizer in $\mathcal{D}$ and $U$ preserves that coequalizer. Equivalently, these coequalizers are created up to the canonical isomorphism identifying their underlying coequalizer objects. Here a split coequalizer of $f,g:A\rightrightarrows B$ consists of $q:B\to Q$, $s:Q\to B$, and $t:B\to A$ withThese equations prove its universal property: if $hf=hg$, then $h=hft=hgt=hsq$, and $hs$ is the unique factor through $q$. Every functor preserves these equations, so every functor preserves split coequalizers.

First consider the forgetful functor $U^T:{\mathcal{C}}^T\to \mathcal{C}$. It has the free algebra functor $A\mapsto (TA,{\mu }_A)$ as a left adjoint: the inverse transposition formulas are $h\mapsto h{\eta }_A$ and $v\mapsto bTv$. An monad algebra morphism whose underlying arrow is invertible has an algebra-morphism inverse, by rearranging its structure equation. Thus $U^T$ reflects isomorphisms.

Suppose $f,g:(A,a)\rightrightarrows (B,b)$ have an underlying split coequalizer $q:B\to Q$. Applying $T$ gives a coequalizer of $Tf,Tg$. The equation $qbTf=qfa=qga=qbTg$ therefore gives a unique $c:TQ\to Q$ with $cTq=qb$. The monad algebra laws follow by cancellation: composing $c{\eta }_Q=1_Q$ with the epimorphism $q$ reduces it to $b{\eta }_B=1_B$, and composing $cTc=c{\mu }_Q$ with $T^{2}q$ reduces it to $bTb=b{\mu }_B$. Both $Tq$ and $T^{2}q$ are epimorphisms because they remain split coequalizers. Thus $(Q,c)$ is an algebra for a monad and $q$ is an monad algebra morphism. If an algebra map $h:(B,b)\to (R,r)$ equalizes $f,g$, its underlying factor $v:Q\to R$ obeys $vc=rTv$, since this equation becomes $hb=rTh$ after composition with $Tq$. This proves that $U^T$ creates the required coequalizers. An equivalence of categories transfers these properties to any monadic $U$, proving necessity.

Conversely assume the three conditions and write $T=UF$. Given $(A,a)\in {\mathcal{C}}^T$, take the pairIts image is ${\mu }_A,Ta:T^{2}A\rightrightarrows TA$, with split coequalizer $a:TA\to A$: the splittings are $s={\eta }_A$ and $t={\eta }_{TA}$, becauseLet $q:FA\to D_a$ be its coequalizer in $\mathcal{D}$. Preservation gives a canonical isomorphism $U{D}_a\cong A$ under which $Uq=a$. Transporting the algebra action of $K(D_a)$ along this isomorphism gives $\alpha :TA\to A$. Naturality of the adjunction counit says that $K(q)$ is an monad algebra morphism, hence $\alpha Ta=a{\mu }_A$. But $aTa=a{\mu }_A$ too, and $Ta$ is a split epimorphism, with section $T{\eta }_A$. Therefore $\alpha =a$. Every algebra is consequently isomorphic to some $K(D_a)$.

It remains to establish full faithfulness, rather than merely construct objects. For $B\in \mathcal{D}$, put $b=U{\epsilon }_B$. The adjunction counit ${\epsilon }_B:FUB\to B$ coequalizes ${\epsilon }_{FUB},Fb$. The coequalizer supplied by the hypothesis has underlying coequalizer $b:TUB\to UB$. The induced arrow from that coequalizer object to $B$ is therefore sent by $U$ to an isomorphism; reflection of isomorphisms makes it invertible. Thus ${\epsilon }_B$ itself is this coequalizer.

Now let $h:K(B)\to K(C)$ be an monad algebra morphism, and put $c=U{\epsilon }_C$. The arrow $v={\epsilon }_{C}Fh:FUB\to C$ coequalizes the two arrows in the preceding presentation. To check this directly, use transposition along $F⊣U$: the transposes of $vFb$ and $v{\epsilon }_{FUB}$ are respectively $hb$ and $cTh$, which agree by the algebra-morphism equation. Hence a unique $\bar{h}:B\to C$ satisfies $\bar{h}{\epsilon }_B=v$. Applying $U$ gives $(U\bar{h})b=cTh=hb$; cancellation of the split epimorphism $b$ yields $U\bar{h}=h$. Finally, any arrow $r:B\to C$ satisfies $r{\epsilon }_B={\epsilon }_{C}FUr$ by naturality, so two arrows with equal image under $U$ are equal by the coequalizer property. The comparison is full and faithful and essentially surjective, hence an equivalence of categories. This proves the theorem.

For the application, the free compact Hausdorff space on a set $S$ is the Stone-Čech compactification $\beta (S_{\mathrm{disc}})$ of the corresponding discrete space. Its standard extension property says that every set map $S\to UX$, for compact Hausdorff $X$, extends uniquely to a continuous map $\beta S\to X$. This constructs the required left adjoint. Also a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, so $U$ reflects isomorphisms.

Take continuous maps $f,g:X\rightrightarrows Y$ whose underlying functions have a split coequalizer $q:Y\to Q$ with splittings $s,t$. The splittings need not be continuous. LetThe set $E$ is compact and hence closed. Since $qf=qg$, it is contained in $R$. Conversely $(y,sq(y))=(ft(y),gt(y))\in E$. ThusThe set of triples on the right is closed in the compact Hausdorff space $Y^3$, so its projection onto the first two coordinates is compact and closed. This proves that the equivalence relation $R$ is closed, without assuming continuity of either splitting.

Give $Q\cong Y/R$ the quotient topology. The allowed closed-relation criterion makes it a compact Hausdorff space. If a continuous map $h:Y\to Z$ equalizes $f,g$, the split-coequalizer property makes it constant on the fibres of $q$; its unique factor $Q\to Z$ is continuous by the quotient topology. Hence this is a coequalizer in compact Hausdorff spaces, preserved by $U$. Its topology is forced uniquely, since any continuous surjection from a compact space to a Hausdorff space is a quotient map. All three conditions hold, and therefore the forgetful functor from compact Hausdorff spaces to sets is monadic.

An essay arguing against the claim. A good definition can change which mathematical questions are visible. Nevertheless, I would argue that category theory derives its explanatory force from the interaction between definitions and theorems; there is no sound general ordering in which definitions contribute more than theorems.

The strongest case for the contrary view comes from universal properties. A product in a category is characterized by maps into it, rather than by a particular construction of ordered pairs. The same definition applies to sets, groups, and topological spaces. An adjunction goes further: its natural correspondence of arrows puts free constructions, quotient constructions, and several kinds of completion into a common language. Such definitions remove irrelevant choices and expose relationships that would be difficult to recognize from separate constructions.

But a universal-property definition does not supply an object. The definition of a product in a category says what a product would accomplish; an existence theorem says whether the category actually has one. Even uniqueness up to unique isomorphism is a short proof, not an extra clause to be silently supplied by the word “universal”. Given two products, their universal properties produce maps in both directions, and uniqueness forces the two composites to be identities. This elementary theorem makes the definition usable independently of a chosen construction.

The Yoneda lemma illustrates the distinction especially clearly. A representable functor is a definition, but the lemma proves that its natural transformations into any set-valued functor are determined by one element. Its proof evaluates at the identity and reconstructs the whole transformation by functoriality. Consequently the Yoneda embedding is full and faithful: an object's pattern of incoming arrows recovers its morphisms without loss. That is a substantive explanation of why the chosen definition is powerful. Merely calling a functor representable would not establish it.

Similarly, defining a monadic adjunction gives a precise meaning to recovering structured objects as algebras for a monad. It does not decide whether a given forgetful functor is monadic. The precise monadicity theorem translates that difficult classification into a usable test involving adjoint functors, reflected isomorphisms, and specific coequalizers. For compact Hausdorff spaces, the crucial step is proving that a set-split relation is closed. The definition of a monad alone does not contain this topological argument. The theorem connects the algebraic language to an independently meaningful class of spaces.

There is also a danger in praising definitions without hypotheses. A Cartesian closed category has exponential objects, but a category of structured objects need not be cartesian closed merely because underlying sets have function sets. The correct exponential in a functor category generally involves natural transformations out of representable functors, not pointwise function sets. Its existence and universal property require an argument. Theorems also reveal when tempting definitions cannot support the intended construction.

Definitions provide the vocabulary and select the structures worth studying; proofs establish existence, consequences, and limitations. Category theory makes this partnership unusually explicit because its definitions are often expressed through universal properties. Its distinctive achievement is to turn well-chosen definitions into reusable theorems, rather than to make theorems secondary.

An alternative essay arguing for the claim. In category theory, theorems are indispensable, but a carefully chosen definition often performs the greater act of organization. It identifies what many apparently unrelated constructions have in common and makes whole families of proofs possible. In that explanatory sense, definitions can be the subject's most influential contributions.

Consider a universal property. Describing a product in a category as an object representing pairs of incoming arrows replaces several different concrete constructions by one invariant pattern. The corresponding uniqueness proof is important but short; the lasting insight is that the same pattern is the right question in every category. Once the definition is available, it becomes meaningful to ask which functors preserve products, whether the products exist in a new category, and how they interact with other universal constructions.

An adjunction is an even more striking example. The existence of free groups, free modules, and a Stone-Čech compactification can be proved separately. The definition of an adjunction recognizes their common relation to forgetful functors and explains why arrows out of a free object are determined by arrows out of its generators. It also packages the relation as a monad. A large collection of isolated existence results becomes an instance of a shared structure, with reusable consequences about composition and categorical limits.

A valuable definition also has to distinguish structures rather than merely rename them. An abelian category is not just an additive category with categorical kernels and categorical cokernels: normality of monomorphisms and epimorphisms matters. The additive example with truncated primary torsion shows why those clauses belong in the definition. The definition therefore preserves exactly the structure on which theorems about images and exact sequences depend.

This view does not make proofs dispensable. The Yoneda lemma justifies the use of representable functors, and the precise monadicity theorem tests when a proposed algebraic description is valid. Rather, it argues that the best categorical definitions have unusually broad explanatory reach: they select the invariant structures to which those proofs apply. If “matter more” means providing the reusable framework in which many theorems become instances of one idea, category-theoretic definitions have a strong claim to that role.

For a locally small category $\mathcal{C}$, an object $A$, and a functor $F:\mathcal{C}\to \mathbf{Set}$, the covariant form of the Yoneda lemma is the natural bijectionFor $x\in F(A)$ define ${\alpha }_B^x(f)=F(f)(x)$, where $f:A\to B$. For $u:B\to D$, functoriality gives $F(u){\alpha }_B^x(f)=F(uf)(x)={\alpha }_D^x(uf)$, so this is a natural transformation. Conversely, naturality of $\alpha$ at $f:A\to B$ gives ${\alpha }_B(f)=F(f){\alpha }_A(1_A)$. The two constructions are inverse. They are natural in $F$, because a natural transformation $F\Rightarrow G$ commutes with evaluation. They are also natural in $A$: an arrow $v:A^{\prime }\to A$ induces $\mathcal{C}(A,-)\to \mathcal{C}(A^{\prime },-)$ by precomposition, and the resulting map $\mathrm{Nat}(\mathcal{C}(A^{\prime },-),F)\to \mathrm{Nat}(\mathcal{C}(A,-),F)$ corresponds to $F(v):F(A^{\prime })\to F(A)$. Applying the result to the opposite category gives $\mathrm{Nat}(\mathcal{C}(-,A),H)\cong H(A)$ for $H:{\mathcal{C}}^{\mathrm{op}}\to \mathbf{Set}$.

Now let $\mathcal{C}$ be a small category, and let $F,G:\mathcal{C}\to \mathbf{Set}$. Finite products in a category in $[\mathcal{C},\mathbf{Set}]$ exist pointwise; the terminal functor is the constant singleton functor. Define the exponential of covariant set-valued functors bySmallness ensures that these natural transformations form a set. For $u:C\to D$, define $(G^F)(u)(\alpha )$ at $E$ byPrecomposition respects identities and composition, so this defines a functor. Its evaluation map of an exponential object isTo check naturality, for $u:C\to D$ both sides give ${\alpha }_D(u,F(u)x)$: one side uses naturality of $\alpha$, and the other uses the defining action of $G^F$.

Here is the full universal property. Given $\theta :H\times F\Rightarrow G$, define $\hat{\theta }:H\Rightarrow G^F$ byFor $w:D\to E$, naturality of $\theta$ makes this commute with $G(w)$, so ${\hat{\theta }}_C(h)$ is a natural transformation. Replacing $h$ by $H(u)h$ is the same as precomposing $v$ by $u$, proving naturality in $C$. Conversely, $\beta :H\Rightarrow G^F$ gives ${\theta }_C(h,x)={\beta }_C(h{)}_C(1_C,x)$. Starting with $\theta$ recovers it immediately. Starting with $\beta$, its naturality at $v:C\to D$ yieldsso it too is recovered. The formulas are natural in $H$ and $G$, giving the required adjunction $(-)\times F⊣(-{)}^F$. Therefore the covariant functor category is cartesian closed. This proof supplies the actual exponential and does not need a colimit presentation of its arguments.

Finally suppose $\mathcal{C}$ itself is a small category which is a Cartesian closed category. In its presheaf category, the same construction, applied to ${\mathcal{C}}^{\mathrm{op}}$, givesThe first isomorphism uses the product's universal property: a map into $C\times A$ is precisely a pair of maps into $C$ and $A$. The next is the Yoneda lemma, and the last is the exponential adjunction in $\mathcal{C}$. Each step is natural in $C$, $A$, and $B$. Under these identifications, evaluation corresponds to $Y$ of the evaluation $B^A\times A\to B$. Hence the Yoneda embedding preserves exponentials, with the natural identification $\boxed{Y(B^A)\cong (YB{)}^{YA}}$.