A functor $F: C \to B$ is a discrete fibration if for every object $c$ in $C$, and every morphism of the form $g : b\to F(c)$ in $B$ there is a unique morphism $h : d\to c$ in $C$ such that $F(h) = g$.
A functor $F: C \to B$ is a discrete opfibration if $F^{op}:C^{op}\to B^{op}$ is a discrete fibration.
A discrete fibration is a special case of a Grothendieck fibration.
Given a cartesian category $E$, internal categories $C,B$ in $E$, an internal functor $F: C \to B$ is a discrete fibration of internal categories if the square
is cartesian.
Given a discrete fibration $F: C \to B$, define a functor $F^*: B^{op} \to Set$ as follows:
There is a size issue here, is $F^*(x)$ in fact small? We say that the fibration has small fibres if so; else we must pass to a larger universe when we define Set.
Conversely, give a functor $F^*: B^{op} \to Set$, define a category $C$ and a discrete fibration $F: C \to B$ as follows:
If you start from $F^*$, construct $C$ and $F$, and then construct a new $F^*$, it will be equal to the original $F^*$. Conversely, if you start with $C$ and $F$, construct $F^*$, and then construct a new $C'$ and $F'$, then there will be an isomorphism of categories between $C$ and $C'$, relative to which $F$ and $F'$ are equal.
Note that the definition of fibration refers to equality of morphisms without previously assuming that the sources match, while the construction of $F^*$ from $F$ refers to equality of objects. This is also why we get equality of functors and isomorphism of categories in the immediately preceding paragraph. So the only thing on this page which respects the principle of equivalence is the idea of a functor to Set. That is the fundamental invariant notion; a discrete fibration is just a convenient way of talking about it.
(…)
Let $E$ be a cartesian category. A span of internal categories $A\stackrel{p}\leftarrow C\stackrel{q}\to B$ in $Cat(E)$ is called a discrete fibration from $A$ to $B$ if in the diagram
in which the two squares are the cartesian satisfies the following 3 properties:
$p\circ i_r : C_1\to A$ is a discrete fibration
$q\circ i_l: C_l\to B$ is a discrete opfibration
Let $X$ be defined as the pullback
and $j:X\hookrightarrow C_1\times_{C_0} C_1$ the canonical inclusion. Then the morphism $c\circ j : X\to C_1$, where $c: C_1\times_{C_0} C_1\to C_1$ is the composition morphism of internal category $C$, is invertible.
Example. Given internal functors $a : A\to D$ and $b : B\to D$ in $E$, the obvious span $A\leftarrow a\downarrow b\rightarrow B$ is a discrete fibration from $A$ to $B$.
Emily Riehl and Fosco Loregian, Categorical notions of fibration. arXiv:1806.06129
Last revised on October 4, 2021 at 09:22:05. See the history of this page for a list of all contributions to it.