nLab
discrete fibration

Discrete fibrations

Definition

A functor F:CBF: C \to B is a discrete fibration if for every object cc in CC, and every morphism of the form g:bF(c)g : b\to F(c) in BB there is a unique morphism h:dch : d\to c in CC such that F(h)=gF(h) = g.

A functor F:CBF: C \to B is a discrete opfibration if F op:C opB opF^{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 EE, internal categories C,BC,B in EE, an internal functor F:CBF: C \to B is a discrete fibration of internal categories if the square

C 1 F 1 B 1 d 0 d 0 C 0 F 0 B 0\begin{matrix} C_1 &\stackrel{F_1}\to& B_1\\ d_0\downarrow && \downarrow d_0\\ C_0 &\stackrel{F_0}\to& B_0 \end{matrix}

is cartesian.

Discussion via category of elements

Given a discrete fibration F:CBF: C \to B, define a functor F *:B opSetF^*: B^{op} \to Set as follows:

  • For xx an object of BB, let F *(x)F^*(x) be the set of objects yy of CC such that F(y)=xF(y) = x.
  • For g:xyg: x \to y a morphism of BB, let F *(g):F *(y)F *(x)F^*(g): F^*(y) \to F^*(x) be the function that maps each element of F *(y)F^*(y) to the unique morphism hh determined by the definition of discrete fibration above.

There is a size issue here, is F *(x)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 opSetF^*: B^{op} \to Set, define a category CC and a discrete fibration F:CBF: C \to B as follows:

  • Let CC be the category of elements of the functor FF; that is:
    • an object of CC is a pair consisting of an object xx of BB and an element of F *(x)F^*(x),
    • a morphism from (x,a)(x,a) to (y,b)(y,b) in CC is a morphism g:xyg: x \to y in BB such that F *(g)F^*(g) assigns aa to bb.
  • The functor from CC to BB is the obvious forgetful functor.

If you start from F *F^*, construct CC and FF, and then construct a new F *F^*, it will be equal to the original F *F^*. Conversely, if you start with CC and FF, construct F *F^*, and then construct a new CC' and FF', then there will be an isomorphism of categories between CC and CC', relative to which FF and FF' 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 F *F^* from FF 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 EE be a cartesian category. A span of internal categories ApCqBA\stackrel{p}\leftarrow C\stackrel{q}\to B in Cat(E)Cat(E) is called a discrete fibration from AA to BB if in the diagram

A 0 C l i l A p C i r C r q B B 0\begin{matrix} A_0 & \leftarrow & C_l && \\ \downarrow &&\downarrow i_l &&\\ A &\stackrel{p}\leftarrow & C &\stackrel{i_r}\leftarrow & C_r\\ &&q \downarrow && \downarrow \\ && B &\leftarrow & B_0 \end{matrix}

in which the two squares are the cartesian satisfies the following 3 properties:

  • pi r:C 1Ap\circ i_r : C_1\to A is a discrete fibration

  • qi l:C lBq\circ i_l: C_l\to B is a discrete opfibration

  • Let XX be defined as the pullback

    X (C r) 1 (C l) 1 C 0\begin{matrix} X & \to & (C_r)_1 \\ \downarrow &&\downarrow \\ (C_l)_1 &\to & C_0 \end{matrix}

    and j:XC 1× C 0C 1j:X\hookrightarrow C_1\times_{C_0} C_1 the canonical inclusion. Then the morphism cj:XC 1c\circ j : X\to C_1, where c:C 1× C 0C 1C 1c: C_1\times_{C_0} C_1\to C_1 is the composition morphism of internal category CC, is invertible.

Example. Given internal functors a:ADa : A\to D and b:BDb : B\to D in EE, the obvious span AabBA\leftarrow a\downarrow b\rightarrow B is a discrete fibration from AA to BB.

Revised on April 27, 2013 00:55:16 by David Carchedi (88.153.46.18)