For the monad , an algebra for a monad is with and . A morphism of algebras for a monad satisfies . These objects and arrows form the Eilenberg-Moore category .
The free algebra functor sends to and to . The monad identities verify the algebra laws. For the forgetful functor , the free adjunction is
with inverse . The algebra law makes the latter an monad algebra morphism. The identities and prove the bijection.
In the category of adjunctions inducing a fixed monad, objects are adjunctions with their induced monad identified with . A morphism to is a functor between the right-hand categories satisfying , and compatibility with units and counits. With these strict identifications, define
The triangle identities give the unit algebra law; naturality of at gives the multiplication law. Naturality at makes an monad algebra morphism. Moreover , because , and is the free-adjunction counit at . Hence is a morphism into the Eilenberg-Moore adjunction.
For any other such , its underlying object at must be . Counit compatibility forces its algebra action to be , and the forgetful functor, which is a faithful functor, forces . Thus . This proves terminality of the Eilenberg-Moore adjunction. If adjunctions are specified only up to coherent isomorphisms, the same argument gives uniqueness up to the corresponding compatible natural isomorphism.
In an abelian category, the image factorization in an abelian category of is
where the abelian-category axiom identifies coimage with image. Thus is epic and is monic. Any other epi-mono factorization has and . Since epimorphisms are cokernels of their kernels, its middle object is canonically isomorphic to , uniquely compatibly with the two factors.
For a square , define by
The first arrow exists because factors through , so annihilates . Its composite with equals after the epimorphism , proving the second equation. Uniqueness after proves preservation of identities and composition. This gives the functoriality of abelian image factorization as a functor from the arrow category.
For pullback stability of abelian image factorization, state the standard facts that pullbacks preserve monomorphisms, epimorphisms in an abelian category are stable under pullback, and two adjoining pullback squares have pullback outer rectangle. In the given diagram, is therefore monic and is epic, while the composite is the pullback of . Its epi-mono factorization is an image factorization by the uniqueness just proved. Thus the top row is the image factorization of the pulled-back arrow, with its middle object canonically the pullback of the original image subobject.
Take the definition of an elementary topos as a category with finite limits, exponential objects and a subobject classifier . Its power object is , and is precomposition with . Transposing a predicate on in either variable gives
Thus is left adjoint to the contravariant power-object functor .
Here are the remaining hypotheses for the crude monadicity theorem, obtained from those topos axioms. The unit of this adjunction is , internally . It is monic: if two such evaluations agree, evaluate on the singleton predicate classified by the diagonal to obtain . If is invertible, naturality therefore makes monic. The characteristic map of this mono, regarded as a global element of , pulls back along to the everywhere-true predicate on . Since is monic, that characteristic map was already everywhere true on . The classifier pullback then says that is invertible. Hence is a conservative functor.
It remains to check preservation of reflexive coequalizers in the opposite category. Equivalently, let be a coreflexive pair, with satisfying , and let be their equalizer. Both and are monic. For any mono , there is a direct-image map between power objects: a subobject is sent to its composite with . This uses only classification of monos, not the prior existence of general images or colimits. We have .
For a predicate , consider its direct image along . Its pullbacks along the two sections are
To verify the second equality, with implies after applying , and therefore ; conversely supplies that witness. This argument works for parameterized subobjects as well, so it is an equality of arrows between power objects.
Now if satisfies , then . Hence is its unique factorization through , uniqueness following from the section . Therefore
is a coequalizer. Finite limits supply every required coreflexive equalizer. The right adjoint reflects isomorphisms and preserves the corresponding reflexive coequalizers, so is monadic. In particular is equivalent to the Eilenberg-Moore category of the double-power-object monad on .
Let be a logical functor, and suppose . Preservation of exponentials and the classifier gives , compatibly with the units, counits and resulting monads. Thus is the algebra functor lifting the base functor through the two monadic power-object functors. The adjoint lifting theorem for monad algebra functors applies to the base adjunction : its required coequalizers exist in , because has finite equalizers. It supplies a left adjoint . Taking opposites gives , the required right adjoint to .
Preserving either of the two logical structures by itself is insufficient. For the exponential example take constant at . The constant-empty functor is its left adjoint, since both relevant hom-sets are singletons. Its canonical exponential comparison is , so it preserves exponentials. It has no right adjoint: a functor with a right adjoint would preserve the initial object, whereas .
For the classifier example take to be fixed points. The trivial-action functor is left adjoint to . In a group-action topos the classifier is the trivial-action two-element set, since invariant subsets have ordinary equivariant characteristic maps. Therefore preserves the classifier, its true arrow and the terminal object. But does not preserve the coequalizer of the identity and the nontrivial translation on the regular two-element group set: that coequalizer is , while the fixed-point sets of the domain and codomain of the parallel pair are empty. Their set-theoretic coequalizer is empty, not . Thus has no right adjoint.
Write the Cartesian comonad as , with preserving finite limits. A coalgebra for a comonad is with , and . Its forgetful functor is faithful, creates finite limits, and has the cofree coalgebra right adjoint . We construct the two remaining topos structures explicitly.
For exponential objects, take coalgebras and start with . Put , with structure , and let
Transpose the following two maps into maps :
using . The cofree adjunction transposes once more into coalgebra morphisms . Let be their equalizer. A coalgebra map corresponds to an arbitrary ambient map . It factors through precisely when
which is exactly the condition that be a coalgebra morphism. Therefore represents and is the required exponential in a coalgebra topos.
For the subobject classifier, let classify the mono . In the cofree coalgebra , form
Both arrows are coalgebra morphisms. The cofree transpose of factors through this equalizer and gives its true arrow. To verify classification, let have ambient characteristic map . It supports a subcoalgebra of exactly when it is invariant under , equivalently
The counit proves the reverse containment in the first equation; the forward containment supplies the restricted structure map, whose coalgebra laws follow through the mono. Under the cofree adjunction, the second equation says exactly that factors through . Pulling back its true arrow recovers , since . This proves the universal property of the subobject classifier of a coalgebra topos. Hence is a topos.
Now let be a geometric morphism, with . The comonad is Cartesian: preserves finite limits and the right adjoint preserves limits. Put , already a topos. The forgetful adjunction defines with , so is faithful.
The comparison functor
preserves finite limits. It has a right adjoint , given on a coalgebra by
Indeed, the transposed arrow corresponds to a coalgebra map exactly when it equalizes these two maps. Applying the finite-limit-preserving shows that is the equalizer of
That equalizer is . If equalizes the pair, then , proving the claimed universal property. Consequently the counit is invertible. The fully faithful adjoint criterion makes full and faithful.
Thus defines a geometric embedding , and identifies the composite with . The requested factorization is
where is a surjective geometric morphism and is full and faithful.
The two introductory requests can be settled before the lettered applications. In the functor category , finite limits and finite unions of subobjects are pointwise. The component of the diagonal at is ordinary equality on . Its only possible complement is
This forms a subfunctor exactly when each sends unequal elements to unequal elements, equivalently when every is injective. In that case and the diagonal are disjoint and their union is at every component. Conversely, a diagonal complement must have these components and be stable under every transition map. Hence is decidable exactly when every transition map is injective.
Regard a monoid as a one-object category; a covariant set-valued functor is a left M-set. Give the diagonal left action . Let
Right multiplication on the first coordinate commutes with the diagonal left action, so remains equivariant. The formula obeys and . Evaluation is
It is equivariant because .
For an equivariant , define
This is equivariant in , and . Evaluation recovers . Conversely, currying the evaluation of a map recovers that map by its equivariance. This proves the exponential universal property and the natural identification
with exactly the stated action. In particular, decidability in a set-valued functor category says that a left M-set is decidable if and only if each of its action maps is injective.
The covariant form of the Yoneda lemma says that for a locally small category , a functor and an object , there is a bijection, natural in and ,
Explicitly its two directions are
For , functoriality gives , so is a natural transformation. Conversely, naturality of at gives . This proves that the displayed maps are inverses.
Naturality in follows because postcomposition by sends to . For , precomposition of transformations by sends to . This also verifies naturality in the representing object.
In the Category of sets, an epimorphism is exactly a surjective function. A surjective function is right-cancellable. If misses , the constant-zero function and the function that is one at and zero elsewhere are distinct maps with equal composites with .
If every is surjective, equality for natural transformations gives for every . Thus is an epimorphism in the functor category.
For the converse, construct the pointwise amalgamated double
where exactly the two copies of each element of are identified; different elements of remain different. Define . Naturality of implies that takes its image into the image at the target, so this formula is well-defined and gives a functor. The maps form natural transformations , with .
If is an epimorphism, . Since the two copies of an element outside would be distinct, every element must lie in that image. Hence is epic if and only if every component is epic. This proves the pointwise epimorphism in a functor category criterion directly, including the needed existence and naturality of the separating functor.
A functor is a representable functor if some object admits a natural isomorphism . Here the representable is covariant.
For the identity functor on the Category of sets, choose the singleton . The evaluation maps
are bijections with inverse . For , evaluation of is , proving naturality. Hence the identity functor on sets is represented by a singleton.
Choose a representing object and a natural isomorphism . Using the assumed small coproducts in a category, define
For a function , define by . The coproduct in a category uniqueness clause proves preservation of identities and composition, so this is a functor.
Restriction to the coproduct summands, followed by , gives
These bijections are natural in by the definition of , and natural in by naturality of . They establish , the left adjoint to a covariant representable functor. The empty set is sent to the empty coproduct.
A monad consists of an endofunctor and natural transformations and , the unit and multiplication of a monad, satisfying
An algebra for a monad is with satisfying and . A morphism of algebras for a monad satisfies . These objects and morphisms form the Eilenberg-Moore category ; its composition works because is a functor.
For the list monad, is the set of finite ordered lists, including the empty list. The map applies to each entry; and concatenates a list of lists. The unit laws say that adding singleton brackets and then flattening changes nothing. Associativity says that flattening a list of lists of lists in either order produces the same ordered sequence. These descriptions also prove naturality.
If is an algebra for a monad, define
The singleton law gives . Apply the algebra associativity law to and to obtain . Applying it to and shows
Thus is a monoid. Applying the same law to shows inductively that is necessarily ordered multiplication of its entries, with the empty product .
Conversely, any monoid defines such a list-fold map . The monoid unit proves , and associativity and the unit prove that multiplying flattened lists equals multiplying their individual products, including empty sublists. Hence . An algebra morphism preserves the empty-list value and two-entry-list values, so it is a monoid homomorphism; conversely a monoid homomorphism preserves every ordered product and is an algebra morphism. Therefore
Thus list-monad algebras are monoids, with the identification also matching every morphism.
Fix the chosen categorical limit object and its categorical cone . For , the family
is a categorical cone, by naturality of . The universal property of supplies a unique morphism
The identity morphism of satisfies the equations for , so . For composable , the equations for agree with those for ; uniqueness gives . Hence the chosen limits define a functor . This argument also handles an empty indexing category, when each chosen categorical limit is a terminal object.
Equivalently, represents the categorical cone functor , and functoriality of chosen representations supplies the same .
Conversely, assume that every hom-set functor preserves existing categorical limits. For a categorical limit cone in , a categorical cone determines an element of . The assumed bijection
gives one and only one such for every and every categorical cone. That is the universal property of the image cone itself. Therefore the hom-set tests detect limit preservation:
This proof works for all diagram sizes for which the relevant categorical limits and compatible-family sets are under consideration.
For every , the preceding part identifies the composite with the covariant representable functor . A covariant representable functor preserves every existing categorical limit, since a morphism into a categorical limit is the same as a compatible family of morphisms into the diagram objects. The limit functor preserves limits. The hom-set detection of categorical limits gives
In particular, it preserves all small categorical limits. They exist in : compute each one at every using completeness of , and use the uniqueness of the pointwise mediating morphisms to obtain its functor structure and universal natural transformations. Another expression of the same result is the adjunction .