2.6. Opposite categories [000Q]

We adapt Bénabou’s construction as reported by Streicher (Fibred Categories à La Jean Bénabou, 2018).

[001Z] Construction 2.6·a.

Let $E$ be fibered over $B$; we may define the opposite fibered category $\OpCat{E}$ over $B$ like so:

  1. An object of $\OpCat{E}\Sub{x}$ is given by an object of $E\Sub{x}$.

  2. Given $f : x \to y\in B$, a morphism $\bar{x}\to_f \bar{y}$ in $\OpCat{E}$ is given in terms of $E$ by a cartesian map $\bar{y}\Sub{f} : \bar{y}\Sub{x} \to\Sub{f} \bar{y}$ together with a vertical map $h : \bar{y}\Sub{x}\to\Sub{\Idn{x}} \bar{y}$ as depicted below: such that $\brc{\bar{x} \leftarrow \bar{y}\Sub{x}\Sup{1}\to \bar{y}}$ is identified with $\brc{\bar{x}\leftarrow\bar{y}\Sub{x}\Sup{2}\to \bar{y}}$ when they agree up to the unique vertical isomorphism $\bar{y}\Sub{x}\Sup{1}\cong\bar{y}\Sub{x}\Sup{2}$ induced by the universal property of cartesian maps in the sense that the following diagram commutes:

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.

2.6.2. Cartesian lifts in the opposite category [000U]

The foregoing characterization of cartesian maps in $\OpCat{E}$ immediately implies that $\OpCat{E}$ is fibered over $B$.

[0021] Corollary 2.6.2·a.

The displayed category $\OpCat{E}$ is a cartesian fibration.

Proof. Fixing $\bar{y}\in \OpCat{E}\Sub{y}$ and $f:x\to y\in B$, we must exhibit a cartesian lift $\bar{f} : \bar{x}\to\Sub{f}\bar{y}\in \OpCat{E}$. By the characterization [000T] it suffices to find any map over $f$ whose vertical component is an isomorphism. Writing $\bar{y}\Sub{x}\to\Sub{f}\bar{y}$ for the cartesian lift of $f$ in $E$, consider the map in $\OpCat{E}$ presented by the following span in $E$:

2.6.3. Exegesis of opposite categories [000S]

The construction of fibered opposite categories (Construction 2.6·a [001Z]) does appear quite involved, but it can be seen to be inevitable from the perspective of the fiber categories $\OpCat{E}\Sub{x}$ (Section 2.5 [0005]). Indeed, let $u,v\in \OpCat{E}\Sub{x}$ and fix a vertical map $h : u \to v\in \OpCat{E}\Sub{x}$; by unfolding definitions, we see that the vertical map $h : u \to v$ is uniquely determined by a morphism $v\to u\in E\Sub{x}$.

Proof. A displayed morphism $u\to\Sub{\Idn{x}} v\in \OpCat{E}$ is determined by a span $\brc{u\leftarrow v\Sub{x} \to v}\in E$ where the right-hand map is cartesian over $\Idn{x} : x\to x$ and the left-hand map is vertical, taken up to the identification of different cartesian lifts $v\Sub{x}\to x$. A displayed morphism that is cartesian over the identity is an isomorphism; hence, displayed morphisms $u\to\Sub{\Idn{x}} v\in\OpCat{E}$ are equivalently determined by vertical maps $v\to u \in E$.