2.6.1. Characterization of cartesian maps [000T]

There is a simple characterization of cartesian maps in $\OpCat{E}$.

[0020] Lemma 2.6.1·a.

A morphism $\bar{f}:\bar{x}\to\Sub{f} \bar{y}\in\OpCat{E}$ is cartesian over $f:x\to y$ if and only if the vertical leg of $f$ is an isomorphism.

Proof. Suppose that $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$ is represented by a span $\brc{\bar{x}\leftarrow\bar{y}\Sub{x}\to\bar{y}}$ in $E$ in which the vertical leg $\bar{x}\leftarrow\bar{y}\Sub{x}$ is an isomorphism. We must show that $\bar{x}\to_f\bar{y}$ is cartesian in $\OpCat{E}$. We fix a morphism $\bar{h}:\bar{w}\to\Sub{m;f}\bar{y}\in \OpCat{E}$ where $m:w\to x$, depicted below in terms of $\OpCat{E}$:

We must define the unique intervening map $\bar{w}\to_m \bar{x}$ in $\OpCat{E}$. We first translate the above into the language of $E$ by unfolding definitions:

The desired intervening map $\bar{w}\to\Sub{m} \bar{x}\in \OpCat{E}$ shakes out in the language of $E$ to be a span $\brc{\bar{w}\leftarrow \bar{x}\Sub{w}\to\Sub{m} \bar{x}}$ in which the left-hand leg is vertical and the right-hand leg is cartesian over $m:w\to x$. But the left-hand span $\brc{\bar{w}\leftarrow\bar{y}\Sub{w}\to \bar{y}\Sub{x}\cong \bar{x}}$ in the diagram above is exactly what we need.

We leave the converse to the reader.