The Stacks project

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

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{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(y)) \to \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(x))$ is a bijection. Hence $\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(z, x) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(x))} \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(y))$ is bijective to $\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(z, x)$. Hence the displayed map of Definition 4.33.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$

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

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

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$

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.33.1 and Lemma 4.33.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$

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

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

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

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.32.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 $(a, 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$

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

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.33.5 are satisfied and we win. $\square$

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

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.33.4. $\square$

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

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

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

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

(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$