## 4.32 Fibred categories

A very brief discussion of fibred categories is warranted.

Let $p : \mathcal{S} \to \mathcal{C}$ be a category over $\mathcal{C}$. Given an object $x \in \mathcal{S}$ with $p(x) = U$, and given a morphism $f : V \to U$, we can try to take some kind of “fibre product $V \times _ U x$” (or a *base change* of $x$ via $V \to U$). Namely, a morphism from an object $z \in \mathcal{S}$ into “$V \times _ U x$” should be given by a pair $(\varphi , g)$, where $\varphi : z \to x$, $g : p(z) \to V$ such that $p(\varphi ) = f \circ g$. Pictorially:

\[ \xymatrix{ z \ar@{~>}[d]^ p \ar@{-}[r] & ? \ar[r] \ar@{~>}[d]^ p & x \ar@{~>}[d]^ p \\ p(z) \ar[r] & V \ar[r]^ f & U } \]

If such a morphism $V \times _ U x \to x$ exists then it is called a strongly cartesian morphism.

Definition 4.32.1. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a category over $\mathcal{C}$. A *strongly cartesian morphism*, or more precisely a *strongly $\mathcal{C}$-cartesian morphism* is a morphism $\varphi : y \to x$ of $\mathcal{S}$ such that for every $z \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$ the map

\[ \mathop{Mor}\nolimits _\mathcal {S}(z, y) \longrightarrow \mathop{Mor}\nolimits _\mathcal {S}(z, x) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(z), p(x))} \mathop{Mor}\nolimits _\mathcal {C}(p(z), p(y)), \]

given by $\psi \longmapsto (\varphi \circ \psi , p(\psi ))$ is bijective.

Note that by the Yoneda Lemma 4.3.5, given $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$ lying over $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ and the morphism $f : V \to U$ of $\mathcal{C}$, if there is a strongly cartesian morphism $\varphi : y \to x$ with $p(\varphi ) = f$, then $(y, \varphi )$ is unique up to unique isomorphism. This is clear from the definition above, as the functor

\[ z \longmapsto \mathop{Mor}\nolimits _\mathcal {S}(z, x) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(z), U)} \mathop{Mor}\nolimits _\mathcal {C}(p(z), V) \]

only depends on the data $(x, U, f : V \to U)$. Hence we will sometimes use $V \times _ U x \to x$ or $f^*x \to x$ to denote a strongly cartesian morphism which is a lift of $f$.

Lemma 4.32.2. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a category over $\mathcal{C}$.

The composition of two strongly cartesian morphisms is strongly cartesian.

Any isomorphism of $\mathcal{S}$ is strongly cartesian.

Any strongly cartesian morphism $\varphi $ such that $p(\varphi )$ is an isomorphism, is an isomorphism.

**Proof.**
Proof of (1). Let $\varphi : y \to x$ and $\psi : z \to y$ be strongly cartesian. Let $t$ be an arbitrary object of $\mathcal{S}$. Then we have

\begin{align*} & \mathop{Mor}\nolimits _\mathcal {S}(t, z) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, y) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, x) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y)) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, x) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z)) \end{align*}

hence $z \to x$ is strongly cartesian.

Proof of (2). Let $y \to x$ be an isomorphism. Then $p(y) \to p(x)$ is an isomorphism too. Hence $\mathop{Mor}\nolimits _\mathcal {C}(p(z), p(y)) \to \mathop{Mor}\nolimits _\mathcal {C}(p(z), p(x))$ is a bijection. Hence $\mathop{Mor}\nolimits _\mathcal {S}(z, x) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(z), p(x))} \mathop{Mor}\nolimits _\mathcal {C}(p(z), p(y))$ is bijective to $\mathop{Mor}\nolimits _\mathcal {S}(z, x)$. Hence the displayed map of Definition 4.32.1 is a bijection as $y \to x$ is an isomorphism, and we conclude that $y \to x$ is strongly cartesian.

Proof of (3). Assume $\varphi : y \to x$ is strongly cartesian with $p(\varphi ) : p(y) \to p(x)$ an isomorphism. Applying the definition with $z = x$ shows that $(\text{id}_ x, p(\varphi )^{-1})$ comes from a unique morphism $\chi : x \to y$. We omit the verification that $\chi $ is the inverse of $\varphi $.
$\square$

Lemma 4.32.3. Let $F : \mathcal{A} \to \mathcal{B}$ and $G : \mathcal{B} \to \mathcal{C}$ be composable functors between categories. Let $x \to y$ be a morphism of $\mathcal{A}$. If $x \to y$ is strongly $\mathcal{B}$-cartesian and $F(x) \to F(y)$ is strongly $\mathcal{C}$-cartesian, then $x \to y$ is strongly $\mathcal{C}$-cartesian.

**Proof.**
This follows directly from the definition.
$\square$

Lemma 4.32.4. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a category over $\mathcal{C}$. Let $x \to y$ and $z \to y$ be morphisms of $\mathcal{S}$. Assume

$x \to y$ is strongly cartesian,

$p(x) \times _{p(y)} p(z)$ exists, and

there exists a strongly cartesian morphism $a : w \to z$ in $\mathcal{S}$ with $p(w) = p(x) \times _{p(y)} p(z)$ and $p(a) = \text{pr}_2 : p(x) \times _{p(y)} p(z) \to p(z)$.

Then the fibre product $x \times _ y z$ exists and is isomorphic to $w$.

**Proof.**
Since $x \to y$ is strongly cartesian there exists a unique morphism $b : w \to x$ such that $p(b) = \text{pr}_1$. To see that $w$ is the fibre product we compute

\begin{align*} & \mathop{Mor}\nolimits _\mathcal {S}(t, w) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(w)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z))} (\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x)) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z))) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {S}(t, y)} \mathop{Mor}\nolimits _\mathcal {S}(t, y) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {S}(t, y)} \mathop{Mor}\nolimits _\mathcal {S}(t, x) \end{align*}

as desired. The first equality holds because $a : w \to z$ is strongly cartesian and the last equality holds because $x \to y$ is strongly cartesian.
$\square$

Definition 4.32.5. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a category over $\mathcal{C}$. We say $\mathcal{S}$ is a *fibred category over $\mathcal{C}$* if given any $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$ lying over $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ and any morphism $f : V \to U$ of $\mathcal{C}$, there exists a strongly cartesian morphism $f^*x \to x$ lying over $f$.

Assume $p : \mathcal{S} \to \mathcal{C}$ is a fibred category. For every $f : V \to U$ and $x\in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U)$ as in the definition we may choose a strongly cartesian morphism $f^\ast x \to x$ lying over $f$. By the axiom of choice we may choose $f^*x \to x$ for all $f: V \to U = p(x)$ simultaneously. We claim that for every morphism $\phi : x \to x'$ in $\mathcal{S}_ U$ and $f : V \to U$ there is a unique morphism $f^\ast \phi : f^\ast x \to f^\ast x'$ in $\mathcal{S}_ V$ such that

\[ \xymatrix{ f^\ast x \ar[r]_{f^\ast \phi } \ar[d] & f^\ast x' \ar[d] \\ x \ar[r]^{\phi } & x' } \]

commutes. Namely, the arrow exists and is unique because $f^*x' \to x'$ is strongly cartesian. The uniqueness of this arrow guarantees that $f^\ast $ (now also defined on morphisms) is a functor $ f^\ast : \mathcal{S}_ U \to \mathcal{S}_ V$.

Definition 4.32.6. Assume $p : \mathcal{S} \to \mathcal{C}$ is a fibred category.

A *choice of pullbacks*^{1} for $p : \mathcal{S} \to \mathcal{C}$ is given by a choice of a strongly cartesian morphism $f^\ast x \to x$ lying over $f$ for any morphism $f: V \to U$ of $\mathcal{C}$ and any $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U)$.

Given a choice of pullbacks, for any morphism $f : V \to U$ of $\mathcal{C}$ the functor $f^* : \mathcal{S}_ U \to \mathcal{S}_ V$ described above is called a *pullback functor* (associated to the choices $f^*x \to x$ made above).

Of course we may always assume our choice of pullbacks has the property that $\text{id}_ U^*x = x$, although in practice this is a useless property without imposing further assumptions on the pullbacks.

Lemma 4.32.7. Assume $p : \mathcal{S} \to \mathcal{C}$ is a fibred category. Assume given a choice of pullbacks for $p : \mathcal{S} \to \mathcal{C}$.

For any pair of composable morphisms $f : V \to U$, $g : W \to V$ there is a unique isomorphism

\[ \alpha _{g, f} : (f \circ g)^\ast \longrightarrow g^\ast \circ f^\ast \]

as functors $\mathcal{S}_ U \to \mathcal{S}_ W$ such that for every $y\in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U)$ the following diagram commutes

\[ \xymatrix{ g^\ast f^\ast y \ar[r] & f^\ast y \ar[d] \\ (f \circ g)^\ast y \ar[r] \ar[u]^{(\alpha _{g, f})_ y} & y } \]

If $f = \text{id}_ U$, then there is a canonical isomorphism $\alpha _ U : \text{id} \to (\text{id}_ U)^*$ as functors $\mathcal{S}_ U \to \mathcal{S}_ U$.

The quadruple $(U \mapsto \mathcal{S}_ U, f \mapsto f^*, \alpha _{g, f}, \alpha _ U)$ defines a pseudo functor from $\mathcal{C}^{opp}$ to the $(2, 1)$-category of categories, see Definition 4.28.5.

**Proof.**
In fact, it is clear that the commutative diagram of part (1) uniquely determines the morphism $(\alpha _{g, f})_ y$ in the fibre category $\mathcal{S}_ W$. It is an isomorphism since both the morphism $(f \circ g)^*y \to y$ and the composition $g^*f^*y \to f^*y \to y$ are strongly cartesian morphisms lifting $f \circ g$ (see discussion following Definition 4.32.1 and Lemma 4.32.2). In the same way, since $\text{id}_ x : x \to x$ is clearly strongly cartesian over $\text{id}_ U$ (with $U = p(x)$) we see that there exists an isomorphism $(\alpha _ U)_ x : x \to (\text{id}_ U)^*x$. (Of course we could have assumed beforehand that $f^*x = x$ whenever $f$ is an identity morphism, but it is better for the sake of generality not to assume this.) We omit the verification that $\alpha _{g, f}$ and $\alpha _ U$ so obtained are transformations of functors. We also omit the verification of (3).
$\square$

Lemma 4.32.8. Let $\mathcal{C}$ be a category. Let $\mathcal{S}_1$, $\mathcal{S}_2$ be categories over $\mathcal{C}$. Suppose that $\mathcal{S}_1$ and $\mathcal{S}_2$ are equivalent as categories over $\mathcal{C}$. Then $\mathcal{S}_1$ is fibred over $\mathcal{C}$ if and only if $\mathcal{S}_2$ is fibred over $\mathcal{C}$.

**Proof.**
Denote $p_ i : \mathcal{S}_ i \to \mathcal{C}$ the given functors. Let $F : \mathcal{S}_1 \to \mathcal{S}_2$, $G : \mathcal{S}_2 \to \mathcal{S}_1$ be functors over $\mathcal{C}$, and let $i : F \circ G \to \text{id}_{\mathcal{S}_2}$, $j : G \circ F \to \text{id}_{\mathcal{S}_1}$ be isomorphisms of functors over $\mathcal{C}$. We claim that in this case $F$ maps strongly cartesian morphisms to strongly cartesian morphisms. Namely, suppose that $\varphi : y \to x$ is strongly cartesian in $\mathcal{S}_1$. Set $f : V \to U$ equal to $p_1(\varphi )$. Suppose that $z' \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_2)$, with $W = p_2(z')$, and we are given $g : W \to V$ and $\psi ' : z' \to F(x)$ such that $p_2(\psi ') = f \circ g$. Then

\[ \psi = j \circ G(\psi ') : G(z') \to G(F(x)) \to x \]

is a morphism in $\mathcal{S}_1$ with $p_1(\psi ) = f \circ g$. Hence by assumption there exists a unique morphism $\xi : G(z') \to y$ lying over $g$ such that $\psi = \varphi \circ \xi $. This in turn gives a morphism

\[ \xi ' = F(\xi ) \circ i^{-1} : z' \to F(G(z')) \to F(y) \]

lying over $g$ with $\psi ' = F(\varphi ) \circ \xi '$. We omit the verification that $\xi '$ is unique.
$\square$

The conclusion from Lemma 4.32.8 is that equivalences map strongly cartesian morphisms to strongly cartesian morphisms. But this may not be the case for an arbitrary functor between fibred categories over $\mathcal{C}$. Hence we define the $2$-category of fibred categories as follows.

Definition 4.32.9. Let $\mathcal{C}$ be a category. The *$2$-category of fibred categories over $\mathcal{C}$* is the sub $2$-category of the $2$-category of categories over $\mathcal{C}$ (see Definition 4.31.1) defined as follows:

Its objects will be fibred categories $p : \mathcal{S} \to \mathcal{C}$.

Its $1$-morphisms $(\mathcal{S}, p) \to (\mathcal{S}', p')$ will be functors $G : \mathcal{S} \to \mathcal{S}'$ such that $p' \circ G = p$ and such that $G$ maps strongly cartesian morphisms to strongly cartesian morphisms.

Its $2$-morphisms $t : G \to H$ for $G, H : (\mathcal{S}, p) \to (\mathcal{S}', p')$ will be morphisms of functors such that $p'(t_ x) = \text{id}_{p(x)}$ for all $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$.

In this situation we will denote

\[ \mathop{Mor}\nolimits _{\textit{Fib}/\mathcal{C}}(\mathcal{S}, \mathcal{S}') \]

the category of $1$-morphisms between $(\mathcal{S}, p)$ and $(\mathcal{S}', p')$

Note the condition on $1$-morphisms. Note also that this is a true $2$-category and not a $(2, 1)$-category. Hence when taking $2$-fibre products we first pass to the associated $(2, 1)$-category.

Lemma 4.32.10. Let $\mathcal{C}$ be a category. The $(2, 1)$-category of fibred categories over $\mathcal{C}$ has 2-fibre products, and they are described as in Lemma 4.31.3.

**Proof.**
Basically what one has to show here is that given $F : \mathcal{X} \to \mathcal{S}$ and $G : \mathcal{Y} \to \mathcal{S}$ morphisms of fibred categories over $\mathcal{C}$, then the category $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$ described in Lemma 4.31.3 is fibred. Let us show that $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$ has plenty of strongly cartesian morphisms. Namely, suppose we have $(U, x, y, \phi )$ an object of $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$. And suppose $f : V \to U$ is a morphism in $\mathcal{C}$. Choose strongly cartesian morphisms $a : f^*x \to x$ in $\mathcal{X}$ lying over $f$ and $b : f^*y \to y$ in $\mathcal{Y}$ lying over $f$. By assumption $F(a)$ and $G(b)$ are strongly cartesian. Since $\phi : F(x) \to G(y)$ is an isomorphism, by the uniqueness of strongly cartesian morphisms we find a unique isomorphism $f^*\phi : F(f^*x) \to G(f^*y)$ such that $G(b) \circ f^*\phi = \phi \circ F(a)$. In other words $(G(a), G(b)) : (V, f^*x, f^*y, f^*\phi ) \to (U, x, y, \phi )$ is a morphism in $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$. We omit the verification that this is a strongly cartesian morphism (and that these are in fact the only strongly cartesian morphisms).
$\square$

Lemma 4.32.11. Let $\mathcal{C}$ be a category. Let $U \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$. If $p : \mathcal{S} \to \mathcal{C}$ is a fibred category and $p$ factors through $p' : \mathcal{S} \to \mathcal{C}/U$ then $p' : \mathcal{S} \to \mathcal{C}/U$ is a fibred category.

**Proof.**
Suppose that $\varphi : x' \to x$ is strongly cartesian with respect to $p$. We claim that $\varphi $ is strongly cartesian with respect to $p'$ also. Set $g = p'(\varphi )$, so that $g : V'/U \to V/U$ for some morphisms $f : V \to U$ and $f' : V' \to U$. Let $z \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$. Set $p'(z) = (W \to U)$. To show that $\varphi $ is strongly cartesian for $p'$ we have to show

\[ \mathop{Mor}\nolimits _\mathcal {S}(z, x') \longrightarrow \mathop{Mor}\nolimits _\mathcal {S}(z, x) \times _{\mathop{Mor}\nolimits _{\mathcal{C}/U}(W/U, V/U)} \mathop{Mor}\nolimits _{\mathcal{C}/U}(W/U, V'/U), \]

given by $\psi ' \longmapsto (\varphi \circ \psi ', p'(\psi '))$ is bijective. Suppose given an element $(\psi , h)$ of the right hand side, then in particular $g \circ h = p(\psi )$, and by the condition that $\varphi $ is strongly cartesian we get a unique morphism $\psi ' : z \to x'$ with $\psi = \varphi \circ \psi '$ and $p(\psi ') = h$. OK, and now $p'(\psi ') : W/U \to V/U$ is a morphism whose corresponding map $W \to V$ is $h$, hence equal to $h$ as a morphism in $\mathcal{C}/U$. Thus $\psi '$ is a unique morphism $z \to x'$ which maps to the given pair $(\psi , h)$. This proves the claim.

Finally, suppose given $g : V'/U \to V/U$ and $x$ with $p'(x) = V/U$. Since $p : \mathcal{S} \to \mathcal{C}$ is a fibred category we see there exists a strongly cartesian morphism $\varphi : x' \to x$ with $p(\varphi ) = g$. By the same argument as above it follows that $p'(\varphi ) = g : V'/U \to V/U$. And as seen above the morphism $\varphi $ is strongly cartesian. Thus the conditions of Definition 4.32.5 are satisfied and we win.
$\square$

Lemma 4.32.12. Let $\mathcal{A} \to \mathcal{B} \to \mathcal{C}$ be functors between categories. If $\mathcal{A}$ is fibred over $\mathcal{B}$ and $\mathcal{B}$ is fibred over $\mathcal{C}$, then $\mathcal{A}$ is fibred over $\mathcal{C}$.

**Proof.**
This follows from the definitions and Lemma 4.32.3.
$\square$

Lemma 4.32.13. Let $p : \mathcal{S} \to \mathcal{C}$ be a fibred category. Let $x \to y$ and $z \to y$ be morphisms of $\mathcal{S}$ with $x \to y$ strongly cartesian. If $p(x) \times _{p(y)} p(z)$ exists, then $x \times _ y z$ exists, $p(x \times _ y z) = p(x) \times _{p(y)} p(z)$, and $x \times _ y z \to z$ is strongly cartesian.

**Proof.**
Pick a strongly cartesian morphism $\text{pr}_2^*z \to z$ lying over $\text{pr}_2 : p(x) \times _{p(y)} p(z) \to p(z)$. Then $\text{pr}_2^*z = x \times _ y z$ by Lemma 4.32.4.
$\square$

Lemma 4.32.14. Let $\mathcal{C}$ be a category. Let $F : \mathcal{X} \to \mathcal{Y}$ be a $1$-morphism of fibred categories over $\mathcal{C}$. There exist $1$-morphisms of fibred categories over $\mathcal{C}$

\[ \xymatrix{ \mathcal{X} \ar@<1ex>[r]^ u & \mathcal{X}' \ar[r]^ v \ar@<1ex>[l]^ w & \mathcal{Y} } \]

such that $F = v \circ u$ and such that

$u : \mathcal{X} \to \mathcal{X}'$ is fully faithful,

$w$ is left adjoint to $u$, and

$v : \mathcal{X}' \to \mathcal{Y}$ is a fibred category.

**Proof.**
Denote $p : \mathcal{X} \to \mathcal{C}$ and $q : \mathcal{Y} \to \mathcal{C}$ the structure functors. We construct $\mathcal{X}'$ explicitly as follows. An object of $\mathcal{X}'$ is a quadruple $(U, x, y, f)$ where $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{X}_ U)$, $y \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{Y}_ U)$ and $f : y \to F(x)$ is a morphism in $\mathcal{Y}_ U$. A morphism $(a, b) : (U, x, y, f) \to (U', x', y', f')$ is given by $a : x \to x'$ and $b : y \to y'$ with $p(a) = q(b) : U \to U'$ and such that $f' \circ b = F(a) \circ f$.

Let us make a choice of pullbacks for both $p$ and $q$ and let us use the same notation to indicate them. Let $(U, x, y, f)$ be an object and let $h : V \to U$ be a morphism. Consider the morphism $c : (V, h^*x, h^*y, h^*f) \to (U, x, y, f)$ coming from the given strongly cartesian maps $h^*x \to x$ and $h^*y \to y$. We claim $c$ is strongly cartesian in $\mathcal{X}'$ over $\mathcal{C}$. Namely, suppose we are given an object $(W, x', y', f')$ of $\mathcal{X}'$, a morphism $(a, b) : (W, x', y', f') \to (U, x, y, f)$ lying over $W \to U$, and a factorization $W \to V \to U$ of $W \to U$ through $h$. As $h^*x \to x$ and $h^*y \to y$ are strongly cartesian we obtain morphisms $a' : x' \to h^*x$ and $b' : y' \to h^*y$ lying over the given morphism $W \to V$. Consider the diagram

\[ \xymatrix{ y' \ar[d]_{f'} \ar[r] & h^*y \ar[r] \ar[d]_{h^*f} & y \ar[d]_ f \\ F(x') \ar[r] & F(h^*x) \ar[r] & F(x) } \]

The outer rectangle and the right square commute. Since $F$ is a $1$-morphism of fibred categories the morphism $F(h^*x) \to F(x)$ is strongly cartesian. Hence the left square commutes by the universal property of strongly cartesian morphisms. This proves that $\mathcal{X}'$ is fibred over $\mathcal{C}$.

The functor $u : \mathcal{X} \to \mathcal{X}'$ is given by $x \mapsto (p(x), x, F(x), \text{id})$. This is fully faithful. The functor $\mathcal{X}' \to \mathcal{Y}$ is given by $(U, x, y, f) \mapsto y$. The functor $w : \mathcal{X}' \to \mathcal{X}$ is given by $(U, x, y, f) \mapsto x$. Each of these functors is a $1$-morphism of fibred categories over $\mathcal{C}$ by our description of strongly cartesian morphisms of $\mathcal{X}'$ over $\mathcal{C}$. Adjointness of $w$ and $u$ means that

\[ \mathop{Mor}\nolimits _\mathcal {X}(x, x') = \mathop{Mor}\nolimits _{\mathcal{X}'}((U, x, y, f), (p(x'), x', F(x'), \text{id})), \]

which follows immediately from the definitions.

Finally, we have to show that $\mathcal{X}' \to \mathcal{Y}$ is a fibred category. Let $c : y' \to y$ be a morphism in $\mathcal{Y}$ and let $(U, x, y, f)$ be an object of $\mathcal{X}'$ lying over $y$. Set $V = q(y')$ and let $h = q(c) : V \to U$. Let $a : h^*x \to x$ and $b : h^*y \to y$ be the strongly cartesian morphisms covering $h$. Since $F$ is a $1$-morphism of fibred categories we may identify $h^*F(x) = F(h^*x)$ with strongly cartesian morphism $F(a) : F(h^*x) \to F(x)$. By the universal property of $b : h^*y \to y$ there is a morphism $c' : y' \to h^*y$ in $\mathcal{Y}_ V$ such that $c = b \circ c'$. We claim that

\[ (a, c) : (V, h^*x, y', h^*f \circ c') \longrightarrow (U, x, y, f) \]

is strongly cartesian in $\mathcal{X}'$ over $\mathcal{Y}$. To see this let $(W, x_1, y_1, f_1)$ be an object of $\mathcal{X}'$, let $(a_1, b_1) : (W, x_1, y_1, f_1) \to (U, x, y, f)$ be a morphism and let $b_1 = c \circ b_1'$ for some morphism $b_1' : y_1 \to y'$. Then

\[ (a_1', b_1') : (W, x_1, y_1, f_1) \longrightarrow (V, h^*x, y', h^*f \circ c') \]

(where $a_1' : x_1 \to h^*x$ is the unique morphism lying over the given morphism $q(b_1') : W \to V$ such that $a_1 = a \circ a_1'$) is the desired morphism.
$\square$

## Comments (0)