The Grothendieck construction (named after Alexander Grothendieck) is a construction used in the mathematical field of category theory.
It is a fundamental construction in the theory of descent, in the theory of stacks, and in fibred category theory.
In categorical logic, the construction is used to model the relationship between a type theory and a logic over that type theory, and allows for the translation of concepts from indexed category theory into fibred category theory, such as Lawvere's concept of hyperdoctrine.
The Grothendieck construction was first studied for the special case presheaves of sets by Mac Lane, where it was called the category of elements.
is a family of sets indexed by another set, one can form the disjoint union or coproduct
, which is the set of all ordered pairs
The disjoint union set is naturally equipped with a "projection" map
it is possible to reconstruct the original family of sets
up to a canonical bijection, as for each
of the singleton set
is called the "fiber" of
equipped with a choice of function
In this way, the disjoint union construction provides a way of viewing any family of sets indexed by
as a set "fibered" over
, and conversely, for any set
, we can view it as the disjoint union of the fibers of
Jacobs has referred to these two perspectives as "display indexing" and "pointwise indexing".
[2] The Grothendieck construction generalizes this to categories.
, family of categories
indexed by the objects of
in a functorial way, the Grothendieck construction returns a new category
), with Composition of morphisms is defined by
is a group, then it can be viewed as a category,
with one object and all morphisms invertible.
be a functor whose value at the sole object of
a category representing the group
be a functor is then equivalent to specifying a group homomorphism
denotes the group of automorphisms of
Finally, the Grothendieck construction,
results in a category with one object, which can again be viewed as a group, and in this case, the resulting group is (isomorphic to) the semidirect product