Grothendieck Fibrations

A Grothendieck fibration over a base previewcategory $ℬ︀$ is 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.

The notion of a “pullback square” is replaced with that of cartesian morphism, which is the “universal” pull back of an object along a morphism.

Fibrations are widely used in categorical semantics of dependent type theory.

Definition

Preliminary definitions

In this section, we have two categories $ℬ︀$ and $ℰ︀$ , and a functor $𝑝 : ℰ︀ \to ℬ︀$ .

Definition Refinement Let $𝑅 : ℰ︀$ and $𝑋 : ℬ︀$ . We say that $𝑅$ refines $𝑋$ , or $𝑅 ⊏ 𝑋$ , if

𝑋 = 𝑝 (𝑅)

we say that the following diagram commutes

when $𝑝 (𝛼) = 𝑓$ .

Definition Cartesian morphism Let

𝑅, 𝑆 : ℰ︀

. A morphism

𝛼 : 𝑆 \to 𝑅

is said to be cartesian if, for any

𝑆^{'} : ℰ︀

𝛼^{'} : 𝑆^{'} \to 𝑅

and

𝑓 : 𝑝 (𝑆^{'}) \to 𝑝 (𝑆)

such that the following diagram commutes there exists a unique

\hat{𝑓} : 𝑆^{'} \to 𝑆

such that

𝑓 = 𝑝 (\hat{𝑓})

, and such that the following diagram commutes

A (Grothendieck) fibration states that, for every “pullback situtation”, there exists a cartesian morphism that “pulls back”.

Definition Fibration

𝑝

is said to be a fibration if, for any there exists a cartesian morphism

𝛼

making the following diagram commute

Fibrations over a given category can be organized into a category.

Definition Category of fibrations For a base category $ℬ︀$ , define Fibℬ︀ as the category of fibrations over $ℬ︀$ , that is, whose objects are pairs $(ℰ︀, 𝑝)$ with $ℰ︀$ a category and $𝑝 : ℰ︀ \to ℬ︀$ a fibration.

Given two fibrations $𝑝_{𝑖} : {ℰ︀}_{𝑖} \to ℬ︀$ ( $𝑖 = 1, 2$ ) over $ℬ︀$ , a morphism of fibrations from $𝑝_{1}$ to $𝑝_{2}$ is a functor $𝐹 : {ℰ︀}_{1} \to {ℰ︀}_{2}$ making the following diagram commute and which preserves cartesian morphisms.