A functor is a discrete fibration if for every object in , and every morphism of the form in there is a unique morphism in such that .
A functor is a discrete opfibration if is a discrete fibration.
A discrete fibration is a special case of a Grothendieck fibration.
Given a cartesian category , internal categories in , an internal functor is a discrete fibration of internal categories if the square
Discussion via category of elements
Given a discrete fibration , define a functor as follows:
- For an object of , let be the set of objects of such that .
- For a morphism of , let be the function that maps each element of to the unique morphism determined by the definition of discrete fibration above.
There is a size issue here, is 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 , define a category and a discrete fibration as follows:
- Let be the category of elements of the functor ; that is:
- an object of is a pair consisting of an object of and an element of ,
- a morphism from to in is a morphism in such that assigns to .
- The functor from to is the obvious forgetful functor.
If you start from , construct and , and then construct a new , it will be equal to the original . Conversely, if you start with and , construct , and then construct a new and , then there will be an isomorphism of categories between and , relative to which and are equal.
Invariance under equivalence
Note that the definition of fibration refers to equality of morphisms without previously assuming that the sources match, while the construction of from 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.
Generalization for spans internal to a category
Let be a cartesian category. A span of internal categories in is called a discrete fibration from to if in the diagram
in which the two squares are the cartesian satisfies the following 3 properties:
is a discrete fibration
is a discrete opfibration
Let be defined as the pullback
and the canonical inclusion. Then the morphism , where is the composition morphism of internal category , is invertible.
Example. Given internal functors and in , the obvious span is a discrete fibration from to .