Lemma 4.33.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{\mathrm{Mor}}\nolimits _\mathcal {S}(t, w) \\ & = \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, z) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(z))} \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(w)) \\ & = \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, z) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(z))} (\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(x)) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(z))) \\ & = \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, z) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(x)) \\ & = \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, z) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, y)} \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, y) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(t), p(x)) \\ & = \mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, z) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(t, y)} \mathop{\mathrm{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$
Comments (0)