Grothendieck Construction

Definition

Let $\mathcal{C}$ be a category and $P:\mathcal{C}\to \mathbf{Set}$ be a functor. The Grothendieck construction (also known as the category of elements) of $P$, denoted $\int P$ or ${\int }_{\mathcal{C}}P$, is the category defined by:

1. Objects: Pairs $(c,x)$ where $c$ is an object of $\mathcal{C}$ and $x\in P(c)$.
2. Morphisms: A morphism from $(c,x)$ to $(c^{\prime },x^{\prime })$ is a morphism $f:c\to c^{\prime }$ in $\mathcal{C}$ such that $P(f)(x)=x^{\prime }$.
3. Composition: Inherited directly from $\mathcal{C}$.

There is a canonical projection functor $\pi :\int P\to \mathcal{C}$ defined by $\pi (c,x)=c$ and $\pi (f)=f$.

Properties

Fibration

The projection $\pi$ is a discrete opfibration.

• The fibers ${\pi }^{-1}(c)$ correspond to the sets $P(c)$.
• For any object $(c,x)$ and morphism $u:c\to c^{\prime }$ in $\mathcal{C}$, there is a unique morphism in $\int P$ extending $(c,x)$ over $u$, given by the map to $(c^{\prime },P(u)(x))$.

Type Theoretic Analogue

This construction provides the categorical semantics for dependent sum types.

• Base category $\mathcal{C}$ corresponds to a context or type $A$.
• Functor $P:\mathcal{C}\to \mathbf{Set}$ corresponds to a type family $B:A\to \mathcal{U}$.
• Total category $\int P$ corresponds to the $\Sigma$-type ${\Sigma }_{a:A}B(a)$.

Sources

• https://ncatlab.org/nlab/show/Grothendieck+construction
• maclane1978-categories
• riehl2016-category-theory