nLab equivalence of categories

Redirected from "equivalence of groupoids".
Equivalence of categories

Context

Category theory

Equality and Equivalence

Equivalence of categories

Idea

The concept of equivalence of categories is the correct category theoretic notion of “sameness” of categories.

Concretely, an equivalence between two categories is a pair of functors between them which are inverse to each other up to natural isomorphism of functors (inverse functors).

This is like an isomorphism, but weakened such as to accomodate for the fact that the correct ambient context for categories is not iself a 1-category, but is the 2-category Cat of all categories. Hence abstractly an equivalence of categories is just the special case of an equivalence in a 2-category specialized to Cat.

If some foundational fine print is taken care of, then a functor exhibits an equivalence of categories precisely if it is both essentially surjective and fully faithful. This is true in classical mathematics if the axiom of choice is assumed. It remains true non-classically, say for internal categories, if the concept of functor is suitably adapted (“anafunctors”), or the concept of essentially surjective is suitably adapted (“split essentially surjective”).

From the point of view of logic one may say that two categories are equivalent if they have the same properties — although this only applies (by definition) to properties that obey the principle of equivalence.

Just as equivalence of categories is the generalization of isomorphism of sets from sets to categories, so the concept generalizes further to higher categories (see e.g. equivalence of 2-categories, equivalence of (∞,1)-categories) and ultimately to equivalence of \infty-categories.

Definitions

Definition

An equivalence between two categories 𝒞\mathcal{C} and 𝒟\mathcal{D} is an equivalence in the 2-category Cat of all categories, hence a pair of inverse functors, hence it is

  1. a pair of functors

    𝒞AAFAAAAGAA𝒟, \mathcal{C} \underoverset {\underset{\phantom{AA}F \phantom{AA}}{\longrightarrow}} {\overset{\phantom{AA}G\phantom{AA}}{\longleftarrow}} {} \mathcal{D},
  2. natural isomorphisms

    FGId 𝒟 F \circ G \cong Id_{\mathcal{D}}

    and

    GFId 𝒞. G \circ F \cong Id_{\mathcal{C}} \,.

This is called an adjoint equivalence if the natural isomorphisms above satisfy the triangle identities, thus exhibiting FF and GG as a pair of adjoint functors.

Two categories are called equivalent if there exists an equivalence between them.

Proposition

Let F:𝒞𝒟F \colon \mathcal{C} \to \mathcal{D} be a functor. Then the following are equivalent:

  1. FF is part of an equivalence of categories in the sense of def.

  2. FF is

    1. a split essentially surjective functor and

    2. a fully faithful functor.

Proof

This proof is from the HoTT book, and is set in the context of homotopy type theory. The categories here are what the HoTT book calls “precategories”, i.e. not univalent categories:

Suppose FF is an equivalence of categories with G,η,ϵG,\eta,\epsilon specified. Then we have the function

hom B(Fa,Fb) hom A(a,b), g η b 1G(g)η a. \begin{aligned} hom_B(F a, F b) &\to hom_A(a,b), \\ g &\mapsto \eta_b^{-1}\circ G(g) \circ \eta_a. \end{aligned}

For f:hom A(a,b)f:hom_A(a,b), we have

η b 1G(F(f))η a=η b 1η bf=f\eta_b^{-1} \circ G(F(f)) \circ \eta_a = \eta_b^{-1} \circ \eta_b \circ f = f

while for g:hom B(Fa,Fb)g: hom_B(F a, F b) we have

F(η b 1G(g)η a) =F(η b 1)F(G(g))F(η a) =ϵ FbF(G(g))F(η a) =gϵ FaF(η a) =g \begin{aligned} F(\eta_b^{-1} \circ G(g) \circ \eta_a) &= F(\eta_b^{-1}) \circ F(G(g)) \circ F(\eta_a) \\ &= \epsilon_{F b} \circ F(G(g)) \circ F(\eta_a) \\ &= g \circ \epsilon_{F a} \circ F(\eta_a) \\ &= g \end{aligned}

using naturality of ϵ\epsilon, and the triangle identities twice. Thus, F a,bF_{a,b} is an equivalence, so FF is fully faithful. Finally, for any b:Bb:B, we have Gb:AG b : A and ϵ b:FGbb\epsilon_b : F G b \cong b.

On the other hand, suppose FF is fully faithful and split essentially surjective. Define G 0:B 0A 0G_0:B_0\to A_0 by sending b:Bb:B to the a:Aa:A given by the specified essential splitting, and write ϵ b\epsilon_b for the likewise specified isomorphism FGbbF G b \cong b.

Now for any g:hom B(b,b)g: hom_B(b,b'), define G(g):hom A(Gb,Gb)G(g): hom_A(G b, G b') to be the unique morphism such that F(G(g))=(ϵ b) 1gϵ bF(G(g))=(\epsilon_{b'})^{-1} \circ g \circ \epsilon_b which exists since FF is fully faithful. Finally for a:Aa:A define η a:hom A(a,GFa)\eta_a : hom_A(a,G F a) to be the unique morphism such that Fη a=ϵ Fa 1F \eta_a = \epsilon^{-1}_{F a}. It is easy to verify that GG is a functor and that (G,ηϵ)(G,\eta \epsilon) exhibit FF as an equivalence of categories.

We clearly recover the same function G 0:B 0A 0G_0 : B_0 \to A_0. For the action of FF on hom-sets, we must show that for g:hom B(b,b)g:hom_B (b,b'), G(g)G(g) is the necessarily unique morphism such taht F(G(g))=(ϵ b) 1gϵ bF(G(g))=(\epsilon_{b'})^{-1} \circ g \circ \epsilon_b.

But this holds by naturality of ϵ\epsilon. Then we show (2)(1)(2)(2) \to (1) \to (2) gives the same data hence (1)(2)(1)\simeq (2).

Variants

We discuss some possible variants of the definition of equivalence of categories, each of which comes naturally from a different view of Cat.

The first, isomorphism, comes from viewing CatCat as a mere 1-category; it is too strong and is really only of interest for strict categories. The next, strong equivalence, comes from viewing CatCat as a strict 2-category; it is the most common definition given and is correct if and only if the axiom of choice holds. The next definition, weak equivalence, comes from viewing CatCat as a model category; it is correct with or without choice and is about as simple to define as strong equivalence. The fourth, anaequivalence, comes from viewing CatCat as a bicategory that is not (without the axiom of choice) equivalent (as a bicategory!) to the strict 22-category that defines strong equivalence; it is also always correct.

It is also possible to define ‘category’ in such a way that only a correct definition can be stated, but here we use the usual algebraic definitions of category, functor, and natural isomorphism.

Isomorphism

Two strict categories CC and DD are isomorphic if there exist strict functors F:CDF\colon C \to D and G:DCG\colon D \to C such that FGF G and GFG F are each equal to the appropriate identity functor. In this case, we say that FF is an isomorphism from CC to DD (so GG is an isomorphism from DD to CC) and call the pair (F,G)(F,G) an isomorphism between CC and DD. The functor GG is called the strict inverse of FF (so FF is the strict inverse of GG).

If you think of CatCat as the category of (strict) categories and functors, then this is the usual notion of isomorphism in a category. This is the most obvious notion of equivalence of categories and the first to be considered, but it is simply too strong for the purposes to which category theory is put. For example, here are some basic and important equivalences of categories that are not isomorphisms:

  • Let CC be the category of pointed sets, and let DD be the category of sets and partial functions. The functor F:CDF:C\to D takes a pointed set to its subset of non-basepoint elements, and a pointed function to the induced partial function on these (which is defined on those elements not sent to the basepoint). See the section “The category of sets and partial functions” in partial function for this equivalence.

  • Let CC be the category of finite-dimensional vector spaces over a field kk, and let DD be the category whose objects are natural numbers and whose morphisms nmn\to m are m×nm\times n matrices of elements of kk (which is equivalently the full subcategory of CC spanned by the specific vector spaces k nk^n). Note in particular that here DD is a small category, while CC is not (though it is essentially small, being equivalent to DD).

Strong equivalence

Two strict categories CC and DD are strongly equivalent if there exist strict functors F:CDF\colon C \to D and G:DCG\colon D \to C such that FGF G and GFG F are each naturally isomorphic (isomorphic in the relevant functor category) to the appropriate identity functor. In this case, we say that FF is a strong equivalence from CC to DD (so GG is a strong equivalence from DD to CC). The functor GG is called a weak inverse of FF (so FF is a weak inverse of GG).

Note that an isomorphism is precisely a strong equivalence in which the natural isomorphisms are identity natural transformations.

If you think of CatCat as the strict 2-category of (strict) categories, functors, and natural transformations, then this is the usual notion of equivalence in a 22-category. This is the first ‘correct’ definition of equivalence to be considered and the one most often seen today; it is only correct using the axiom of choice.

If possible, use or modify the counterexample to isomorphism to show how choice follows if strong equivalence is assumed correct.

Weak equivalence

Two categories CC and DD are weakly equivalent if there exist a category XX and functors F:XDF\colon X \to D and G:XCG\colon X \to C that are essentially surjective and fully faithful. In this case, we say that FF is a weak equivalence from XX to DD (so GG is a weak equivalence from XX to CC) and call the span (X,F,G)(X,F,G) a weak equivalence between CC and DD. (It is not entirely trivial to check that such spans can be composed, but they can be.)

A strict functor with a weak inverse is necessarily essentially surjective and fully faithful; the converse is equivalent to the axiom of choice. Thus any strong equivalence becomes a weak equivalence in which XX is taken to be either CC or DD (or even built symmetrically out of CC and DD if you're so inclined); a weak equivalence becomes a strong equivalence using the axiom of choice to find weak inverses and composing across XX.

If you think of CatCat as the model category of categories and functors with the canonical model structure, then this is the usual notion of weak equivalence in a model category.

Anaequivalence

Two categories CC and DD are anaequivalent if there exist anafunctors F:CDF\colon C \to D and G:DCG\colon D \to C such that FGF G and GFG F are each ananaturally isomorphic (isomorphic in the relevant anafunctor category) to the appropriate identity anafunctor. In this case, we say that FF is an anaequivalence from CC to DD (so GG is an anaequivalence from DD to CC). The functor GG is called an anainverse of FF (so FF is an anainverse of GG). See also weak equivalence of internal categories.

Any strict functor is an anafunctor, so any strong equivalence is an anaequivalence. Using the axiom of choice, any anafunctor is ananaturally isomorphic to a strict functor, so any anaequivalence defines a strong equivalence. Using the definition of an anafunctor as an appropriate span of strict functors, a weak equivalence defines two anafunctors which form an anaequivalence; conversely, either anafunctor in an anaequivalence is (as a span) a weak equivalence.

If you think of CatCat as the bicategory of categories, anafunctors, and ananatural transformations, then this is the usual notion of equivalence in a 22-category. It's fairly straightforward to turn any discussion of functors and strong equivalences in a context where the axiom of choice is assumed into a discussion of anafunctors and anaequivalences in a more general context.

We can also regard the 22-category CatCat above as obtained from the 22-category StrCatStr Cat of strict categories, strict functors, and natural transformations by formally inverting the weak equivalences as in homotopy theory.

Fully faithful essentially surjective functors

Finally, there are fully faithful and essentially surjective functors. However, while in general, these are not the same as equivalences in all mathematical foundations, they are the same under certain restrictions:

Proposition

Assume the ambient context is one of the following:

Let F:𝒞𝒟F \colon \mathcal{C} \to \mathcal{D} be a functor. Then the following are equivalent:

  1. FF is part of an equivalence of categories in the sense of def.

  2. FF is

    1. an essentially surjective functor and

    2. a fully faithful functor.

Remarks

Note that weak inverses go with strong equivalences. The terminology isn't entirely inconsistent (weak inverses contrast with strict ones, while weak equivalences contrast with strong ones) but developed at different times. The prefix ‘ana‑’ developed last and is perfectly consistent.

If you accept the axiom of choice, then you don't have to worry about the different kinds of equivalence (as long as you don't use isomorphism). This is not just a question of foundations, however, since the axiom of choice usually fails in internal contexts.

It's also possible to use foundations (such as homotopy type theory, some other forms of type theory, or FOLDS) in which isomorphism and strong equivalence are impossible to state. In such a case, one usually drops the prefixes ‘weak’ and ‘ana‑’. In the nn-Lab, we prefer to remain agnostic about foundations but usually drop these prefixes as well, leaving it up to the reader to insert them if necessary.

Adjoint equivalence

Any equivalence can be improved to an adjoint equivalence: a strong equivalence or anaequivalence whose natural isomorphisms satisfy the triangle identities. In that case, GG is called the adjoint inverse of FF (so FF is the adjoint inverse of GG). When working in the 22-category CatCat, a good rule of thumb is that it is okay to consider either

  • a functor with the property of being a general equivalence or
  • a functor with the structure of being an adjoint equivalence (that is, a functor GG and a pair of natural isomorphisms FG1F G \cong 1 and 1GF1 \cong G F satisfying the triangle identities),

whereas considering

  • a functor with the structure of being a general equivalence (that is, merely a functor GG and a pair of natural isomorphisms FG1F G \cong 1 and 1GF1 \cong G F)

is fraught with peril. For instance, an adjoint inverse is unique up to unique isomorphism (much as a strict inverse is unique up to equality), while a weak inverse or anainverse is not. Including adjoint equivalences is also the only way to make a higher-categorical structure completely algebraic.

An example of a non-adjoint equivalence

Identify a group HH with its delooping. One can check the following:

  • Any equivalence F:HH:GF : H \leftrightarrows H : G of a group with itself comprises two automorphisms F,GF, G, such that FGF G and GFG F are inner. The unit and counit are the group elements g ρg_{\rho} such that GF(k)=g ρkg ρ 1GF(k) = g_{\rho} k g_{\rho}^{-1} and g σg_{\sigma} such that FG(k)=g σ 1kg σFG(k) = g_{\sigma}^{-1} k g_{\sigma} for any kHk \in H.

  • Any equivalence of HH with itself where FF and GG are themselves also inner is an adjoint equivalence.

  • If HH has trivial center, then any equivalence of HH with itself is an adjoint equivalence.

  • To obtain a non-adjoint equivalence, we therefore need a group HH with nontrivial center and nontrivial outer automorphisms, such that we can pick two whose products are inner.

  • So take H=KH = K the Klein 4-group. This is a product of abelian groups, so abelian, so is its own center. In fact, it’s /2×/2\mathbb{Z}/2 \mathbb{Z} \times \mathbb{Z} / 2 \mathbb{Z}, so let F=GF = G the automorphism which interchanges coordinates. FG=GF=id KFG = GF = \operatorname{id}_{K}, which is given by conjugation by any element.

  • If this were adjoint, the triangle equality for FF will stipulate that F(g ρ)=g σ 1F(g_{\rho}) = g_{\sigma}^{-1}. We can pick g ρg_{\rho} and g σg_{\sigma} to break this. For example, let g ρg_{\rho} be (1,1)(1,1) and let g σg_{\sigma} be (0,1)(0,1).

This is a special case of the fact that, given a non-adjoint equivalence, you can always replace its unit with another unit (which determines the counit) to improve the equivalence to an adjoint equivalence.

In higher categories

All of the above types of equivalence make sense for nn-categories and \infty-categories defined using an algebraic definition of higher category; again, it is the weak notion that is usually wanted. When using a geometric definition of higher category, often isomorphism cannot even be written down, so equivalence comes more naturally.

In particular, one expects (although a proof depends on the exact definition and hasn't always been done) that in any (n+1)(n+1)-category of nn-categories, every equivalence (in the sense of an (n+1)(n+1)-category) will be essentially kk-surjective for all 0kn+10\le k\le n+1; this is the nn-version of “full, faithful, and essentially surjective.” The converse should be true assuming that

  • we have an axiom of choice and use weak (pseudo) nn-functors, or
  • we use nn-anafunctors? (which are automatically weak).

If we use too strict a notion of nn-functor, then we will not get the correct notion of equivalence; if we use weak nn-functors but not anafunctors, then we will get the correct notion of equivalence only if the axiom of choice holds, although again this can be corrected by moving to a span. Note that even strict nn-categories need weak nn-functors to get the correct notion of equivalence between them!

For example, assuming choice, a strict 2-functor between strict 22-categories is an equivalence in BicatBicat if and only if it is essentially (up to equivalence) surjective on objects, locally essentially surjective, and locally fully faithful. However, its weak inverse may not be a strict 22-functor, and even if it is, the equivalence transformations need not be strictly 22-natural. Thus, it need not be an equivalence in the strict 3-category Str2CatStr 2 Cat of 22-categories, strict 22-functors, and strict 22-natural transformations, or even in the semi-strict 3-category? GrayGray of strict 22-categories, strict 22-functors, and pseudonatural transformations.

As with CatCat, we can recover BicatBicat as a full subtricategory of GrayGray by formally inverting all such weak equivalences. Note that even with the axiom of choice, BicatBicat is not equivalent (as a tricategory) to GrayGray, even though by the coherence theorem for tricategories it is equivalent to some GrayGray-category; see here.

basic properties of…

Last revised on February 28, 2024 at 16:47:16. See the history of this page for a list of all contributions to it.