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

1. The composition of two strongly cartesian morphisms is strongly cartesian.

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

3. 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$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).