Documentation

Mathlib.CategoryTheory.Grothendieck

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 CategoryTheory.Functor.Elements for the category of elements of functor F : C ⥤ Type.

  • base : C

    The underlying object in C

  • fiber : ↑(F.obj s.base)

    The object in the fiber of the base object.

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

Instances For
    • base : X.base Y.base

      The morphism between base objects.

    • fiber : (F.map s.base).obj X.fiber Y.fiber

      The morphism from the pushforward to the source fiber object to the target fiber object.

    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
      theorem CategoryTheory.Grothendieck.ext {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} (f : CategoryTheory.Grothendieck.Hom X Y) (g : CategoryTheory.Grothendieck.Hom X Y) (w_base : f.base = g.base) (w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (F.map g.base).obj X.fiber = (F.map f.base).obj X.fiber)) f.fiber = g.fiber) :
      f = g
      theorem CategoryTheory.Grothendieck.congr {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} {f : X Y} {g : X Y} (h : f = g) :
      f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (F.map f.base).obj X.fiber = (F.map g.base).obj X.fiber)) g.fiber
      @[simp]
      theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat)) :
      ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom (_ : ((CategoryTheory.Functor.comp G CategoryTheory.typeToCat).map (CategoryTheory.CategoryStruct.id { base := X.base, fiber := { as := X.2.as } }.base)).obj { base := X.base, fiber := { as := X.2.as } }.fiber = { base := X.base, fiber := { as := X.2.as } }.fiber)
      @[simp]
      theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat)) :
      ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom (_ : ((CategoryTheory.Functor.comp G CategoryTheory.typeToCat).map (CategoryTheory.CategoryStruct.id { base := X.base, fiber := { as := X.2.as } }.base)).obj { base := X.base, fiber := { as := X.2.as } }.fiber = { base := X.base, fiber := { as := X.2.as } }.fiber)

      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.

      Instances For