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 non-evil thing on this page 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$.
Last revised on July 21, 2020 at 11:08:06. See the history of this page for a list of all contributions to it.