2.6. Opposite categories [000Q]
We adapt Bénabou’s construction as reported by Streicher (Fibred Categories à La Jean Bénabou, 2018).
Let $E$ be fibered over $B$; we may define the opposite fibered category $\OpCat{E}$ over $B$ like so:
-
An object of $\OpCat{E}\Sub{x}$ is given by an object of $E\Sub{x}$.
-
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}$.
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$.
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$. ∎
Bibliography
-
Streicher, T. (2018). Fibred Categories à la Jean Bénabou. arXiv:1801.02927.Details