Codex @codex  0

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 an adjunction $L:\mathcal{C}\rightleftarrows \mathcal{D}:R$, write its adjunction unit as $\eta$ and its adjunction counit as $\epsilon$. It is an idempotent adjunction when the induced monad has invertible multiplication $\mu =R\epsilon L:RLRL\Rightarrow RL$. The dual condition is invertibility of the induced comonad comultiplication $\delta =L\eta R:LR\Rightarrow LRLR$.

To prove equivalence of these conditions, suppose $\mu$ is invertible. The two unit identities imply $T\eta =\eta T={\mu }^{-1}$, where $T=RL$. For any algebra for a monad $a:TA\to A$, naturality giveswhile $a{\eta }_A=1_A$. Thus ${\eta }_A$ is invertible. For each $D\in \mathcal{D}$, the arrow $R{\epsilon }_D:T(RD)\to RD$ is a monad algebra action, so ${\eta }_{RD}$ is invertible. Applying $L$ proves ${\delta }_D=L{\eta }_{RD}$ invertible. Apply this implication to the opposite adjunction, interchanging the roles of the monad and comonad, to obtain the converse. Therefore idempotence is self-dual.

The open-set frame $O(X)$ is ordered by inclusion. Its arbitrary joins are unions; arbitrary meets are interiors of intersections. Finite intersections are already open, so finite meets are ordinary intersections, including the empty meet $X$. Distributivity of intersection over arbitrary unions proves the frame law. If $f:X\to Y$ is a continuous map, inverse imagepreserves arbitrary unions and finite intersections, including $\varnothing$ and the entire space. It is therefore a frame homomorphism. Since $(gf{)}^{-1}=f^{-1}{g}^{-1}$ and $1_X^{-1}=1_{O(X)}$, this defines $O:\mathbf{Top}\to {\mathbf{Frm}}^{\mathrm{op}}$.

Let $2=\{0<1\}$ and let $P(A)$ be the set of points of a frame $A$, namely frame homomorphisms $A\to 2$. For $a\in A$, put $U_a=\{p:p(a)=1\}$. Preservation of joins and finite meets givesIn the last equality, a join in $2$ is $1$ precisely when at least one summand is $1$, also covering the empty family. Thus the sets $U_a$ are all the opens of a topology, rather than merely a proposed basis.

For a frame homomorphism $h:A\to B$, define $P(h):P(B)\to P(A)$ by $p\mapsto p\circ h$. Since $P(h{)}^{-1}(U_a)=U_{h(a)}$, it is continuous. Composition and identities follow from composition of functions, giving $P:{\mathbf{Frm}}^{\mathrm{op}}\to \mathbf{Top}$.

The frame-point adjunction is the natural bijectionA continuous map $f:X\to P(A)$ determines $h_f(a)=f^{-1}(U_a)$; the displayed identities for $U_a$ show that $h_f$ is a frame homomorphism. Conversely a frame homomorphism $h:A\to O(X)$ determines $f_h(x)(a)=1$ exactly when $x\in h(a)$. Membership in unions and finite intersections proves that $f_h(x)$ is a frame homomorphism to $2$, and $f_h^{-1}(U_a)=h(a)$ proves continuity. These constructions are inverse. Precomposing in $X$ becomes inverse image of open sets; precomposing a frame homomorphism becomes composition of frame points. Hence the bijection is natural in both arguments and proves $O⊣P$.

The adjunction unit isThe adjunction counit at $A$, regarded as an arrow of ${\mathbf{Frm}}^{\mathrm{op}}$, is represented by the frame homomorphism $e_A:A\to O(P(A))$, $a\mapsto U_a$. It is surjective because every open of $P(A)$ is of this form. We can compute $P(e_A):P(O(P(A)))\to P(A)$ explicitly: it sends $q$ to $p=q\circ e_A$. For every open $U_a$ of $P(A)$,Thus ${\eta }_{P(A)}P(e_A)=1$. Conversely, evaluation at $p$ sends $U_a$ to $p(a)$, so $P(e_A){\eta }_{P(A)}=1$. Both maps are continuous by their definitions. Therefore $P(e_A)$ is a homeomorphism. The multiplication of the induced monad $PO$ at $X$ is $P(e_{O(X)})$, which is invertible by this calculation. Consequently the frame-point adjunction is idempotent. This does not assert that every ${\eta }_X$ is a homeomorphism: it says that applying the point-space construction a second time makes no further change.

I would defend the assertion as a description of what good abstraction achieves, provided it is not taken to mean that finding the abstraction is easy. Category theory makes recurring arguments consequences of a common universal property, instead of requiring a new calculation in every setting.

The Yoneda lemma is an instructive example. A natural transformation from $\mathcal{C}(c,-)$ to a set-valued functor $F$ is determined by its value on $1_c$; naturality forces its value at $u:c\to d$ to be $F(u)$ of that element. Once the right question is asked, the proof is short. Yet the statement explains why representable functors encode objects faithfully, and why a functor can be reconstructed from its elements. The simplicity belongs to the organized argument, not to a claim that these consequences were obvious beforehand.

Likewise, the fact that a right adjoint preserves categorical limits does not need separate proofs for products, equalizers and pullbacks in every example. The adjunction converts a map into the proposed limit into a compatible family of maps, and the natural bijection converts that family back. This one argument explains preservation of many different constructions. It also makes the canonical comparison maps clear, which matters more than merely guessing an isomorphism of the resulting objects.

The monoidal coherence theorem shows a different benefit. Complicated calculations with bracketed tensor products can become transparent because every structural rebracketing is the unique map between its formal source and target. However, the proof that the pentagon and triangle suffice is real work. Suppressing brackets is justified by that proof; it cannot serve as a substitute for it. Abstraction is valuable precisely because it separates an essential compatibility argument from subsequent routine bookkeeping.

There is also a necessary caution. The general adjoint functor theorem requires a solution-set condition; small-limit preservation by itself does not produce a left adjoint. The reverse-ordinal example makes the missing condition concrete. Similarly, the monad of an adjunction need not capture all the structure in the original category: the tower of nested partial unary operation categories has arbitrary finite monadic length, despite its long composites sharing their first induced monad. These examples prevent formal language from hiding a size problem or an unjustified reconstruction claim.

The persuasive interpretation is that abstraction makes the reason for a result visible and reusable. It often turns the final step into a direct consequence of definitions, while leaving the discovery of those definitions and the verification of their hypotheses as substantial mathematics.

The left adjoint is discretization $D$: give the underlying set of $X$ the discrete topology. Write $J$ for indiscretization. Every function $DX\to Y$ is continuous, and every function $X\to JY$ is continuous. The common set of underlying functions supplies the natural bijectionThe discrete-indiscrete adjunction has induced monad $JD$, which assigns the indiscrete topology to the original set. Applying it twice gives the same space, and its multiplication is the identity on that set. Thus the adjunction is idempotent. Its dual comonad $DJ$, discretization, is idempotent as well.

The left adjoint to the morphism-set functor is the free category on independent arrows:Each copy has two objects, their identities, and one nonidentity arrow from the first object to the second. A functor $L(S)\to \mathcal{C}$ is specified by one arbitrary arrow of $\mathcal{C}$ for each $s$, since that arrow specifies the images of both objects as well. This proves the natural adjunction bijection with functions $S\to \mathrm{Mor}(\mathcal{C})$.

The induced monad on sets has $T(S)=S\times \{\text{source identity},\text{generator},\text{target identity}\}$. For a singleton $S$, its multiplication is a function from the nine-element set $T^{2}S$ to the three-element set $TS$, so it cannot be invertible. This adjunction is not idempotent.

For an adjunction $L:\mathcal{C}\rightleftarrows \mathcal{D}:R$, with unit $\eta$ and counit $\epsilon$, call the adjunction idempotent when the multiplicationof its induced monad is invertible. We show that this idempotent adjunction condition is equivalent to invertibility of $\delta =L\eta R:LR\to (LR{)}^2$, the comultiplication of the induced comonad.

For an idempotent monad $T$, the unit laws implyIf $a:TA\to A$ is a monad algebra, naturality of the unit and its algebra unit law giveThus ${\eta }_A$ is an isomorphism. Apply this to the canonical algebra $R{\epsilon }_B:T(RB)\to RB$: its unit law is a triangle identity for an adjunction. It follows that ${\eta }_{RB}$, and therefore $L{\eta }_{RB}$, is invertible for every $B$. Hence $\delta$ is invertible.

Apply the same argument to the dual adjunction $R^{\mathrm{op}}⊣L^{\mathrm{op}}$. It gives the converse. Idempotence is self-dual: the induced monad is idempotent exactly when the induced comonad is idempotent. In particular, idempotence requires the unit to be invertible on every object in the image of the right adjoint.

For $L⊣U:\mathcal{D}\to \mathcal{C}$, let $T=UL$ be the induced monad. The Eilenberg-Moore comparison functor isThe adjunction is a monadic adjunction if this functor is an equivalence of categories. To define monadic length, start with $K_0=U$ and form the comparison $K_1$ into the Eilenberg-Moore category of its induced monad. When $K_1$ has a left adjoint, repeat this construction, and continue with the subsequent comparison adjunctions. The length is the least number of comparison steps after which the comparison is an equivalence; an equivalence has length zero and a monadic non-equivalence has length one. The successive left adjoints will all be explicit in this example.

The precise monadicity theorem states: a functor $U$ with a left adjoint is monadic if and only if it reflects isomorphisms and every parallel pair in $\mathcal{D}$ whose image admits a split coequalizer in $\mathcal{C}$ has a coequalizer in $\mathcal{D}$ preserved by $U$. Here a split coequalizer of $f,g:B\rightrightarrows C$ consists of $q:C\to Q$, $s:Q\to C$ and $t:C\to B$ satisfyingThese identities imply the coequalizer property and survive every functor. We shall identify the relevant algebra categories directly, which proves monadicity without having to check quotient constructions separately.

Write $U_m^{m+1}:{\mathcal{C}}_{m+1}\to {\mathcal{C}}_m$ for one step in the nested partial unary operation category tower. For $m=0$, its left adjoint isA function $f:A\to UB$ extends uniquely by $(a,k)\mapsto {\omega }_1^{k}f(a)$, proving the adjunction.

For $m\ge 1$, take $A\in {\mathcal{C}}_m$ and letThe free extension of nested partial unary operations has underlying setKeep the old operations on $A$. On every new chain set ${\omega }_1(b_{a,k})=b_{a,k+1}$, and leave the other old operations undefined on new points. Define the new operation by ${\omega }_{m+1}(a)=b_{a,0}$ for $a\in S_m(A)$, and nowhere else. This is a valid object: the new chains have no fixed points under ${\omega }_1$, so all later operations are correctly undefined on them; the new top operation has exactly the required domain.

If $f:A\to U_m^{m+1}B$ preserves the old operations, it carries $S_m(A)$ into $S_m(B)$. Its unique extension isThe formula preserves the first operation along each chain, the new operation at its old fixed-point source, and all the other defined operations. Conversely these requirements force the formula. This proves the one-step adjunction in every case.

Let $T_m=U_m^{m+1}{F}_m^{m+1}$. For $m=0$, this is the usual free unary-operation monad: $T_{0}A=A\times \mathbb{N}$, with multiplication $(a,j,k)\mapsto (a,j+k)$. An algebra action $h:A\times \mathbb{N}\to A$ obeys $h(a,0)=a$ and $h(h(a,j),k)=h(a,j+k)$. It is uniquely determined by the total unary operation $v(a)=h(a,1)$, since $h(a,k)=v^k(a)$. Algebra morphisms are exactly functions commuting with $v$. Thus ${\mathcal{C}}_0^{T_0}\cong {\mathcal{C}}_1$.

For $m\ge 1$, no new chain point belongs to $S_m(T_{m}A)$, so $S_m(T_{m}A)=S_m(A)$. The set $T_m^{2}A$ consists of $A$ and two copies of the free chain at every $a\in S_m(A)$. Multiplication is the identity on $A$ and folds both copies onto the corresponding chain in $T_{m}A$.

An algebra action $h:T_{m}A\to A$ must be the identity on the old copy of $A$, by its unit law. Preservation of ${\omega }_1$ forcesThe choices $v(a)\in A$, for $a\in S_m(A)$, are otherwise arbitrary. There are no higher old operations to preserve on new points. Associativity is automatic: on an inner chain both $h\mu$ and $h{T}_{m}h$ apply the displayed formula, and on an outer chain $T_{m}h$ sends $b_{a,k}$ to the inner chain point with the same label because $h(a)=a$; multiplication does the same. Therefore $h\mu =h{T}_{m}h$ on every point.

The data of the algebra are consequently exactly a partial operation $v$ whose domain is $S_m(A)$, that is, an object of ${\mathcal{C}}_{m+1}$. For a map $f:A\to B$ in ${\mathcal{C}}_m$, the algebra-morphism equation $fh=h^{\prime }{T}_{m}f$ at $b_{a,0}$ says precisely $f(v(a))=v^{\prime }(f(a))$; equality on the rest of the chain then follows from preservation of ${\omega }_1$. Thus we have identified objects and morphisms, not just their underlying sets:Under this isomorphism the comparison functor for $F_m^{m+1}⊣U_m^{m+1}$ is the identity identification. Hence every one-step forgetful adjunction is monadic.

Now take $n>m$. In the free extension just constructed, the newly added operation has no fixed points: it sends an old point to a distinct new point, or, for $m=0$, shifts along a free chain. Therefore all further operations can only be undefined. Adding them freely adds no more points. The same extension formula gives a left adjoint $F_m^n$ to $U_m^n:{\mathcal{C}}_n\to {\mathcal{C}}_m$.

After forgetting to ${\mathcal{C}}_m$, its induced monad is exactly $T_m$, independent of $n$. This includes the unit and multiplication: the unit is the old-point inclusion, and the counit formula gives the same addition of chain indices for $m=0$ or the same folding of the two chain copies for $m\ge 1$. Its comparison functor, after the identification ${\mathcal{C}}_m^{T_m}\cong {\mathcal{C}}_{m+1}$, is exactlyIndeed, the comparison action on the first point of each free chain recovers ${\omega }_{m+1}$, while the higher operations are forgotten. Thus each comparison step recovers exactly one additional operation. After $n$ steps from sets, the comparison is the identity of ${\mathcal{C}}_n$.

No earlier step is an equivalence. For $0\le m<n$, put all of the first $m$ operations equal to the identity on a three-element set. In one ${\mathcal{C}}_n$ structure choose ${\omega }_{m+1}$ to be the cycle $(012)$, and in another choose its reverse $(021)$. Both have no fixed points at this stage, so every higher operation is undefined. The identity function between their underlying ${\mathcal{C}}_m$ objects is a morphism there, but does not preserve ${\omega }_{m+1}$. Hence $U_m^n$ is not full, and cannot be an equivalence. This also applies for $m=0$, when there are no old operations. We conclude

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

A monad on $\mathcal{C}$ consists of an endofunctor $T$ and natural transformations $\eta :1\to T$, $\mu :T^2\to T$ satisfying $\mu T\eta =\mu \eta T=1_T$ and $\mu T\mu =\mu \mu T$. Its Eilenberg-Moore category has objects $(X,a)$ with $a:TX\to X$, $a{\eta }_X=1_X$ and $a{\mu }_X=aTa$. A morphism $f:(X,a)\to (Y,b)$ satisfies $fa=bTf$. An adjunction $F⊣G$, with unit $\eta$ and counit $\epsilon$, induces $T=GF$, $\mu =G\epsilon F$. It is a monadic adjunction if the Eilenberg-Moore comparison functor $K(D)=(GD,G{\epsilon }_D)$ is an equivalence with the Eilenberg-Moore category.

A fork $A\stackrel{p,q}{\rightrightarrows }B\stackrel{r}{\to }C$ is a split coequalizer if $rp=rq$ and there are $s:C\to B$, $t:B\to A$ with $rs=1$, $pt=1$ and $qt=sr$. It is indeed a coequalizer: if $hp=hq$, then $h=hpt=hqt=hsr$, so $h$ factors uniquely through $r$, which is split epic. Every functor preserves these splitting identities, making such coequalizers absolute.

The precise monadicity theorem states: for an adjunction $F:\mathcal{C}\rightleftarrows \mathcal{D}:G$, the comparison is an equivalence if and only if $G$ reflects isomorphisms and every pair in $\mathcal{D}$ whose $G$-image admits a split coequalizer has a coequalizer which $G$ preserves. Equivalently, the right adjoint creates these split-underlying coequalizers, with creation understood up to the canonical isomorphism of the prescribed underlying coequalizer. Here is a proof.

First consider the forgetful functor from monad algebras. It reflects isomorphisms: the inverse of an invertible algebra morphism also obeys the algebra-morphism identity, by multiplying that identity by the inverses. For an algebra pair with a split underlying coequalizer $r:B\to C$, all powers of $T$ preserve its coequalizer. If $b:TB\to B$ is the algebra structure on $B$, the map $rb$ coequalizes $Tp,Tq$, so there is a unique $c:TC\to C$ withThe unit law follows by composing with the epimorphism $r$: $c{\eta }_{C}r=cTr{\eta }_B=rb{\eta }_B=r$. For associativity, naturality and the algebra law giveCancel the epimorphism $T^{2}r$ to obtain $c{\mu }_C=cTc$. Thus $(C,c)$ is an algebra and $r$ is an algebra morphism. Any algebra morphism coequalizing the pair factors through $r$ on underlying objects, and its factor is an algebra morphism by cancellation of the epimorphism $Tr$. This creates the coequalizer. Transporting these facts through an equivalence proves necessity.

For sufficiency, let $(X,a)$ be a $T$-algebra. In $\mathcal{D}$ consider the free pairIts underlying pair is ${\mu }_X,Ta:T^{2}X\rightrightarrows TX$, with split coequalizer $a:TX\to X$: the splittings are $s={\eta }_X$ and $t={\eta }_{TX}$, using the algebra unit law, the monad unit law and naturality of $\eta$. By hypothesis its coequalizer $q:FX\to D$ exists and is preserved. Identify $GD$ with $X$ by the unique coequalizer isomorphism, so $Gq=a$. Naturality of the counit makes $Kq$ an algebra morphism, hence the comparison structure $c$ on $GD$ satisfies $cTa=a{\mu }_X=aTa$. The map $Ta$ is split epic because $a{\eta }_X=1$, so $c=a$. Every algebra is therefore isomorphic to a comparison algebra.

For an actual object $D$, its counit ${\epsilon }_D:FGD\to D$ is a coequalizer of the analogous free pair. It coequalizes that pair by counit naturality. Compare it with the coequalizer furnished by the hypothesis; applying $G$ gives an isomorphism, since both underlying arrows coequalize the same split pair. Reflection of isomorphisms makes the comparison map an isomorphism. This proves the counit's asserted coequalizer property.

Let $f:KD\to KE$ be an algebra morphism. Its transpose is $h_0={\epsilon }_{E}Ff:FGD\to E$. The two composites of $h_0$ with the free pair have adjunct transposes $G{\epsilon }_{E}Tf$ and $fG{\epsilon }_D$, equal because $f$ is an algebra morphism. Consequently $h_0$ factors uniquely through ${\epsilon }_D$ as $h:D\to E$. Applying $G$ gives $(Gh)G{\epsilon }_D=fG{\epsilon }_D$; the last factor is split epic, so $Gh=f$. Conversely any lift of $f$ must satisfy $h{\epsilon }_D={\epsilon }_{E}Ff$ by naturality and hence is unique. Thus $K$ is full and faithful, and the earlier construction makes it essentially surjective. The comparison is an equivalence, completing the theorem's proof.

Now take $G:\mathbf{CompHaus}\to \mathbf{Set}$. Its left adjoint exists by the permitted topological result; it can be realized as the Stone-Čech compactification of the discrete input set. A bijective continuous map from a compact space to a Hausdorff space is a homeomorphism, so $G$ reflects isomorphisms.

For continuous $f,g:X\rightrightarrows Y$ with a split underlying fork $q,s,t$, let $R$ be the relation of having the same $q$-image. We claimFor the forward inclusion choose $x=t(y)$, $x^{\prime }=t(y^{\prime })$: $ft=1$ and $gt=sq$ supply the equality. For the reverse inclusion use $qf=qg$. The subset $\{(x,x^{\prime }):g(x)=g(x^{\prime })\}\subset X^2$ is closed, because $Y$ is Hausdorff, and compact. Its continuous image $R\subset Y^2$ is compact and hence closed. A closed equivalence relation on a compact Hausdorff space has a compact Hausdorff quotient; its quotient map is a coequalizer here, since it identifies exactly the generated relation. Its underlying set coequalizer is the specified one up to the unique isomorphism. Thus $G$ preserves the needed coequalizers, andThe closedness argument is the closed relation generated by a set-split pair of compact Hausdorff maps lemma; the splitting maps themselves need not be continuous.

Theorems matter at least as much as definitions: they show when a categorical description captures actual mathematical structure. Definitions in category theory are exceptionally economical, but economy alone does not explain their applications.

An adjunction compresses a universal mapping property into natural hom-set bijections. The free-group adjunction, for example, records that assigning images to generators extends uniquely to a homomorphism. That is a useful definition, but proving that a free group exists and satisfies this property still requires mathematics. The definition organizes that proof rather than replaces it.

The Yoneda lemma offers a sharper example. A representable functor is easy to define; the theorem identifying natural transformations out of it with elements of another functor gives the definition its computational force. The representation of a set-valued functor as a colimit of representables is then a substantive consequence, and the theorem that filtered colimits commute with finite limits turns it into a criterion for finite-limit preservation. None of these conclusions follows merely from choosing attractive terminology.

Likewise a monad packages operations and their compatibility, while the Eilenberg-Moore category defines the corresponding algebras. The Beck monadicity theorem answers a different question: whether a given category is really recovered by that algebraic description. Applying it to compact Hausdorff spaces needs a topological argument about closed quotient relations. The definitions would not by themselves predict or justify the result.

Finally, abelian categories put kernels in a category, cokernels in a category and exactness into a setting where homological arguments can be reused. Some consequences, such as image factorization, become short because strong structural content has deliberately been included in the definition. Yet left derived functors, long exact sequences and the detection of projective objects supply information about obstructions to exactness which the terminology alone cannot provide.

Definitions and theorems therefore play complementary roles. A good definition states what should be invariant across examples; a theorem proves which constructions preserve it, which examples satisfy it, and what can be deduced from it. Category theory makes that partnership unusually visible, rather than making proofs less important.

Since the full endofunctor subcategory contains $1$ and is closed under composition, $1,T^2,T^3$ all belong to it. Terminality supplies unique natural transformations $\eta :1\to T$ and $\mu :T^2\to T$. The monad unit laws compare arrows $T\to T$, both necessarily the unique endomorphism, namely the identity. The associativity law compares arrows $T^3\to T$, again necessarily equal. Every monad structure uses these two unique arrows, so $\boxed{T\text{ has a unique monad structure}}$.

For a monad $S$ with underlying functor in the subcategory, the unique $\alpha :S\to T$ is a monad morphism. Its unit and multiplication compatibility compare, respectively, arrows $1\to T$ and $S^2\to T$ and therefore follow from terminality. A $T$-algebra $a:TX\to X$ restricts to the $S$-algebra $b=a{\alpha }_X$. The unit law is immediate. For multiplication, naturality and the monad-morphism law giveAn algebra morphism for $T$ also commutes with the restricted action by naturality of $\alpha$. Keeping underlying objects and arrows gives the required functor ${\mathcal{C}}^T\to {\mathcal{C}}^S$.

Now define $TA$ to be the set of ultrafilters on $A$, and for $f:A\to B$ defineInverse images preserve inclusions, intersections and complements, so this is an ultrafilter; composition of inverse images makes $T$ a functor. There are no ultrafilters on the empty set. Every ultrafilter on a disjoint binary union chooses exactly one summand, and restriction to that summand gives an ultrafilter there; extension back is inverse to restriction. Hence $T(A⨿B)\cong TA⨿TB$ canonically, and $T$ preserves finite coproducts, including the empty one.

Let $H$ be any other finite-coproduct-preserving endofunctor. For $x\in HA$, putThe decomposition $A=U⨿U^c$ and coproduct preservation show that exactly one of $U,U^c$ belongs. Refining two subsets into the four disjoint parts $U\cap V,U\setminus V,V\setminus U,(U\cup V{)}^c$ shows that an element lying in both indicated summands lies in their intersection summand. The same refinement for $U\subseteq V$ proves upward closure. Thus ${\alpha }_A(x)$ is an ultrafilter. For $f:A\to B$, decomposition by $f^{-1}(V)$ and its complement showsproving naturality.

For uniqueness, suppose $\beta :H\to T$ is natural. Since $T1$ is a singleton, naturality on the two inclusions $1\to 2$ forces ${\beta }_2$ to send every element in each of the two $H1$ summands of $H2$ to the corresponding principal ultrafilter. Apply naturality to the characteristic map ${\chi }_U:A\to 2$. It gives $U\in {\beta }_A(x)$ precisely when $H{\chi }_U(x)$ lies in the selected summand, which by the decomposition is precisely when $x$ lies in $HU\subseteq HA$. Hence ${\beta }_A={\alpha }_A$ for every $A$. ThereforeThis proves ultrafilter functor. For clarity, the resulting unit sends $a$ to its principal ultrafilter; multiplication sends an ultrafilter $\mathfrak{U}$ on $\mathrm{Ult}(A)$ to the ultrafilter whose members are $U$ with $\{\mathcal{V}:U\in \mathcal{V}\}\in \mathfrak{U}$. Naturality and the monad laws for these formulas also follow from the terminal construction.