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, namely one where each fiber is a set.
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.
Under this equivalence, the representable presheaf on an object $X$ corresponds to the canonical functor $B/X \to B$ from the slice category over $X$.
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$.
Last revised on September 22, 2022 at 16:05:25. See the history of this page for a list of all contributions to it.