The Grothendieck construction #
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
.
The Grothendieck construction (often written as ∫ F
in mathematics) for a functor F : C ⥤ Cat
gives a category whose
- objects
X
consist ofX.base : C
andX.fiber : F.obj base
- morphisms
f : X ⟶ Y
consist ofbase : X.base ⟶ Y.base
andf.fiber : (F.map base).obj X.fiber ⟶ Y.fiber
Instances for category_theory.grothendieck
- category_theory.grothendieck.has_sizeof_inst
- category_theory.grothendieck.category_theory.category
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
- category_theory.grothendieck.hom.has_sizeof_inst
- category_theory.grothendieck.hom.inhabited
The identity morphism in the Grothendieck category.
Equations
Composition of morphisms in the Grothendieck category.
Equations
- category_theory.grothendieck.category_theory.category = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.grothendieck F), X.hom Y}, id := λ (X : category_theory.grothendieck F), X.id, comp := λ (X Y Z : category_theory.grothendieck F) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.grothendieck.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
The forgetful functor from grothendieck F
to the source category.
Equations
- category_theory.grothendieck.forget F = {obj := λ (X : category_theory.grothendieck F), X.base, map := λ (X Y : category_theory.grothendieck F) (f : X ⟶ Y), f.base, map_id' := _, map_comp' := _}
Auxiliary definition for grothendieck_Type_to_Cat
, to speed up elaboration.
Equations
- category_theory.grothendieck.grothendieck_Type_to_Cat_functor G = {obj := λ (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)), ⟨X.base, X.fiber.as⟩, map := λ (X Y : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)) (f : X ⟶ Y), ⟨f.base, _⟩, map_id' := _, map_comp' := _}
Auxiliary definition for grothendieck_Type_to_Cat
, to speed up elaboration.
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
- category_theory.grothendieck.grothendieck_Type_to_Cat G = {functor := category_theory.grothendieck.grothendieck_Type_to_Cat_functor G, inverse := category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat)), X.cases_on (λ (X_base : C) (X_fiber : ↥((G ⋙ category_theory.Type_to_Cat).obj X_base)), category_theory.discrete.cases_on X_fiber (λ (X_fiber : G.obj X_base), category_theory.iso.refl ((𝟭 (category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat))).obj {base := X_base, fiber := {as := X_fiber}})))) _, counit_iso := category_theory.nat_iso.of_components (λ (X : G.elements), sigma.cases_on X (λ (X_fst : C) (X_snd : G.obj X_fst), category_theory.iso.refl ((category_theory.grothendieck.grothendieck_Type_to_Cat_inverse G ⋙ category_theory.grothendieck.grothendieck_Type_to_Cat_functor G).obj ⟨X_fst, X_snd⟩))) _, functor_unit_iso_comp' := _}