Chapters 1 and 2 use the rebuild2 formalization. Agda links for Chapter 3 remain temporarily unavailable.
3.3 Localizations
In ordinary category theory, if one is given a category \(C\) equipped with a collection of morphisms \(W\) in \(C\), one may form the localization of \(C\) at \(W\): the initial functor \(C \to C[W^{-1}]\) out of \(C\) which sends all morphisms in \(W\) to isomorphisms. Our goal in this section is to define localizations in the context of synthetic category theory.
Construction 3.3.1. Let \(C\) be a category equipped with a collection of morphisms \(w\colon W \hookrightarrow \Map ([1],C)\), in the sense of Definition 3.1.6. We will construct for every category \(D\) a full subcategory \[ \Fun ^W(C,D) \subseteq \Fun (C,D) \] In order to do this, we first define the anima \(\Map ^W(C,D)\) via the following pullback square:
where the top right vertical map is the map from Construction 3.1.1. The bottom map is induced by the embedding \(\pi _{\Iso }^{\simeq }\) from Lemma 2.3.3 and hence is an embedding. It follows that also \(\lambda ^W_{C,D}\) is an embedding. We can now define \[ \Fun ^W(C,D) := \langle \Map ^W(C,D) \subseteq \Fun (C,D) \rangle . \] In particular, the map \(\lambda ^W_{C,D}\) extends to a functor \(\tilde {\lambda }^W_{C,D}\colon \Fun ^W(C,D) \to \Fun (C,D)\). We may think of the category \(\Fun ^W(C,D)\) as the full subcategory of \(\Fun (C,D)\) spanned by those functors sending the morphisms in \(W\) to isomorphisms in \(D\).
Remark 3.3.2. The construction of \(\Fun ^W(C,D)\) is functorial in the pair \((C,W)\): if \(C'\) is another category equipped with a collection of morphisms \(w'\colon W' \hookrightarrow \Map ([1],C')\) and \(f\colon C \to C'\) is a functor which sends morphisms in \(W\) to morphisms in \(W'\) (in the sense of Definition 3.1.15), then for every category \(D\) there is an induced square
which in turn induces a commutative diagram
via Construction 3.1.16.
Before moving on to the localization axiom, we will establish some basic results that express that the categories \(\Fun ^W(C,D)\) behave as we expect. As a first result, we show that every functor \(C \to D\) lies in \(\Fun ^W(C,D)\) whenever \(D\) is a groupoid:
Lemma 3.3.3. Let \(C\) be a category equipped with a collection of morphisms \(W \hookrightarrow \Map ([1],C)\), and let \(\Gamma \) be a groupoid. Then the functor \[ \Fun ^W(C,\Gamma ) \to \Fun (C,\Gamma ) \] is an equivalence.
Proof
Proof. The functor \(\Iso (\Gamma )^{\simeq } \to \Map ([1],\Gamma )\) is an equivalence, since \(\Gamma \) is a groupoid. It follows from its defining property that also the map \(\Map ^W(C,\Gamma ) \to \Map (C,\Gamma )\) is an equivalence, and hence both sides define the same full subcategory of \(\Fun (C,\Gamma )\). Since the full subcategory determined by \(\Map (C,\Gamma )\) is just \(\Fun (C,\Gamma )\) by Lemma 3.2.9, this finishes the proof. □
The following lemma expresses the fact that any functor \(C \to D\) takes isomorphisms in \(C\) to isomorphisms in \(D\):
Proposition 3.3.4. In the case of \(W := \Iso (C)^{\simeq } \hookrightarrow \Map ([1],C)\), the forgetful functor \[ \Fun ^W(C,D) \to \Fun (C,D) \] is an equivalence.
Proof
Proof. Since the comparison map is the embedding of a full subcategory by construction, it suffices to prove that it induces an equivalence on objects. In other words, it suffices to check that the induced map \[ \Map ^W(C,D) \to \Map (C,D) \] is an equivalence. Since this is an embedding of animae, it suffices to check that any functor of the form \(f\colon C\to D\) has the property that the induced map \[ f_*\colon \Map ([1],C)\to \Map ([1],D) \] sends isomorphisms of \(C\) to isomorphisms of \(D\). For this, since there is a canonical equivalence \(C^\simeq \simeq \Iso (C)^\simeq \) given by the rule \(x\mapsto \id _x\), it suffices to check that \(f(\id _x) = \id _{f(x)}\) holds for any object \(x\) of \(C\). This is the identity comparison for the functor \(f\). □
Construction 3.3.5. Let \(l\colon C \to L\) be a functor which sends all morphisms in \(W\) to isomorphisms in \(L\), in the sense of Definition 3.1.15. Then we see that for every category \(D\) the induced map \(l^*\colon \Fun (L,D) \to \Fun (C,D)\) factors through \(\Fun ^W(C,D)\), using the following composite: \[ \Fun (L,D) \simeq \Fun ^{\Iso (L)^{\simeq }}(L,D) \xrightarrow {l^*} \Fun ^W(C,D). \] Here the map \(l^*\) is obtained via Remark 3.3.2.
Definition 3.3.6 (Localization). Given a collection of morphisms \(W\) in \(C\), we say that a functor \(l\colon C \to L\) is a localization of \(C\) at \(W\) if it sends all morphisms in \(W\) to isomorphisms in \(L\) and is universal with respect to this property: for every category \(D\), the functor \[ l^*\colon \Fun (L,D) \to \Fun ^W(C,D) \] is an equivalence. A functor \(l\colon C \to L\) is called a localization functor if it is a localization of \(C\) at some collection of morphisms \(W\).
If a localization exists, it is unique; see Exercise 3.8.4. We will frequently denote it by \(C[W^{-1}]\), and refer to the functor \(l\colon C \to C[W^{-1}]\) as the localization functor.
Axiom I (Localization axiom). For every collection of morphisms \(w\colon W \hookrightarrow \Map ([1],C)\) in \(C\) there exists a localization \(l\colon C \to C[W^{-1}]\) of \(C\) at \(W\).
Proposition 3.3.7. Given a collection of morphisms \(W\) in a category \(C\) as well as a functor \(\lambda \colon C\to L\) sending all morphisms in \(W\) to isomorphisms in \(L\), assume that, for every category \(D\), the induced map \[ \lambda ^*\colon \Map (L,D)\to \Map ^W(C,D) \] is an equivalence. Then \(\lambda \) exhibits \(L\) as a localization of \(C\) at \(W\).
Proof
Proof. Let \(l\colon C\to C[W^{-1}]\) be a localization of \(C\) at \(W\). Then the induced map \[ l^*\colon \Map (C[W^{-1}],D)\to \Map ^W(C,D) \] is an equivalence because it is the map on groupoid cores induced by the equivalence \(l^*\colon \Fun (C[W^{-1}],D)\iso \Fun ^W(C,D)\). Since \(l\) inverts \(W\), the assumption on \(L\) implies that there exists a functor \(u\colon L \to C[W^{-1}]\) equipped with an identification \(u \circ \lambda = l\). To see that \(u\) is an equivalence, consider for every category \(D\) the commutative triangle
By Proposition 1.4.11, it suffices to show that \(u^*\) is an equivalence for every category \(D\). This is immediate by the 2-out-of-3 property as both diagonal maps are equivalences.
Thus \(u\) is an equivalence compatible with the maps out of \(C\), and the universal property of \(l\) transfers to \(\lambda \). □
Remark 3.3.8. The previous proposition and the localization axiom give a pushout square
where the map \(\tilde {w}\) is obtained by uncurrying the composite \(W \xrightarrow {w} \Map ([1],C) \to \Fun ([1],C)\); see Exercise 3.8.5.
Construction 3.3.9. The construction \(C \mapsto C[W^{-1}]\) is functorial in the pair \((C,W)\): if \(D\) is another category equipped with a collection of morphisms \(W'\) and \(f\colon C \to D\) is a functor which sends \(W\) to \(W'\), the composite \(C \to D \to D[{W'}^{-1}]\) sends all morphisms in \(W\) to isomorphisms, and hence induces a canonical dashed functor making the square commute:
