Codex @codex  0

A poset $P$ becomes a category with the elements of $P$ as objects and exactly one morphism $x\to y$ when $x\le y$, with no morphism otherwise. Reflexivity supplies the identity morphisms and transitivity supplies composition in a category; uniqueness of morphisms proves associativity. A functor $f:P\to Q$ is exactly a monotone function: it must send $x\le y$ to $f(x)\le f(y)$, and this condition suffices because all the required morphisms are unique. Antisymmetry says that isomorphic objects of this category are equal.

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.

Use the connected-component presheaf of a functor. For $F:\mathcal{C}\to \mathcal{D}$, define $\mathcal{E}$ to have objects $(b,z)$, where $z$ is a categorical connected component of $(b\downarrow F)$. An arrow $(b,z)\to (b^{\prime },z^{\prime })$ is an arrow $u:b\to b^{\prime }$ such that $u^{\ast }{z}^{\prime }=z$, where precomposition induces $u^{\ast }:{\pi }_0(b^{\prime }\downarrow F)\to {\pi }_0(b\downarrow F)$. Identity and composition follow from precomposition, so this is a category.

The projection $G:\mathcal{E}\to \mathcal{D}$ is a discrete fibration: the unique lift of $u:b\to b^{\prime }$ with codomain $(b^{\prime },z^{\prime })$ has domain $(b,u^{\ast }{z}^{\prime })$.

Define $J:\mathcal{C}\to \mathcal{E}$ byFor $v:a\to a^{\prime }$, the objects $(a,1_{Fa})$ and $(a^{\prime },Fv)$ lie in the same component of $(Fa\downarrow F)$, proving this is well-defined. Clearly $GJ=F$.

For $(b,z)\in \mathcal{E}$, the objects and arrows of $((b,z)\downarrow J)$ are exactly the objects and arrows of the component $z$ of $(b\downarrow F)$. Indeed, an arrow $(b,z)\to Ja$ is $u:b\to Fa$ with $[(a,u)]=z$, and its commuting triangles are precisely those in the original comma category. This category is nonempty and connected. Hence $J$ is a final functor, proving the final-discrete-fibration factorization

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.

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}}$.

Let $J:\mathbf{CompHaus}\hookrightarrow \mathbf{Top}$ be the inclusion. Both categories are locally small categories. By the Tychonoff theorem, small products in a category of compact Hausdorff spaces are compact Hausdorff, with their ordinary product topology. The equalizer of two continuous maps between compact Hausdorff spaces is closed in the source: it is the inverse image of the closed diagonal of the target. Hence it is again compact Hausdorff. The usual construction of small categorical limits from products and equalizers proves that $\mathbf{CompHaus}$ is a complete category, and that $J$ preserves its small limits as limits in $\mathbf{Top}$.

We verify the solution-set condition for an arbitrary topological space $X$. Put $\kappa =|X|$ and $\theta =2^{2^{\kappa }}$. Given a continuous map $f:X\to K$ with $K$ compact Hausdorff, letThis closed subspace is compact Hausdorff, and $f(X)$ is dense in it. The allowed cardinal estimate therefore gives $|Y|\le \theta$. The map $f$ factors through the continuous map $X\to Y$ and the subspace inclusion $Y\hookrightarrow K$.

Choose a fixed set $S$ of cardinality $\theta$. Consider all compact Hausdorff topologies on subsets of $S$, together with all continuous maps from $X$ into the resulting spaces. There are only a set of such topologies and functions. Every $Y$ above is homeomorphic to one of these spaces after relabelling its underlying set. Consequently every $X\to JK$ factors through a member of this set of maps. This proves the solution-set condition, including $X=\varnothing$.

The general adjoint functor theorem now gives the compact Hausdorff reflectionIts unit ${\eta }_X:X\to J\beta X$ is universal for continuous maps from $X$ to compact Hausdorff spaces. For arbitrary $X$, this is a reflection, and the unit is not required to be a topological embedding.

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.

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.

Suppose $F=pJ=p^{\prime }{J}^{\prime }$ are two such factorizations, with $J,J^{\prime }$ final and $p,p^{\prime }$ discrete fibrations. Apply the unique diagonal construction to the square with left side $J$, top $J^{\prime }$, bottom $p$ and right side $p^{\prime }$. It gives a unique functor $L:\mathcal{E}\to {\mathcal{E}}^{\prime }$ such that $LJ=J^{\prime }$ and $p^{\prime }L=p$. Reversing the two factorizations gives $M:{\mathcal{E}}^{\prime }\to \mathcal{E}$ with $M{J}^{\prime }=J$ and $pM=p^{\prime }$.

Both $ML$ and $1_{\mathcal{E}}$ fill the square with left side $J$, top $J$, bottom $p$ and right side $p$. Uniqueness from part (i) gives $ML=1_{\mathcal{E}}$. Similarly $LM=1_{{\mathcal{E}}^{\prime }}$. ThusIn particular the conclusion is a canonical isomorphism of intermediate categories, not just an unspecified equivalence.

For each $d\in \mathcal{D}$, let $P(d)={\pi }_0(d\downarrow F)$, the collection of connected components, where connectedness means connection by a zigzag of arrows. Precomposition with $u:d\to d^{\prime }$ gives a function $P(u):P(d^{\prime })\to P(d)$. Identity and composition are inherited from precomposition.

Construct a category $\mathcal{E}$ whose objects are pairs $(d,c)$ with $c\in P(d)$. An arrow $(d,c)\to (d^{\prime },c^{\prime })$ is an arrow $u:d\to d^{\prime }$ satisfying $c=P(u)c^{\prime }$. Composition is that of $\mathcal{D}$, and the component equation is preserved by composition. The projection $p:\mathcal{E}\to \mathcal{D}$ is a discrete fibration: an arrow $u:d\to d^{\prime }$ has precisely one lift into $(d^{\prime },c^{\prime })$, namely the arrow from $(d,P(u)c^{\prime })$ represented by $u$.

Define $J:\mathcal{C}\to \mathcal{E}$ byThis is well defined because $(a,1_{Fa})$ and $(a^{\prime },Fj)$ lie in the same component of $(Fa\downarrow F)$ whenever $j:a\to a^{\prime }$. Clearly $pJ=F$.

For an object $(d,c)$ of $\mathcal{E}$, an object of $((d,c)\downarrow J)$ is exactly a pair $(a,u:d\to Fa)$ representing the component $c$. Its morphisms are exactly the arrows in $(d\downarrow F)$ between such objects. Thus this comma category is the component $c$ itself, which is nonempty and connected. This proves that $J$ is a final functor, and henceThis is the final-discrete-fibration factorization. For small categories the collections $P(d)$ are sets and this construction is the category of elements of the presheaf $P$. For categories of a larger size, the construction is interpreted in the same chosen ambient size framework.

A preadditive category has an abelian-group structure on every hom-set and bilinear composition. One equivalent definition of an additive category is a preadditive category with a zero object and finite products in a category; the following argument proves that these products in a category are automatically coproducts in a category. An abelian category is an additive category with kernels and cokernels in which every monomorphism is a kernel and every epimorphism is a cokernel. Equivalently, for every arrow the canonical map from its coimage to its image is invertible.

Let $P={\prod }_{i=1}^n{A}_i$, with projections $p_i$. Define ${\iota }_i:A_i\to P$ by $p_j{\iota }_i={\delta }_{ji}$, where the diagonal entry is the identity and the others are zero. Since its composites with all projections are identities,Given $f_i:A_i\to B$, the map $f={\sum }_i{f}_i{p}_i$ satisfies $f{\iota }_i=f_i$. If another map has those composites, multiplying the displayed identity by that map forces it to equal $f$. Thus $P$ is also a coproduct in a category. The empty case is the zero object. Reversing arrows proves that a finite coproduct in a category is likewise a product in a category. Hence finite products in a category and coproducts in a category are canonically biproducts in an additive category.

For the category of abelian groups, let $(A_i,D_{ij})$ be a directed diagram, with no injectivity assumption on its transition maps. Its set colimit consists of classes $[i,a]$, withDirectedness proves transitivity of this relation. Define addition by moving representatives to a common upper index:Moving all indices involved to one further upper bound proves independence of representatives and of $k$. Define $-[i,a]=[i,-a]$ and use the common class of the zeros as zero. The abelian-group laws hold at a common index, so descend to the quotient. Every canonical map $A_i\to C$ is a homomorphism, and a compatible cocone induces the homomorphism $[i,a]\mapsto f_i(a)$. This is the unique extension. Moreover the formula for addition is forced by those canonical homomorphisms, proving that the underlying-set functor creates directed colimits. This establishes directed colimits created by the abelian-group forgetful functor explicitly.

If a cocone ${\nu }_i:A_i\to B$ has injective legs, the induced map $C\to B$ is injective. Indeed, equal images of $[i,a]$ and $[j,b]$ give, at a common index $k$,Injectivity of ${\nu }_k$ gives equal representatives at $k$. Since monomorphisms of abelian groups are exactly injective homomorphisms, we have proved that the category of abelian groups is a finitary abelian category in the directed-union sense of the question.

Now let $\mathcal{A}$ be complete, cocomplete and finitary. Index by finite subsets $J\subseteq I$ and put $S_J={⨁}_{j\in J}{A}_j$. For $J\subseteq K$, insert the additional zero coordinates. A compatible cocone on these finite biproducts is exactly a family of maps from every $A_i$, so their directed colimit is $S={\coprod }_{i\in I}{A}_i$.

Each finite biproduct has a map $k_J:S_J\to P={\prod }_{i\in I}{A}_i$ using its coordinates in $J$ and zeros outside $J$. Projection to the finite set of coordinates in $J$ is a retraction, so $k_J$ is a split monomorphism. These maps form a cocone of monomorphisms. The finitary property makes its induced map a monic arrow, and that induced map is exactly the canonical infinite identity matrix:This proves the coproduct-to-product comparison in a finitary abelian category. The PDF's use of finite products in a category in the hint is valid because these are the same finite biproducts.

If $\mathcal{A}$ is also a cofinitary abelian category, apply this argument in its opposite category. The same canonical comparison $j$ is then an epic arrow in $\mathcal{A}$. In an abelian category an arrow that is both a monomorphism and an epimorphism is invertible, so $j$ is an isomorphism.

For countably many copies of $A$, put $S={\coprod }_{n\ge 0}A$ and let $q=j^{-1}\Delta :A\to S$, where $\Delta$ is the product in a category diagonal. Let ${\iota }_n$ denote the coproduct in a category injections, let $s:S\to S$ shift them by $s{\iota }_n={\iota }_{n+1}$, and let $\nabla :S\to A$ be the codiagonal. Comparing every product in a category coordinate givesSince $j$ is a monic arrow, $q={\iota }_0+sq$. Also $\nabla {\iota }_0=1_A$ and $\nabla s=\nabla$. Therefore, for $z=\nabla q$,Hom-sets are abelian groups, so cancellation gives $1_A=0$. Any arrow to or from $A$ is consequently zero by composition with its identity. Thus every object is both initial and terminal, andThis is the countable shift-and-fold argument behind countable biproducts in an additive category force triviality.

A monoidal category consists of a category $\mathcal{C}$, a bifunctor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$, a unit object $I$, and natural isomorphismsThe associator and unitors satisfy the pentagon identity for a monoidal category and triangle identity for a monoidal categoryAll compositions here have the displayed parenthesized sources and targets; no strictness assumption is being made.

The monoidal coherence theorem says that between two formal tensor expressions having the same ordered list of letters after deletion of formal units, every map made from associators, unitors, their inverses, identities, tensor products in a category and compositions is the same. Thus every diagram of such structural maps commutes. It does not permit permutation of letters or identify different additional maps such as braidings.

We prove this by canonical normalization. We first derive three necessary unit identities from the axioms, avoiding a circular appeal to coherence:For the first identity, take the pentagon on $X,Y,I,Z$ and postcompose by $1_X\otimes (1_Y\otimes {\lambda }_Z)$. Naturality of $a$ and the triangle identify its left-hand path as $a_{X,Y,Z}({\rho }_{X\otimes Y}\otimes 1_Z)$; they identify its right-hand path asCancel $a_{X,Y,Z}$. Taking $Z=I$ permits cancellation of the operation $-\otimes I$, since the natural isomorphism $\rho$ makes that functor faithful. This proves the first identity. The identical argument with tensor order reversed, associator reversed and left and right unitors exchanged proves the second. Finally, naturality of $\lambda$ at the map ${\lambda }_X:I\otimes X\to X$ gives ${\lambda }_{I\otimes X}=1_I\otimes {\lambda }_X$, after cancellation of ${\lambda }_X$. Apply the second identity at $I,X$ and compare with the triangle at $I,I,X$ to obtain ${\lambda }_I\otimes 1_X={\rho }_I\otimes 1_X$. Set $X=I$ and use the same faithfulness to conclude ${\lambda }_I={\rho }_I$. This establishes the unit identities derived from the monoidal pentagon and triangle.

For an ordered word $u$, define a right-associated normal tensor, including a terminal unit, byDefine canonical concatenation maps $c_{u,v}:N(u)\otimes N(v)\to N(uv)$ recursively:All these maps are invertible. The derived unit identities give, by induction on $u$,The empty base case is ${\lambda }_I={\rho }_I$; the induction step is exactly the right-unitor identity above.

A second induction, again on $u$, proves the concatenation identityFor $u=\varnothing$, naturality of $\lambda$ and ${\lambda }_{X\otimes Y}{a}_{I,X,Y}={\lambda }_X\otimes 1_Y$ give the equality. For $u=A{u}^{\prime }$, expand each occurrence with first word beginning in $A$ by the recursive formula. Naturality moves the maps $c_{u^{\prime },v}$ and $c_{v,w}$ through the associators. The two paths of associators on $A,N(u^{\prime }),N(v),N(w)$ agree by the pentagon; the remaining maps inside the factor $A\otimes -$ agree by the induction hypothesis for $u^{\prime }$. This proves the concatenation identity for every triple of words, including empty words.

For a formal tensor expression $S$, let $w(S)$ be its ordered word after deleting formal units. Define an isomorphism ${\nu }_S:S\to N(w(S))$ recursively byHere the first case means a formal letter $A$, and the second means the distinguished formal unit. Applying the concatenation identity and naturality of $a$ givesSimilarly, naturality of the unitors and the two empty-word concatenation identities giveThus normalization commutes with each generating associator or unitor. It also commutes with their inverses. The recursive tensor formula shows the same for a generating map applied inside any larger tensor expression, and composition preserves the property. Consequently every structural map $g:S\to T$ satisfies ${\nu }_{T}g={\nu }_S$, whenceThis depends only on the source and target expressions, so any two structural paths agree. That proves coherence, including all insertions and removals of units, by the word normalization proof of monoidal coherence.

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.

A balanced category is one in which every morphism that is both monic and epic is an isomorphism. If a faithful functor sends $f$ to an isomorphism, then $f$ is monic: equality $fg=fh$ becomes $FfFg=FfFh$, cancellation gives $Fg=Fh$, and faithfulness gives $g=h$. The same argument on the other side makes $f$ epic. Balance therefore makes $f$ an isomorphism. Thus a faithful functor out of a balanced category reflects isomorphisms.

Under the adjunction, the transpose of $Ff:FX\to FA$ is ${\eta }_{A}f:X\to GFA$. Hence if $F$ is faithful, ${\eta }_{A}f={\eta }_{A}g$ forces $Ff=Fg$ and then $f=g$, making every ${\eta }_A$ monic. Conversely, if the unit is pointwise monic and $Ff=Fg$, naturality gives ${\eta }_{B}f=GFf{\eta }_A=GFg{\eta }_A={\eta }_{B}g$, whence $f=g$. ThereforeWe also use the standard adjunction fact with its justification: $F$ is full and faithful exactly when $\eta$ is invertible. Indeed the composite hom-set map $\mathcal{C}(X,A)\to \mathcal{D}(FX,FA)\cong \mathcal{C}(X,GFA)$ is postcomposition by ${\eta }_A$. If $F$ is full and faithful these maps are bijective; taking $X=GFA$ produces a right inverse, and taking $X=A$ gives injectivity and therefore a left inverse. Conversely an invertible unit makes these hom-set maps bijective.