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.

source
structure CategoryTheory.Grothendieck {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) :
Type (max u_1 u_4)
  • 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
    source
    structure CategoryTheory.Grothendieck.Hom {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) :
    Type (max u_3 u_5)
    • 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
      source
      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
      source
      @[simp]
      theorem CategoryTheory.Grothendieck.id_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) :
      (CategoryTheory.Grothendieck.id X).fiber = CategoryTheory.eqToHom (_ : (F.map (CategoryTheory.CategoryStruct.id X.base)).obj X.fiber = X.fiber)
      source
      @[simp]
      theorem CategoryTheory.Grothendieck.id_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) :
      (CategoryTheory.Grothendieck.id X).base = CategoryTheory.CategoryStruct.id X.base
      source
      def CategoryTheory.Grothendieck.id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) :
      CategoryTheory.Grothendieck.Hom X X

      The identity morphism in the Grothendieck category.

      Instances For
        source
        instance CategoryTheory.Grothendieck.instInhabitedHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) :
        Inhabited (CategoryTheory.Grothendieck.Hom X X)
        source
        @[simp]
        theorem CategoryTheory.Grothendieck.comp_base {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} {Z : CategoryTheory.Grothendieck F} (f : CategoryTheory.Grothendieck.Hom X Y) (g : CategoryTheory.Grothendieck.Hom Y Z) :
        (CategoryTheory.Grothendieck.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
        source
        @[simp]
        theorem CategoryTheory.Grothendieck.comp_fiber {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} {Z : CategoryTheory.Grothendieck F} (f : CategoryTheory.Grothendieck.Hom X Y) (g : CategoryTheory.Grothendieck.Hom Y Z) :
        (CategoryTheory.Grothendieck.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (F.map (CategoryTheory.CategoryStruct.comp f.base g.base)).obj X.fiber = (F.map g.base).obj ((F.map f.base).obj X.fiber))) (CategoryTheory.CategoryStruct.comp ((F.map g.base).map f.fiber) g.fiber)
        source
        def CategoryTheory.Grothendieck.comp {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} {Z : CategoryTheory.Grothendieck F} (f : CategoryTheory.Grothendieck.Hom X Y) (g : CategoryTheory.Grothendieck.Hom Y Z) :
        CategoryTheory.Grothendieck.Hom X Z

        Composition of morphisms in the Grothendieck category.

        Instances For
          source
          instance CategoryTheory.Grothendieck.instCategoryGrothendieck {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} :
          CategoryTheory.Category.{max u_5 u_3, max u_4 u_1} (CategoryTheory.Grothendieck F)
          source
          @[simp]
          theorem CategoryTheory.Grothendieck.id_fiber' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) :
          (CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom (_ : (F.map (CategoryTheory.CategoryStruct.id X).base).obj X.fiber = X.fiber)
          source
          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
          source
          @[simp]
          theorem CategoryTheory.Grothendieck.forget_map {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) :
          (CategoryTheory.Grothendieck.forget F).map f = f.base
          source
          @[simp]
          theorem CategoryTheory.Grothendieck.forget_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) :
          (CategoryTheory.Grothendieck.forget F).obj X = X.base
          source
          def CategoryTheory.Grothendieck.forget {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) :
          CategoryTheory.Functor (CategoryTheory.Grothendieck F) C

          The forgetful functor from Grothendieck F to the source category.

          Instances For
            source
            @[simp]
            theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst {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.grothendieckTypeToCatFunctor G).obj X).fst = X.base
            source
            @[simp]
            theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe {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)) (Y : CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat)) (f : X ⟶ Y) :
            ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base
            source
            @[simp]
            theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd {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.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as
            source
            def CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) :
            CategoryTheory.Functor (CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat)) (CategoryTheory.Functor.Elements G)

            Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) :
              ∀ {X Y : CategoryTheory.Functor.Elements G} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).map f).base = ↑f
              source
              @[simp]
              theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements G) :
              ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst
              source
              @[simp]
              theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements G) :
              ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).fiber.as = X.snd
              source
              def CategoryTheory.Grothendieck.grothendieckTypeToCatInverse {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) :
              CategoryTheory.Functor (CategoryTheory.Functor.Elements G) (CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat))

              Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

              Instances For
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements G) :
                ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).fiber.as = X.snd
                source
                @[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)
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements G) :
                ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).base = X.fst
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base {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).base = CategoryTheory.CategoryStruct.id X.base
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements G) :
                ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.hom.app X) = CategoryTheory.CategoryStruct.id X.fst
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Functor.Elements G) :
                ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.inv.app X) = CategoryTheory.CategoryStruct.id X.fst
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) :
                ∀ {X Y : CategoryTheory.Functor.Elements G} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.map f).base = ↑f
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe {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)) (Y : CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat)) (f : X ⟶ Y) :
                ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base
                source
                @[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)
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd {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).functor.obj X).snd = X.fiber.as
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst {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).functor.obj X).fst = X.base
                source
                @[simp]
                theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base {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).base = CategoryTheory.CategoryStruct.id X.base
                source
                def CategoryTheory.Grothendieck.grothendieckTypeToCat {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) :
                CategoryTheory.Grothendieck (CategoryTheory.Functor.comp G CategoryTheory.typeToCat) ≌ CategoryTheory.Functor.Elements G

                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