Cartesian morphism

Consider a displayed category $𝖣 ⇥ 𝖢$ . Given $𝑓 : 𝑥 \to 𝑦$ in $𝖢$ , we say $𝑓' : 𝑥' \to 𝑓 𝑦'$ in $𝖣$ is cartesian over $𝑓$ , iff for any $𝑚 : 𝑢 \to 𝑥$ and $ℎ' : 𝑢' \to 𝑓 𝑚 𝑦'$ there is a unique factorization $―― 𝑚 : 𝑢' \to 𝑚 𝑥'$ so that $𝑓' ―― 𝑚 = ℎ'$ .¹ #m/def/cat/dis

By analogy to a pullback square, we denote that a given $𝑓'$ is cartesian as shown above.²

Properties

Let $𝑓' : 𝑥' \to 𝑓 𝑦'$ and $𝑔' : 𝑦' \to 𝑔 𝑧'$ be displayed morphisms with $𝑔'$ cartesian. Then $𝑓'$ is cartesian iff $𝑔' 𝑓'$ is cartesian.

Proof of 1

First suppose both $𝑓' : 𝑥' \to 𝑓 𝑦'$ and $𝑔' : 𝑦' \to 𝑔 𝑧'$ are cartesian. Let $𝑚 : 𝑢 \to 𝑥$ and $ℎ' : 𝑢' \to 𝑔 𝑓 𝑚 𝑧'$ . Since $𝑔'$ is cartesian, there is a unique $――― 𝑓 𝑚 : 𝑢' \to 𝑓 𝑚 𝑦'$ such that $𝑔' ――― 𝑓 𝑚 = ℎ'$ . Since $𝑓'$ is cartesian, there is a unique $―― 𝑚 : 𝑢' \to 𝑚 𝑥'$ such that $𝑓' ―― 𝑚 = ――― 𝑓 𝑚$ ; Thus $―― 𝑚$ is the unique solution to $𝑔' 𝑓' ―― 𝑚 = ℎ'$ . Thus $𝑔' 𝑓'$ is cartesian.

For the converse, suppose both $𝑔' : 𝑦' \to 𝑓 𝑧'$ and $𝑔' 𝑓' : 𝑥' \to 𝑓 𝑔 𝑧'$ are cartesian. Let $𝑚 : 𝑢 \to 𝑥$ and $ℎ' : 𝑢' \to 𝑓 𝑚 𝑦'$ . Since $𝑔' 𝑓'$ is cartesian, there is a unique $―― 𝑚$ such that $𝑔' 𝑓' ―― 𝑚 = 𝑔' ℎ'$ . Since $𝑔'$ is cartesian, there is a unique $――― 𝑓 𝑚$ such that $𝑔' ――― 𝑓 𝑚 = 𝑔' ℎ'$ . Thus we conclude $――― 𝑓 𝑚 = 𝑓' ―― 𝑚$ . Thus $―― 𝑚$ is the unique solution to $𝑓' ―― 𝑚 = ℎ'$ , proving ^P1.

Cartesian morphism

Properties

See also

Footnotes