The generalized pullback lemma [frct-0014]

In light of our discussion of the fundamental self-indexing, the following result for displayed categories generalizes the ordinary “pullback lemma.”

Lemma. Generalized pullback lemma [frct-001H]

Let \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\), and suppose that \({\bar {y}}\xrightarrow [g]{\bar {g}}{\bar {z}}\) is cartesian over \(g\). Then \(\bar {f};\bar {g}\) is cartesian over \(f;g\) if and only if \(\bar {f}\) is cartesian over \(f\).

Proof. 

Suppose first that \(\bar {f}\) is cartesian. To see that \(\bar {f};\bar {g}\) is cartesian, we must construct a unique factorization as follows:

Because \(\bar {g}\) is cartesian, we can factor \(\bar {h} = i;\bar {g}\) for a unique \({\bar {u}}\xrightarrow [m;f]{i}{\bar {y}}\). Then, because \(\bar {f}\) is cartesian, we can further factor \(i = j;\bar {f}\) for a unique \({\bar {u}}\xrightarrow [m]{j}{\bar {x}}\). We conclude that there is a unique \({\bar {u}}\xrightarrow [m]{j}{\bar {x}}\) for which \(\bar {h} = j;\bar {f};\bar {g}\), as required.

Conversely, suppose that \(\bar {f};\bar {g}\) is cartesian. To see that \(\bar {f}\) is cartesian, we must construct a unique factorization as follows:

Because \(\bar {f};\bar {g}\) is cartesian, we can factor \(\bar {h};\bar {g} = i;\bar {f};\bar {g}\) for a unique \({\bar {u}}\xrightarrow [m]{i}{\bar {x}}\). On the other hand, because \(\bar {g}\) is cartesian, there is a unique \({\bar {u}}\xrightarrow [m;f]{j}{\bar {y}}\) for which \(\bar {h};\bar {g} = j;\bar {g}\); as both \(\bar {h}\) and \(i;\bar {f}\) satisfy this condition, we conclude \(\bar {h}=i;\bar {f}\). Therefore, there is a unique \({\bar {u}}\xrightarrow [m]{i}{\bar {x}}\) for which \(\bar {h} = i;\bar {f}\), as required.

Context

    Displayed categories and fibrations [frct-0008]

    Definition. Displayed category [frct-0000]

    Let \(B\) be a category. A displayed category \(E\) over \(B\) is defined by the following data according to (Ahrens and Lumsdaine):

    1. for each object \(x\in B\), a collection of displayed objects \(E_{x}\),
    2. for each morphism \({x}\xrightarrow {{f}}{y}\in B\) and displayed objects \(\bar {x}\in E_{x}\) and \(\bar {y}\in E_{y}\), a family of collections of displayed morphisms \(\mathbf {hom}_{E_{f}}{\mathopen {}\left (\bar {x},\bar {y}\right )\mathclose {}}\), an element of which shall denote by \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\),
    3. for each \(x\in B\) and \(\bar {x}\in E_{x}\), a displayed morphism \({\bar {x}}\xrightarrow [1_{x}]{1_{\bar {x}}}{\bar {x}}\),
    4. for each \({x}\xrightarrow {{f}}{y}\) and \({y}\xrightarrow {{g}}{z}\) in \(B\) and objects \(\bar {x}\in E_{x}, \bar {y}\in E_{y}, \bar {z}\in E_{z}\), a function \[ \mathbf {hom}_{E_{f}}{\mathopen {}\left (\bar {x},\bar {y}\right )\mathclose {}} \times \mathbf {hom}_{E_{g}}{\mathopen {}\left (\bar {y},\bar {z}\right )\mathclose {}} \to \mathbf {hom}_{E_{f;g}}{\mathopen {}\left (\bar {x},\bar {z}\right )\mathclose {}} \] that we will denote like ordinary (diagrammatic) function composition,
    5. such that the following equations hold: \[ 1_{\bar {x}};\bar {h} = \bar {h}\qquad \bar {h};1_{\bar {y}} = \bar {h}\qquad \bar {f};(\bar {g};\bar {h}) = (\bar {f};\bar {g});\bar {h} \] Note that these are well-defined because of the corresponding laws for the base category \(B\).

    Notation. Square brackets for subscripts [frct-003R]

    • December 27, 2022

    When we have too many subscripts, we will write \(E[x]\) instead of \(E_{x}\).

    Definition. Cartesian morphism [frct-0001]

    Let \(E\) be displayed over \(B\), and let \({x}\xrightarrow {{f}}{y} \in B\); a morphism \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) in \(E\) is called cartesian over \(f\) when for any \({u}\xrightarrow {{m}}{x}\) and \({\bar {u}}\xrightarrow [m;f]{\bar {h}}{\bar {y}}\) there exists a unique \({\bar {u}}\xrightarrow [m]{\bar {m}}{\bar {x}}\) with \(\bar {m};\bar {f} = \bar {h}\). We visualize this unique factorization of \(\bar {h}\) through \(\bar {f}\) over \(m\) as follows:

    Above we have used the “pullback corner” to indicate \(\bar {x}\to \bar {y}\) as a cartesian map. We return to this in our discussion of the self-indexing of a category.

    Definition. Cleaving of a displayed category [frct-003T]

    Let \(E\) be a displayed category over \(C\); following Ahrens and Lumsdaine, we define a cleaving of \(E\) to be a function assigning to each \({x}\xrightarrow {{f}}{y}\in C\) and \(u\in C_y\) a cartesian morphism \({f^{*}u}\xrightarrow [f]{\bar {f}}{u}\) in \(E\) called the chosen cartesian lift of \(u\) along \(f\).

    Remark. Cleavings from the axiom of choice [frct-003U]

    Assuming the axiom of choice, any cartesian fibration may be equipped with a (non-canonical) cleaving. In the current version of these notes, we freely use this principle, but in the future we would like to follow Ahrens and Lumsdaine in distinguishing between weak and strong fibrations, in which the latter come equipped with cleavings.

    Definition. Cartesian fibration [frct-0002]

      A displayed category \(E\) over \(B\) is said to be a cartesian fibration, when for each morphism \({x}\xrightarrow {{f}}{y}\) and displayed object \(\bar {y}\in E_{y}\), there exists a displayed object \(\bar {x}\in E_{x}\) and a cartesian morphism \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\). Note that the pair \((\bar {x},\bar {f})\) is unique up to unique isomorphism, so being a cartesian fibration is a property of a displayed category.

      We will also refer to cartesian fibrations as simply fibrations or fibered categories.

      There are other variations of fibration. For instance, \(E\) is said to be an isofibration when the condition above holds just for isomorphisms \(f : x\cong y\) in the base.

      The fundamental self-indexing [frct-0003]

        Construction. The fundamental self-indexing [frct-001X]

          Let \(B\) be an ordinary category; there is an important displayed category \(\underline {B}\) over \(B\) given fiberwise by the slices of \(B\).

          1. For \(x\in B\), we define \(\underline {B}_{x}\) to be the collection \({B}_{/x}\) of pairs \((\bar {x}\in B,{\bar {x}}\xrightarrow {{p_{x}}}{x})\).
          2. For \({x}\xrightarrow {{f}}{y}\in B\), we define \(\underline {B}_{f}\) to be the collection of commuting squares in the following configuration:

          Exercise. Pullbacks and cartesian maps [frct-001Y]

            Prove that the fundamental self-indexing \(\underline {B}\) is a cartesian fibration if and only if \(B\) has pullbacks.

            The generalized pullback lemma [frct-0014]

            In light of our discussion of the fundamental self-indexing, the following result for displayed categories generalizes the ordinary “pullback lemma.”

            Lemma. Generalized pullback lemma [frct-001H]

            Let \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\), and suppose that \({\bar {y}}\xrightarrow [g]{\bar {g}}{\bar {z}}\) is cartesian over \(g\). Then \(\bar {f};\bar {g}\) is cartesian over \(f;g\) if and only if \(\bar {f}\) is cartesian over \(f\).

            Proof. 

            Suppose first that \(\bar {f}\) is cartesian. To see that \(\bar {f};\bar {g}\) is cartesian, we must construct a unique factorization as follows:

            Because \(\bar {g}\) is cartesian, we can factor \(\bar {h} = i;\bar {g}\) for a unique \({\bar {u}}\xrightarrow [m;f]{i}{\bar {y}}\). Then, because \(\bar {f}\) is cartesian, we can further factor \(i = j;\bar {f}\) for a unique \({\bar {u}}\xrightarrow [m]{j}{\bar {x}}\). We conclude that there is a unique \({\bar {u}}\xrightarrow [m]{j}{\bar {x}}\) for which \(\bar {h} = j;\bar {f};\bar {g}\), as required.

            Conversely, suppose that \(\bar {f};\bar {g}\) is cartesian. To see that \(\bar {f}\) is cartesian, we must construct a unique factorization as follows:

            Because \(\bar {f};\bar {g}\) is cartesian, we can factor \(\bar {h};\bar {g} = i;\bar {f};\bar {g}\) for a unique \({\bar {u}}\xrightarrow [m]{i}{\bar {x}}\). On the other hand, because \(\bar {g}\) is cartesian, there is a unique \({\bar {u}}\xrightarrow [m;f]{j}{\bar {y}}\) for which \(\bar {h};\bar {g} = j;\bar {g}\); as both \(\bar {h}\) and \(i;\bar {f}\) satisfy this condition, we conclude \(\bar {h}=i;\bar {f}\). Therefore, there is a unique \({\bar {u}}\xrightarrow [m]{i}{\bar {x}}\) for which \(\bar {h} = i;\bar {f}\), as required.

            An alternative definition of fibration [frct-0029]

            Warning. Competing terminologies for cartesian maps [frct-003S]

            Some authors including Grothendieck give an equivalent definition of cartesian fibration that factors through a nonequivalent definition of cartesian morphisms. Such authors refer to our notion of cartesian morphism as “hypercartesian” (see Streicher).

            Definition. Hypocartesian morphisms [frct-002A]

            Let \(E\) be displayed over \(B\), and let \(f:x\to y \in B\); a morphism \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) in \(E\) is called hypocartesian over \(f\) when for any \(\bar {u}\in E_{x}\) and \({\bar {u}}\xrightarrow [f]{\bar {h}}{\bar {y}}\) there exists a unique \({\bar {u}}\xrightarrow [1_{x}]{i}{\bar {x}}\) with \(i;\bar {f} = \bar {h}\) as follows:

            Remark. Hypocartesian morphisms need not be closed composable [frct-003G]

            Cartesian morphisms are clearly hypocartesian (setting \(u=x\) and \(m=1_{x}\)), but the converse does not hold. The problem is that in an arbitrary displayed category, hypocartesian morphisms may not be closed under composition.

            Lemma. Hypocartesian = cartesian in a cartesian fibration [frct-002C]

              Let \(E\) be a cartesian fibration, and let \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) be displayed over \({x}\xrightarrow {{f}}{y}\). The displayed morphism \(\bar {f}\) is cartesian if and only if it is hypocartesian.

              Proof. 

                Any cartesian map is clearly hypocartesian. To see that a hypocartesian map \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) in a cartesian fibration is cartesian, we consider the cartesian lift of \({x}\xrightarrow {{f}}{y}\) under \(\bar {y}\):

                As the cartesian lift \(\bar {x}'\to \bar {y}\) is also hypocartesian, it follows that there is a unique vertical isomorphism identifying \(\bar {x}\) with \(\bar {x}'\) factoring \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) through \({\bar {x}'}\xrightarrow [f]{\bar {f}'}{\bar {y}}\). Being cartesian over \(f\) is clearly stable under isomorphism, hence we conclude that \(\bar {f}\) is cartesian from the fact that \(\bar {f}'\) is cartesian.

                Grothendieck defines a fibration in terms of (what we refer to as) hypocartesian morphisms rather than (what we refer to as) cartesian morphisms, and therefore imposes the additional constraint that the hypocartesian morphisms be closed under composition. Below, we verify that these two definitions of cartesian fibration coincide.

                Lemma. Equivalence with Grothendieck's fibrations [frct-002B]

                Let \(E\) be displayed over \(B\). Then \(E\) is a cartesian fibration if and only if the following two conditions hold:

                1. Hypocartesian lifts. For each \(f:x\to y\in B\) and \(\bar {y}\in E_{y}\) there exists a displayed object \(\bar {x}\in E_{x}\) and hypocartesian morphism \(\bar {f}:\bar {x}\xrightarrow [f]{}\bar {y}\).
                2. Closure under composition. If \(\bar {f}:\bar {x}\xrightarrow [f]{}\bar {y}\) and \(\bar {g}:\bar {y}\xrightarrow [g]{}\bar {z}\) are hypocartesian, then \(\bar {f};\bar {g}\) is hypocartesian.

                Proof. 

                Suppose first that \(E\) is a cartesian fibration in our sense. Then \(E\) has hypocartesian lifts because it has cartesian lifts. For closure under composition, fix hypocartesian \(\bar {f},\bar {g}\); because hypocartesian and cartesian maps coincide in a cartesian fibration we know that \(\bar {f},\bar {g}\) are also cartesian and hence by the generalized pullback lemma so is the composite \(\bar {f};\bar {g}\); therefore it follows that \(\bar {f};\bar {g}\) is also hypocartesian.

                Conversely, suppose that \(E\) is a cartesian fibration in the sense of Grothendieck, and let \(\bar {f}:\bar {x}\xrightarrow [f]{}\bar {y}\) be the hypocartesian lift of \(f:x\to y\) at \(\bar {y}\in E_{y}\); we shall see that \(\bar {f}\) is also a cartesian lift of \(f\) at \(\bar {y}\) by constructing a unique factorization as follows:

                Let \(\bar {m}:\bar {u}'\xrightarrow [m]{}\bar {x}\) be the hypocartesian lift of \(m\) at \(\bar {x}\), where \(\bar {u}'\in E_{u}\). By hypothesis, the composite \(\bar {m};\bar {f} : \bar {u}'\xrightarrow [m;f]{}\bar {y}\) is hypocartesian, so \(\bar {h}\) factors uniquely through \(\bar {m};\bar {f}\) over \(1_{u}\):

                The composite \(i;\bar {m} : \bar {u}\xrightarrow [m]{}\bar {x}\) is the required (cartesian) factorization of \(\bar {h}\) through \(\bar {f}\) over \(m\). To see that \(i;\bar {m}\) is the unique such map, we observe that all morphisms \(\bar {u}\xrightarrow [m]{}\bar {x}\) factor uniquely through \(\bar {m}\) over \(1_{u}\) as a consequence of \(\bar {m}\) being hypocartesian.

                Remark. Two ways to generalize pullbacks [frct-002D]

                  Hypocartesian and cartesian morphisms can be thought of as two distinct ways to generalize the concept of a pullback, depending on what one considers the essential properties of pullbacks. Hypocartesian morphisms more directly generalize the “little picture” universal property of pullbacks as limiting cones, whereas cartesian morphisms generalize the “big picture” dynamics of the pullback pasting lemma. As we have seen, these two notions coincide in any cartesian fibration; the instance of this result for the fundamental self-indexing verifies that pullbacks can be equivalently presented in terms of cartesian morphisms.

                  Displayed and fibered functors [frct-0004]

                    Let \(E\) be displayed over \(B\) and let \(F\) be displayed over \(C\). If \({B}\xrightarrow {{U}}{C}\) is an ordinary functor, than a displayed functor from \(E\) to \(F\) over \(U\) is given by the following data:

                    1. for each displayed object \(\bar {x}\in E_{x}\), a displayed object \(\bar {U}\bar {x}\in F_{Ux}\),
                    2. for each displayed morphism \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\), a displayed morphism \({\bar {U}\bar {x}}\xrightarrow [Uf]{\bar {U}\bar {f}}{\bar {U}\bar {y}}\),
                    3. such that the assignment \(\bar {U}f\) preserves displayed identities and displayed composition.

                    From this notion, we can see that the variation of displayed categories over their base categories itself has a “displayed categorical” structure; up to size issues, we could speak of the displayed bicategory of displayed categories.

                    Note. The correct notion of morphism between cartesian fibrations is given by displayed functors that preserve cartesian maps. We will call these fibered functors.

                    Fiber categories and vertical maps [frct-0005]

                      Let \(E\) be a category displayed over \(B\). A vertical map in \(E\) is defined to be one that lies over the identity map in \(B\). For every \(b\in B\), there the collection \(E_{b}\) of displayed objects has the structure of a category; in particular, we set \(\mathbf {hom}_{E_{b}}{\mathopen {}\left (u,v\right )\mathclose {}}\) to be the collection of vertical maps \(u\xrightarrow [1_{b}]{}v\).

                      Opposite categories [frct-000Q]

                      We adapt Bénabou’s construction as reported by Streicher. Our first construction works for an uncloven fibration, but it has the downside that it requires us to treat the collection of cartesian lifts as a set that can be quotiented, whereas our second construction avoids this by virtue of a cleaving. Up to equivalence, the two constructions coincide for a cloven fibration, which shows that our second construction is independent of the chosen cleaving.

                      Construction. The opposite of an uncloven fibration [frct-001Z]

                        Let \(E\) be fibered over \(B\); we may define the opposite fibered category \(E^{\mathsf {op}}\) over \(B\) like so:

                        1. An object of \(E^{\mathsf {op}}_{x}\) is given by an object of \(E_{x}\).

                        2. Given \({x}\xrightarrow {{f}}{y}\in B\), a morphism \(\bar {x}\xrightarrow [f]{} \bar {y}\) in \(E^{\mathsf {op}}\) is given in terms of \(E\) by a cartesian map \({\bar {y}_{x}}\xrightarrow [f]{\bar {y}_{f}}{\bar {y}}\) together with a vertical map \({\bar {y}_{x}}\xrightarrow [1_{x}]{h}{\bar {x}}\) as depicted below:

                          such that \({\mathopen {}\left \{\bar {x} \leftarrow \bar {y}_{x}^{1}\to \bar {y}\right \}\mathclose {}}\) is identified with \({\mathopen {}\left \{\bar {x}\leftarrow \bar {y}_{x}^{2}\to \bar {y}\right \}\mathclose {}}\) when they agree up to the unique vertical isomorphism \(\bar {y}_{x}^{1}\cong \bar {y}_{x}^{2}\) induced by the universal property of cartesian maps in the sense that the following diagram commutes:

                        Construction. The opposite of a cloven fibration [frct-003W]

                        Let \(E\) be a cloven fibration over \(B\); in this case, we may use the cleaving of \(E\) to give a simple construction of the opposite fibration \(E^{\mathsf {op}}\).

                        1. A displayed object of \(E^{\mathsf {op}}\) over \(x\in B\) is given by an object of \(E\) over \(x\).
                        2. Given \({x}\xrightarrow {{f}}{u}\in B\), a displayed morphism \(\bar {x}\xrightarrow [f]{}\bar {y}\) in \(E^{\mathsf {op}}\) is given by a vertical map \({f^{*}\bar {y}}\xrightarrow [1_{x}]{h}{\bar {x}}\).

                        Going forward, we will not be sensitive to the difference between the two constructions of opposite fibrations.

                        Cartesian maps in the opposite category [frct-000T]

                          There is a simple characterization of cartesian maps in \(E^{\mathsf {op}}\).

                          Lemma. Characterization of cartesian maps [frct-0020]

                            A morphism \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\in E^{\mathsf {op}}\) is cartesian over \({x}\xrightarrow {{f}}{y}\) if and only if the vertical leg of \(f\) is an isomorphism.

                            Proof. 

                              Suppose that \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) is represented by a span \({\mathopen {}\left \{\bar {x}\leftarrow \bar {y}_{x}\to \bar {y}\right \}\mathclose {}}\) in \(E\) in which the vertical leg \(\bar {x}\leftarrow \bar {y}_{x}\) is an isomorphism. We must show that \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\) is cartesian in \(E^{\mathsf {op}}\). We fix a morphism \({\bar {w}}\xrightarrow [m;f]{\bar {h}}{\bar {y}}\in E^{\mathsf {op}}\) where \({w}\xrightarrow {{m}}{x}\), depicted below in terms of \(E^{\mathsf {op}}\):

                              We must define the unique intervening map \({\bar {w}}\xrightarrow [m]{}{\bar {x}}\) in \(E^{\mathsf {op}}\). We first translate the above into the language of \(E\) by unfolding definitions:

                              The desired intervening map \(\bar {w}\xrightarrow [m]{} \bar {x}\in E^{\mathsf {op}}\) shakes out in the language of \(E\) to be a span \({\mathopen {}\left \{\bar {w}\xleftarrow [1_{w}]{} \bar {y}_{w}\xrightarrow [m]{} \bar {x}\right \}\mathclose {}}\) in which the left-hand leg is vertical and the right-hand leg is cartesian over \({w}\xrightarrow {{m}}{x}\). But the left-hand span \({\mathopen {}\left \{\bar {w}\xleftarrow [1_{w}]{}\bar {y}_{w}\to \bar {y}_{x}\cong \bar {x}\right \}\mathclose {}}\) in the diagram above is exactly what we need.

                              We leave the converse to the reader.

                              Cartesian lifts in the opposite category [frct-000U]

                                The foregoing characterization of cartesian maps in \(E^{\mathsf {op}}\) immediately implies that \(E^{\mathsf {op}}\) is fibered over \(B\).

                                Corollary.  [frct-0021]

                                  The displayed category \(E^{\mathsf {op}}\) is a cartesian fibration.

                                  Proof. 

                                    Fixing \(\bar {y}\in E^{\mathsf {op}}_{y}\) and \(f:x\to y\in B\), we must exhibit a cartesian lift \(\bar {f} : \bar {x}\xrightarrow [f]{}\bar {y}\in E^{\mathsf {op}}\). By the characterization it suffices to find any map over \(f\) whose vertical component is an isomorphism. Writing \(\bar {y}_{x}\xrightarrow [f]{}\bar {y}\) for the cartesian lift of \(f\) in \(E\), consider the map in \(E^{\mathsf {op}}\) presented by the following span in \(E\):

                                    Exegesis of opposite categories [frct-000S]

                                      The construction of fibered opposite categories does appear quite involved, but it can be seen to be inevitable from the perspective of the fiber categories \(E^{\mathsf {op}}_{x}\). Indeed, let \(u,v\in E^{\mathsf {op}}_{x}\) and fix a vertical map \(h : u \to v\in E^{\mathsf {op}}_{x}\); by unfolding definitions, we see that the vertical map \(h : u \to v\) is uniquely determined by a morphism \(v\to u\in E_{x}\).

                                      Proof. 

                                        A displayed morphism \(u\xrightarrow [1_{x}]{} v\in E^{\mathsf {op}}\) is determined by a span \({\mathopen {}\left \{u\leftarrow v_{x} \to v\right \}\mathclose {}}\in E\) where the right-hand map is cartesian over \(1_{x} : x\to x\) and the left-hand map is vertical, taken up to the identification of different cartesian lifts \(v_{x}\to x\). A displayed morphism that is cartesian over the identity is an isomorphism; hence, displayed morphisms \(u\xrightarrow [1_{x}]{} v\in E^{\mathsf {op}}\) are equivalently determined by vertical maps \(v\to u \in E\).

                                        Example. The family fibration [frct-0006]

                                        Any ordinary category \(C\) can be viewed as a displayed category \(\boldsymbol {\mathcal {F}}_{C}\) over \(\mathbf {Set}\):

                                        1. For \(S\in \mathbf {Set}\), an object in \(\boldsymbol {\mathcal {F}}_{C}[S]\) is specified by a functor \(C^S\) where \(S\) is regarded as a discrete category.
                                        2. Given \(f : S \to T\) in \(\mathbf {Set}\) and \(x\in C^S\) and \(y\in C^T\), a morphism \(x \xrightarrow [f]{} y\) is given by a morphism \(x\to f^{*}y\) in \(C^S\) where \({C^T}\xrightarrow {{f^{*}}}{C^S}\) is precomposition with \(f\).

                                        The displayed category \(\boldsymbol {\mathcal {F}}_{C}\) is in fact a cartesian fibration. This family fibration is the starting point for developing a relative form of category theory, the purpose of this lecture. By analogy with viewing an ordinary category \(C\) as a fibration \(\boldsymbol {\mathcal {F}}_{C}\) over \(\mathbf {Set}\), we may reasonably define a “relative category” over another base \(B\) to be a fibration over \(B\).

                                        This story for relative category theory reflects the way that ordinary categories are “based on” \(\mathbf {Set}\) in some sense in spite of the fact that they do not necessarily have sets of objects or even sets of morphisms between objects. Being small and locally small respectively will later be seen to be properties of a family fibration over an arbitrary base \(B\), strictly generalizing the classical notions.

                                        Construction. Cleaving the family fibration [frct-003V]

                                        The family fibration can be cloven, constructively. In particular, let \(C\) be a category and consider the family fibration \(\boldsymbol {\mathcal {F}}_{C}\) over \(\mathbf {Set}\); let \({T}\xrightarrow {{f}}{S}\) be a function between sets and let \(u\in C^S\) be an \(S\)-indexed family of objects of \(C\). The family \(f^{*}u = f;u\in C^T\) is the object part of a cartesian lift for \(u\) along \(f\). The cartesian morphism \({f^{*}u}\xrightarrow [f]{\bar {f}}{u}\in \boldsymbol {\mathcal {F}}_{C}\) is given by the identity map \({f^{*}u}\xrightarrow {{1_{f^{*}u}}}{f^{*}u}\in C^T\).

                                        Construction. Change of base of displayed categories [frct-0007]

                                          Suppose that \(E\) is displayed over \(B\) and \({X}\xrightarrow {{F}}{B}\) is a functor; then we may define a displayed category \(F^{*}E\) as over \(X\) follows:

                                          1. An object of \((F^{*}E)_{x}\) is an object of \(E_{Fx}\).
                                          2. Given \(\bar {x}\in (F^{*}E)_{x}\), \(\bar {y}\in (F^{*}E)_{y}\) and \(f : x \to y\), a morphism \(\bar {x}\xrightarrow [f]{}\bar {y}\) in \(F^{*}E\) is given by a morphism \(\bar {x}\xrightarrow [Ff]{}\bar {y}\) in \(E\).

                                          We visualize the change of base scenario as follows:

                                          Full subfibrations and figure shapes [frct-002J]

                                            In a category \(E\), a morphism \({x}\xrightarrow {{f}}{y}\) can be thought of as a “figure” of shape \(x\) drawn in \(y\). For instance, if \(x\) is the point (i.e. \(x=\mathbf {1}_{E}\)) then a morphism \(x\to y\) is a “point” of the “space” \(y\). We refer to \(x\) as the figure-shape in any such scenario. The perspective of morphisms as figures is developed in more detail by Lawvere and Schanuel.

                                            It often happens that a useful class of figure shapes can be arranged into a set-indexed family \({\mathopen {}\left (u_{i}\right )\mathclose {}}_{i\in I}\); viewed from the perspective of the family fibration \(\boldsymbol {\mathcal {F}}_{E}\), this family is just a displayed object \(\bar {u}\) over \(I\) and then a figure shape “in” this family is given by any cartesian morphism \(\bar {z}\to \bar {u}\). We will generalize this situation to the case of an arbitrary fibration, by constructing the full subfibration spanned by displayed objects equipped with a cartesian morphism into \(\bar {u}\) in the associated full subfibration below.

                                            Construction. The full subfibration associated to a displayed object [frct-0010]

                                              Let \(E\) be a cartesian fibration over \(B\); then any displayed object \(\bar {x} \in E_{x}\) induces a full subfibration \(\mathbf {Full}{\mathopen {}\left (\bar {u}\right )\mathclose {}}\subseteq E\) spanned by displayed objects that are classified by \(\bar {u}\), i.e. arise from \(\bar {u}\) by cartesian lift.

                                              1. An object of \(\mathbf {Full}{\mathopen {}\left (\bar {u}\right )\mathclose {}}_{x}\) is specified by an object \(\bar {x}\in E_{x}\) together with a cartesian morphism \(\bar {x}\to \bar {u}\).
                                              2. Given \({x}\xrightarrow {{f}}{y}\in B\), a morphism from \(\bar {x}\to \bar {u}\) to \(\bar {y}\to \bar {u}\in \) over \(f\) is given by any displayed morphism \(\bar {x}\xrightarrow [f]{}\bar {y}\).

                                              Definition. Figures and figure shapes in the full subfibration [frct-002K]

                                                Let \(E\) be a cartesian fibration and let \(\mathbf {Full}{\mathopen {}\left (\bar {s}\right )\mathclose {}}\subseteq E\) be the full subfibration determined by a displayed object \(\bar {s}\in E\). We now develop the following vocabulary:

                                                1. We will refer to each object of \(\mathbf {Full}{\mathopen {}\left (\bar {s}\right )\mathclose {}}\) as a \(\bar {s}\)-figure shape.
                                                2. A displayed morphism \(\bar {z}\to \bar {x}\) is called a \(\bar {s}\)-figure whenever \(\bar {z}\in \mathbf {Full}{\mathopen {}\left (\bar {s}\right )\mathclose {}}\).

                                                Definition. Agreement on a class of figure shapes [frct-002I]

                                                  Let \(\bar {s}\) be a displayed object in a cartesian fibration \(E\) over \(B\). A pair of displayed morphisms \({\bar {x}}\xrightarrow {{f,g}}{\bar {y}}\in E\) are said to agree on \(\bar {s}\)-figures when for any \(\bar {s}\)-figure \({\bar {z}}\xrightarrow {{h}}{\bar {x}}\), we have \({\bar {z}}\xrightarrow {{h;f = h;g}}{\bar {y}}\).

                                                  Backlinks

                                                    Lemma. Locally small externalization [frct-000Y]

                                                    The externalization is locally small.

                                                    Proof. 

                                                    Fix \(x\in E\) and \(u,v\in {\mathopen {}\left [C\right ]\mathclose {}}_{x}\), we must exhibit a terminal object to the (total) category \(\widetilde {\mathbf {H}_{{\mathopen {}\left [C\right ]\mathclose {}}_{x}}(u,v)}\) of “hom candidates”. First we define \({\mathopen {}\left [u,v\right ]\mathclose {}}\) to be the following pullback in \(E\):

                                                    We define \(\overline {p}:{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}{u}\xrightarrow [p]{} u\in {\mathopen {}\left [C\right ]\mathclose {}}_{{\mathopen {}\left [u,v\right ]\mathclose {}}}\) to be the cartesian lift of \(u\in {\mathopen {}\left [C\right ]\mathclose {}}_{x}\) along \(p:{\mathopen {}\left [u,v\right ]\mathclose {}}\to x\):

                                                    We need to define a displayed evaluation map \(\epsilon : {\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\xrightarrow [p]{} v\); unraveling the definition of a displayed morphism in the externalization of \(C\), we choose the following diagram:

                                                    Putting all this together, we assert that the terminal object of \(\widetilde {\mathbf {H}_{{\mathopen {}\left [C\right ]\mathclose {}}_{x}}(u,v)}\) is the following span in \({\mathopen {}\left [C\right ]\mathclose {}}\):

                                                    Fixing another such candidate hom span \({\mathopen {}\left \{u \leftarrow \bar {h}\rightarrow v\right \}\mathclose {}}\in \widetilde {\mathbf {H}_{{\mathopen {}\left [C\right ]\mathclose {}}_{x}}(u,v)}\), we must exhibit a unique cartesian morphism \(\bar \alpha : \bar {h}\to {\mathopen {}\left [u,v\right ]\mathclose {}}^{*}{u}\) making the following diagram commute:

                                                    First we note that the evaluation map \(\epsilon _{h} : \bar {h}\to v\) amounts to an internal morphism \(h\to C_{1}\) satisfying the appropriate compatibility conditions. Therefore we may define the base \(\alpha :h\to {\mathopen {}\left [u,v\right ]\mathclose {}}\) of the universal map using the universal property of the pullback that defines \({\mathopen {}\left [u,v\right ]\mathclose {}}\):

                                                    The morphism \(\alpha :h\to {\mathopen {}\left [u,v\right ]\mathclose {}}\) defined above is the unique map in \(E\) satisfying the conditions required of the base for \(\bar \alpha \); therefore, it suffices to show that there exists a cartesian morphism \(\bar \alpha :\bar {h}\xrightarrow [\alpha ]{}{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\) since it will be unique if it exists. We define \(\bar \alpha \) using the universal property of the cartesian lift:

                                                    That \(\bar {\alpha }:\bar {h}\xrightarrow [\alpha ]{}{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\) is cartesian follows from the generalized pullback lemma for cartesian morphisms: it suffices to observe that both \(\bar {p}_{h}:\bar {h}\to u\) and its second factor \(\bar {p}:{\mathopen {}\left [u,v\right ]\mathclose {}}^{*}u\to u\) are cartesian.

                                                    Related

                                                      The fundamental self-indexing [frct-0003]

                                                        Construction. The fundamental self-indexing [frct-001X]

                                                          Let \(B\) be an ordinary category; there is an important displayed category \(\underline {B}\) over \(B\) given fiberwise by the slices of \(B\).

                                                          1. For \(x\in B\), we define \(\underline {B}_{x}\) to be the collection \({B}_{/x}\) of pairs \((\bar {x}\in B,{\bar {x}}\xrightarrow {{p_{x}}}{x})\).
                                                          2. For \({x}\xrightarrow {{f}}{y}\in B\), we define \(\underline {B}_{f}\) to be the collection of commuting squares in the following configuration:

                                                          Exercise. Pullbacks and cartesian maps [frct-001Y]

                                                            Prove that the fundamental self-indexing \(\underline {B}\) is a cartesian fibration if and only if \(B\) has pullbacks.