An equivalence of categories consists of functors and together with invertible natural transformations and . A strict isomorphism of categories instead requires a functor with an inverse whose composites are literally identity functors.
First suppose belongs to an equivalence of categories. The isomorphisms give essential surjectivity. If , apply and conjugate by to obtain , so is a faithful functor. Similarly is a faithful functor. Writing , any has a preimage
Indeed naturality of gives , and faithfulness of gives . Thus is a full and faithful functor.
Conversely, assume is a full and faithful functor and has essential surjectivity. Using the axiom of choice, for each choose an object and an isomorphism . Define on a morphism by the unique lift
The full and faithful functor property makes preserve identities and composition, and makes a natural transformation. For , lift uniquely to . Lifting its inverse shows that is invertible. The naturality of and faithfulness of imply the naturality of . This proves
For large categories, this choice argument is understood in a fixed universe, or with the corresponding class-choice convention; ordinary set-sized axiom of choice suffices for small categories.
For the category of partial functions, let , with a tagged new element as basepoint. Send a partial function to the basepoint-preserving total function
Undefined composition is sent to the basepoint, so this is a functor . Restriction away from the basepoint recovers each partial function uniquely; hence it is a full and faithful functor. Every pointed set is isomorphic to , so there is an equivalence of categories. This particular equivalence can also be constructed explicitly, without choice, by deleting and adjoining the basepoint.
These actual categories are equivalent but not isomorphic. In the empty set is the only zero object: if is nonempty, its identity differs from its nowhere-defined endomorphism, so it cannot be initial or terminal. In every singleton pointed set is a zero object, and distinct singleton underlying sets give distinct objects. An isomorphism of categories is a bijection on objects preserving zero objects; it cannot take one such object onto several. This uses the categories of all actual sets, as in the paper, rather than chosen skeletal categories of representatives.
A skeletal category has no distinct isomorphic objects. If an equivalence joins two skeletal categories, essential surjectivity becomes surjectivity on objects. If , lift the identity of that object and its inverse using full and faithful to obtain , so . Thus is bijective on objects and on every hom-set. Its inverse on objects and morphisms is a strictly inverse functor, proving that it is an isomorphism of categories.
Under the axiom of choice, choose one object from each isomorphism class of a small category. The full subcategory on those objects is a skeleton of a category, and its inclusion is a full and faithful functor with essential surjectivity, hence an equivalence of categories.
For the converse, form the small category which is a groupoid with objects for , and exactly one morphism when , with no morphisms when . Suppose it is equivalent to a skeletal category , with quasi-inverse functors and . For each , the objects for are isomorphic, hence all equal to a uniquely determined . The isomorphism ensures that for some . The rule is a choice function. In particular, no representative in had to be chosen to define , since it is unique. Consequently
Assume is a full and faithful functor and its essential image is closed under strong quotients. First its unit is invertible. To prove this directly, fullness gives with . The triangle identity and faithfulness give . Naturality of at and the other triangle identity give
Thus is an isomorphism, and is also an isomorphism.
Factor as a strong epimorphism followed by a monomorphism. By closure under strong quotients, the intermediate object can, after transport along an isomorphism, be written as :
Fullness gives for . Taking the transpose of under the adjunction, whose transpose is , gives
Hence is a split monomorphism, so is a monomorphism. A strong epimorphism which is monic is invertible: apply its lifting property to the square with that same map on both sides and identity top and bottom edges. Thus is invertible and is monic. We have proved the pointwise-monic unit-and-counit criterion:
For a counterexample without the balanced hypothesis, use the pointwise-monic adjunction over a non-balanced poset. Let and let have one object and only its identity. The unique is left adjoint to selecting , since both and are singletons. All morphisms in a poset viewed as a category are monomorphisms, so the unit and counit are monic. However is not full: the identity has no preimage . The arrow is both monic and epic but not invertible, so is not a balanced category. The balanced hypothesis cannot be dropped.
A balanced category is one in which every morphism that is both a monomorphism and an epimorphism is an isomorphism. A faithful functor reflects both of these cancellation properties: for instance, implies , so monicity of and faithfulness imply ; the dual argument applies to epimorphisms. If is invertible, it is both monic and epic. Thus a faithful functor from a balanced category reflects isomorphisms.
For the adjunction , the unit and counit of an adjunction satisfy
If is a faithful functor and , applying and composing with gives , hence . Thus each is a monomorphism. Conversely, if every is monic and for , naturality gives
so . This proves the faithful left adjoint criterion.
Now assume both and are pointwise monic. The first triangle identity makes a split epimorphism; since it is also a monomorphism, it is invertible and is its inverse. The faithful left adjoint criterion says that is faithful, and the balanced category argument above then reflects the invertibility of to that of .
For completeness, an invertible unit makes a full and faithful functor. For , set . The triangle identity gives , so naturality of yields
Faithfulness was already proved.
Let be a strong epimorphism, and put
Then naturality gives . The square with left edge , right edge the monomorphism , top edge , and bottom edge has a diagonal by the defining lifting property of a strong epimorphism. Thus . A monic split epimorphism is invertible, so . The essential image of is therefore closed under strong quotients.
A monad on is an endofunctor with natural transformations and satisfying
An algebra for a monad is with and . A morphism of algebras for a monad satisfies . These form the Eilenberg-Moore category . Its free algebra functor is , and its adjunction to the forgetful functor has the explicit bijection
Write , , and let be the coproduct in a category injections. Set
Here is an algebra morphism, with underlying multiplication . For an algebra , an algebra morphism corresponds to , and the transposes of are respectively
For the second formula, by naturality of and the monad unit law. Thus exactly when, writing ,
These say precisely that and are morphisms of algebras for a monad. Consequently any coequalizer of represents pairs of algebra morphisms out of and , proving the coproduct presentation for monad algebras:
Its two algebra injections have underlying morphisms and ; the equivalence just proved verifies both the algebra equations and their universal property.
The displayed pair is a reflexive pair, with common section
Indeed by the algebra unit laws, while
Now suppose has all finite colimits and preserves reflexive coequalizers. The permitted creation theorem gives reflexive coequalizers in : the underlying pair is reflexive and its coequalizer exists and is preserved by . The preceding construction therefore gives binary algebra coproducts in a category. The initial object is , since the free algebra functor is a left adjoint and is initial in .
For any algebra pair , the augmented pair
is a reflexive pair, with common section the injection of , and has exactly the same coequalizing morphisms as . Hence all coequalizers exist in . The construction of finite colimits from coproducts and reflexive coequalizers now gives