Here we define the Grothendieck construction for groupoids

def CategoryTheory.toCat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) : CategoryTheory.Functor C CategoryTheory.Cat

Equations

• CategoryTheory.toCat G = G.comp CategoryTheory.Grpd.forgetToCat

@[simp]

theorem CategoryTheory.toCat_obj_α {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) (X : C) : ↑((CategoryTheory.toCat G).obj X) = ↑(G.obj X)

@[simp]

theorem CategoryTheory.toCat_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.toCat G).map f = CategoryTheory.Grpd.forgetToCat.map (G.map f)

@[simp]

theorem CategoryTheory.toCat_obj_str {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Functor C CategoryTheory.Grpd) (X : C) : ((CategoryTheory.toCat G).obj X).str = CategoryTheory.Groupoid.toCategory

def CategoryTheory.Grothendieck.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck G} {Y : CategoryTheory.Grothendieck G} (s : X.base ≅ Y.base) (t : (G.map s.hom).obj X.fiber ≅ Y.fiber) : X ≅ Y

A morphism in the Grothendieck construction is an isomorphism if

• the morphism in the base is an isomorphism; and
• the fiber morphism is an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.GroupoidalGrothendieck {C : Type u₁} [CategoryTheory.Groupoid C] (F : CategoryTheory.Functor C CategoryTheory.Grpd) : Type (max u₁ u₂)

In Mathlib.CategoryTheory.Grothendieck we find the Grothendieck construction for the functors F : C ⥤ Cat. Given a functor F : G ⥤ Grpd, we show that the Grothendieck construction of the composite F ⋙ Grpd.forgetToCat, where forgetToCat : Grpd ⥤ Cat is the embedding of groupoids into categories, is a groupoid.

Equations

• CategoryTheory.GroupoidalGrothendieck F = CategoryTheory.Grothendieck (CategoryTheory.toCat F)

instance CategoryTheory.GroupoidalGrothendieck.instCategory {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} (CategoryTheory.GroupoidalGrothendieck F)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.GroupoidalGrothendieck.instGroupoidαCategoryObjCatToCat {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} (X : C) : CategoryTheory.Groupoid ↑((CategoryTheory.toCat F).obj X)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.GroupoidalGrothendieck.isoMk {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} {X : CategoryTheory.GroupoidalGrothendieck F} {Y : CategoryTheory.GroupoidalGrothendieck F} (f : X ⟶ Y) : X ≅ Y

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.GroupoidalGrothendieck.inv {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} {X : CategoryTheory.GroupoidalGrothendieck F} {Y : CategoryTheory.GroupoidalGrothendieck F} (f : X ⟶ Y) : Y ⟶ X

Equations

• CategoryTheory.GroupoidalGrothendieck.inv f = (CategoryTheory.GroupoidalGrothendieck.isoMk f).inv

instance CategoryTheory.GroupoidalGrothendieck.groupoid {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Groupoid (CategoryTheory.GroupoidalGrothendieck F)

Equations

• CategoryTheory.GroupoidalGrothendieck.groupoid = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.GroupoidalGrothendieck F} (f : X ⟶ Y) => CategoryTheory.GroupoidalGrothendieck.inv f) ⋯ ⋯

def CategoryTheory.GroupoidalGrothendieck.forget {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Functor (CategoryTheory.GroupoidalGrothendieck F) C

Equations

• CategoryTheory.GroupoidalGrothendieck.forget = CategoryTheory.Grothendieck.forget (F.comp CategoryTheory.Grpd.forgetToCat)

def CategoryTheory.GroupoidalGrothendieck.ToGrpd {C : Type u₁} [CategoryTheory.Groupoid C] {F : CategoryTheory.Functor C CategoryTheory.Grpd} : CategoryTheory.Functor (CategoryTheory.GroupoidalGrothendieck F) CategoryTheory.Grpd

Equations

• CategoryTheory.GroupoidalGrothendieck.ToGrpd = CategoryTheory.GroupoidalGrothendieck.forget.comp F

def CategoryTheory.GroupoidalGrothendieck.functorial {C : CategoryTheory.Grpd} {D : CategoryTheory.Grpd} (F : C ⟶ D) (G : CategoryTheory.Functor (↑D) CategoryTheory.Grpd) : CategoryTheory.Functor (CategoryTheory.Grothendieck (CategoryTheory.toCat (CategoryTheory.Functor.comp F G))) (CategoryTheory.Grothendieck (CategoryTheory.toCat G))

Equations

• One or more equations did not get rendered due to their size.