Grothendieck fibrations
1. Introduction
A Grothendieck fibration over a base category a generalization of the structure of pullback over . Rather than pulling back a morphism along a morphism, one can pull back any object in the total category along a morphism in , assuming the “codomain” of that object is the same as that of the morphism.
2. Definition
Preliminary definitions
In this section, we have two categories and , and a functor .
Definition 1 (Refinement). Let and . We say that refines , or , if
we say that the following diagram commutes
if .
Definition 2 (Cartesian morphism). Let . A morphism is cartesian if, for any , , and such that the following diagram commutes There exists a unique such that , and such that the following diagram commutes
Definition 3 (Fibration). is said to be a fibration if, for any there exists a cartesion morphism making the following commute
Definition 4 (Category of fibrations). For a base category , define as the category of fibrations over , that is, whose objects are pairs with a category and a fibration. Given two fibrations over for , a morphism of fibrations between and is a functor making the following diagram commute and which preserves cartesianity of morphisms.
Definition 5 (Category of pseudofunctors). For a given base category , define as the category whose elements are contravariant pseudo-functors in , that is, for each object , a natural isomorphism called the pseudo unit of at ; for each morphisms and in , a natural isomorphism called the pseudo composition law of at and . We additionally require the following coherence conditions: for , the following diagram commutes Furthermore, for , and , the following diagram commutes Given two pseudofunctors and , a morphism is a pseudonatural transformation between and , that is, for each point , a functor and, for each morphism in , a natural isomorphism satisfying the following coherence conditions:
for , the following pasting is
that is,
if and are two morphisms in , is obtained by pasting the squares (plus pseudo-composition)
that is,
Main theorem
We aim at proving the
Theorem 6 (Main theorem). For a given base category , we have