# mathlib3documentation

category_theory.grothendieck

# The Grothendieck construction #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a functor F : C ⥤ Cat, the objects of grothendieck F consist of dependent pairs (b, f), where b : C and f : F.obj c, and a morphism (b, f) ⟶ (b', f') is a pair β : b ⟶ b' in C, and φ : (F.map β).obj f ⟶ f'

Categories such as PresheafedSpace are in fact examples of this construction, and it may be interesting to try to generalize some of the development there.

## Implementation notes #

Really we should treat Cat as a 2-category, and allow F to be a 2-functor.

There is also a closely related construction starting with G : Cᵒᵖ ⥤ Cat, where morphisms consists again of β : b ⟶ b' and φ : f ⟶ (F.map (op β)).obj f'.

## References #

See also category_theory.functor.elements for the category of elements of functor F : C ⥤ Type.

@[nolint]
structure category_theory.grothendieck {C : Type u_1} (F : C category_theory.Cat) :
Type (max u_1 u_6)

The Grothendieck construction (often written as ∫ F in mathematics) for a functor F : C ⥤ Cat gives a category whose

• objects X consist of X.base : C and X.fiber : F.obj base
• morphisms f : X ⟶ Y consist of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber
Instances for category_theory.grothendieck
structure category_theory.grothendieck.hom {C : Type u_1} {F : C category_theory.Cat} (X Y : category_theory.grothendieck F) :
Type (max u_3 u_5)

A morphism in the Grothendieck category F : C ⥤ Cat consists of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber.

Instances for category_theory.grothendieck.hom
@[ext]
theorem category_theory.grothendieck.ext {C : Type u_1} {F : C category_theory.Cat} {X Y : category_theory.grothendieck F} (f g : X.hom Y) (w_base : f.base = g.base) (w_fiber : = g.fiber) :
f = g

The identity morphism in the Grothendieck category.

Equations
@[protected, instance]
Equations
def category_theory.grothendieck.comp {C : Type u_1} {F : C category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

Composition of morphisms in the Grothendieck category.

Equations
@[simp]
theorem category_theory.grothendieck.comp_base {C : Type u_1} {F : C category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :
= f.base g.base
@[simp]
theorem category_theory.grothendieck.comp_fiber {C : Type u_1} {F : C category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :
= (F.map g.base).map f.fiber g.fiber
@[protected, instance]
Equations
theorem category_theory.grothendieck.congr {C : Type u_1} {F : C category_theory.Cat} {X Y : category_theory.grothendieck F} {f g : X Y} (h : f = g) :

The forgetful functor from grothendieck F to the source category.

Equations

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations
@[simp]

The Grothendieck construction applied to a functor to Type (thought of as a functor to Cat by realising a type as a discrete category) is the same as the 'category of elements' construction.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.grothendieck.grothendieck_Type_to_Cat_counit_iso {C : Type u_1} (G : C Type w) :
= category_theory.nat_iso.of_components (λ (X : G.elements), sigma.cases_on X (λ (X_fst : C) (X_snd : G.obj X_fst), _
@[simp]
theorem category_theory.grothendieck.grothendieck_Type_to_Cat_unit_iso {C : Type u_1} (G : C Type w) :
= category_theory.nat_iso.of_components (λ (X : , X.cases_on (λ (X_base : C) (X_fiber : X_base)), category_theory.discrete.cases_on X_fiber (λ (X_fiber : G.obj X_base), category_theory.iso.refl {base := X_base, fiber := {as := X_fiber}})))) _