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)