The Groupidal Grothendieck construction

↑Grothendieck (toCat A) -- toPGrpd --> PGrpd | | | | ↑ Grothendieck.forget PGrpd.forgetToGrpd | | v v ↑Γ--------------A---------------> Grpd

Main definitions

• CategoryTheory.Grothendieck.Groupoidal takes a functor from a groupoid into Grpd the category of groupoids, composes it with the forgetful functor into Cat the category of categories, then applies CategoryTheory.Grothendieck. This is a groupoid.

Main statements

• CategoryTheory.Grothendieck.Groupoidal.groupoid is an instance of a groupoid structure on the groupidal Grothendieck construction.
• CategoryTheory.Grothendieck.Groupoidal.isPullback shows that Grothendieck.forget A is classified by PGrpd.forgetToGrpd as the pullback of A. This uses the proof of the similar fact CategoryTheory.Grothendieck.isPullback, as well as the proof CategoryTheory.isPullback_forgetToGrpd_forgetToCat that PGrpd is the pullback of PCat.

• TODO Probably the proof of Groupoidal.IsPullback can be shortened significantly by providing a direct proof of pullback using the IsMegaPullback defintions
• NOTE Design: Groupoidal.ι, Groupoidal.pre and so on should not be reduced by simp. Instead we should add simp lemmas by hand. This avoids Grpd.forgetToCat cluttering the user's context

@[reducible, inline]

abbrev CategoryTheory.Groupoid.compForgetToCat {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : Functor Γ Cat

Equations

• CategoryTheory.Groupoid.compForgetToCat A = A.comp CategoryTheory.Grpd.forgetToCat

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.Groupoidal {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C 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.Grothendieck.Groupoidal F = CategoryTheory.Grothendieck (CategoryTheory.Groupoid.compForgetToCat F)

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

Equations

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

instance CategoryTheory.Grothendieck.Groupoidal.instGroupoidαCategoryObjCatCompForgetToCat {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (X : C) : Groupoid ↑((Groupoid.compForgetToCat F).obj X)

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.Grothendieck.Groupoidal.inv f = (CategoryTheory.Grothendieck.Groupoidal.isoMk f).inv

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

Equations

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

def CategoryTheory.Grothendieck.Groupoidal.ι {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) : Functor (↑(F.obj c)) (Groupoidal F)

The inclusion of a fiber F.obj c of a functor F : C ⥤ Cat into its groupoidal Grothendieck construction.

Equations

• CategoryTheory.Grothendieck.Groupoidal.ι F c = CategoryTheory.Grothendieck.ι (F.comp CategoryTheory.Grpd.forgetToCat) c

def CategoryTheory.Grothendieck.Groupoidal.map {C : Type u} [Groupoid C] {F G : Functor C Grpd} (α : F ⟶ G) : Functor (Groupoidal F) (Groupoidal G)

The groupoidal Grothendieck construction is functorial: a natural transformation α : F ⟶ G induces a functor Groupoidal.map : Groupoidal F ⥤ Groupoidal G.

Equations

• CategoryTheory.Grothendieck.Groupoidal.map α = CategoryTheory.Grothendieck.map (CategoryTheory.whiskerRight α CategoryTheory.Grpd.forgetToCat)

theorem CategoryTheory.Grothendieck.Groupoidal.map_obj {C : Type u} [Groupoid C] {F G : Functor C Grpd} {α : F ⟶ G} (X : Groupoidal F) : (map α).obj X = { base := X.base, fiber := (α.app X.base).obj X.fiber }

def CategoryTheory.Grothendieck.Groupoidal.pre {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor D Grpd) (G : Functor C D) : Functor (Groupoidal (G.comp F)) (Groupoidal F)

Applying a functor G : D ⥤ C to the base of the groupoidal Grothendieck construction induces a functor Groupoidal (G ⋙ F) ⥤ Groupoidal F.

Equations

• CategoryTheory.Grothendieck.Groupoidal.pre F G = CategoryTheory.Grothendieck.pre (F.comp CategoryTheory.Grpd.forgetToCat) G

def CategoryTheory.Grothendieck.Groupoidal.functorial {C D : Grpd} (F : C ⟶ D) (G : Functor (↑D) Grpd) : Functor (Grothendieck (Groupoid.compForgetToCat (Functor.comp F G))) (Grothendieck (Groupoid.compForgetToCat G))

Equations

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

def CategoryTheory.Grothendieck.Groupoidal.Map (Δ : Grpd) (Γ : Grpd) (σ : Functor ↑Δ ↑Γ) (A : Functor (↑Γ) Grpd) (B : Functor (Groupoidal A) Grpd) : Functor (Groupoidal (σ.comp A)) Grpd

Equations

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

instance CategoryTheory.Grothendieck.Groupoidal.toPCatObjGroupoid {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (x : Grothendieck (Groupoid.compForgetToCat A)) : Groupoid ↑x.toPCatObj

Equations

• CategoryTheory.Grothendieck.Groupoidal.toPCatObjGroupoid A x = id inferInstance

instance CategoryTheory.Grothendieck.Groupoidal.toPCatObjPointed {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (x : Grothendieck (Groupoid.compForgetToCat A)) : PointedGroupoid ↑x.toPCatObj

Equations

• CategoryTheory.Grothendieck.Groupoidal.toPCatObjPointed A x = CategoryTheory.PointedGroupoid.of (↑x.toPCatObj) CategoryTheory.PointedCategory.pt

def CategoryTheory.Grothendieck.Groupoidal.toPGrpd {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : Functor (Grothendieck (Groupoid.compForgetToCat A)) PGrpd

Equations

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

theorem CategoryTheory.Grothendieck.Groupoidal.toPGrpd_comp_forgetToPCat {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : (toPGrpd A).comp PGrpd.forgetToPCat = toPCat (Groupoid.compForgetToCat A)

theorem CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.comm_sq {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : (toPGrpd A).comp PGrpd.forgetToGrpd = (forget (Groupoid.compForgetToCat A)).comp A

theorem CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.toPGrpd_eq_lift {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Grpd} : toPGrpd A = PGrpd.IsMegaPullback.lift (toPCat (Groupoid.compForgetToCat A)) ((forget (Groupoid.compForgetToCat A)).comp A) ⋯

def CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.lift {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Grpd} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PGrpd) (snd : Functor C Γ) (w : fst.comp PGrpd.forgetToGrpd = snd.comp A) : Functor C (Groupoidal A)

Equations

• CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.lift fst snd w = CategoryTheory.Grothendieck.IsMegaPullback.lift (fst.comp CategoryTheory.PGrpd.forgetToPCat) snd ⋯

theorem CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.fac_left' {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Grpd} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PGrpd) (snd : Functor C Γ) (w : fst.comp PGrpd.forgetToGrpd = snd.comp A) : ((lift fst snd w).comp (toPGrpd A)).comp PGrpd.forgetToPCat = fst.comp PGrpd.forgetToPCat

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.fac_left {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Grpd} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PGrpd) (snd : Functor C Γ) (w : fst.comp PGrpd.forgetToGrpd = snd.comp A) : (lift fst snd w).comp (toPGrpd A) = fst

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.fac_right {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Grpd} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PGrpd) (snd : Functor C Γ) (w : fst.comp PGrpd.forgetToGrpd = snd.comp A) : (lift fst snd w).comp (forget (Groupoid.compForgetToCat A)) = snd

theorem CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.lift_uniq {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Grpd} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PGrpd) (snd : Functor C Γ) (w : fst.comp PGrpd.forgetToGrpd = snd.comp A) (m : Functor C (Groupoidal A)) (hl : m.comp (toPGrpd A) = fst) (hr : m.comp (forget (Groupoid.compForgetToCat A)) = snd) : m = lift fst snd w

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftGrpd : Cat

Equations

• CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftGrpd = CategoryTheory.Cat.ofULift CategoryTheory.Grpd

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftA {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : Cat.ofULift Γ ⟶ uLiftGrpd

Equations

• CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftA A = CategoryTheory.ULift.downFunctor.comp (A.comp CategoryTheory.ULift.upFunctor)

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftPGrpd : Cat

Equations

• CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftPGrpd = CategoryTheory.Cat.ofULift CategoryTheory.PGrpd

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftPGrpdForgetToGrpd : uLiftPGrpd ⟶ uLiftGrpd

Equations

• CategoryTheory.Grothendieck.Groupoidal.IsPullback.uLiftPGrpdForgetToGrpd = CategoryTheory.ULift.downFunctor.comp (CategoryTheory.PGrpd.forgetToGrpd.comp CategoryTheory.ULift.upFunctor)

noncomputable def CategoryTheory.Grothendieck.Groupoidal.IsPullback.var' {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : IsPullback.uLiftGrothendieck (Groupoid.compForgetToCat A) ⟶ IsPullback.uLiftGrothendieck Grpd.forgetToCat

The universal lift var' : Grothendieck(Groupoid.compForgetToCat A) ⟶ Grothendieck(Grpd.forgetToCat) given by pullback pasting in the following pasting diagram.

↑Grothendieck (Groupoid.compForgetToCat A) .-.-.-.-> ↑GrothendieckForgetToCat -----> ↑PCat.{u,u} | | | | | | ↑ Grothendieck.forget ↑Grothendieck.forget ↑PCat.forgetToCat | | | v v v ↑Γ----------------------> ↑Grpd.{u,u} ----------------> ↑Cat.{u,u}

Equations

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

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.var'_uLiftToPCat {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : CategoryStruct.comp (var' A) (IsPullback.uLiftToPCat Grpd.forgetToCat) = IsPullback.uLiftToPCat (Groupoid.compForgetToCat A)

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.var'_forget {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : CategoryStruct.comp (var' A) (IsPullback.uLiftGrothendieckForget Grpd.forgetToCat) = CategoryStruct.comp (IsPullback.uLiftGrothendieckForget (Groupoid.compForgetToCat A)) (uLiftA A)

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.isPullback_uLiftGrothendieckForget_Groupoid.compForgetToCat_uLiftGrothendieckForget_grpdForgetToCat {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : IsPullback (Cat.homOf (var' A)) (IsPullback.uLiftGrothendieckForget (Groupoid.compForgetToCat A)) (IsPullback.uLiftGrothendieckForget Grpd.forgetToCat) (uLiftA A)

The following square is a pullback ↑Grothendieck (Groupoid.compForgetToCat A) ------- var' -------> ↑Grothendieck Grpd.forgetToCat | | | | ↑ Grothendieck.forget ↑Grothendieck.forget | | v v ↑Γ--------------↑A----------------------------> ↑Grpd.{u,u}

by pullback pasting

↑Grothendieck (Groupoid.compForgetToCat A) --> ↑Grothendieck Grpd.forgetToCat ---> ↑PCat.{u,u} | | | | | | ↑ Grothendieck.forget ↑Grothendieck.forget ↑PCat.forgetToCat | | | v v v ↑Γ----------------------> ↑Grpd.{u,u} ----------------> ↑Cat.{u,u}

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.isPullback_aux {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : IsPullback (CategoryStruct.comp (Cat.homOf (var' A)) (Cat.ULift_iso_self ≪≫ PGrpd.isoGrothendieckForgetToCat.symm).hom) (IsPullback.uLiftGrothendieckForget (Groupoid.compForgetToCat A)) (Cat.homOf PGrpd.forgetToGrpd) (CategoryStruct.comp (uLiftA A) Cat.ULift_iso_self.hom)

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.toPGrpd_comp_forgetToPCat_eq_var'_comp_isoGrothendieckForgetToCatInv_comp_forgetToPCat {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : ULift.downFunctor.comp ((toPGrpd A).comp PGrpd.forgetToPCat) = Functor.comp (var' A) (ULift.downFunctor.comp (PGrpd.isoGrothendieckForgetToCatInv.comp PGrpd.forgetToPCat))

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.toPGrpd_comp_forgetToGrpd_eq_var'_comp_isoGrothendieckForgetToCatInv_comp_forgetToGrpd {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : ULift.downFunctor.comp ((toPGrpd A).comp PGrpd.forgetToGrpd) = Functor.comp (var' A) (ULift.downFunctor.comp (PGrpd.isoGrothendieckForgetToCatInv.comp PGrpd.forgetToGrpd))

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.toPGrpd_eq_var'_comp_isoGrothendieckForgetToCatInv' {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : Cat.homOf (ULift.downFunctor.comp (toPGrpd A)) = Cat.homOf (Functor.comp (var' A) (ULift.downFunctor.comp PGrpd.isoGrothendieckForgetToCatInv))

theorem CategoryTheory.Grothendieck.Groupoidal.IsPullback.toPGrpd_eq_var'_comp_isoGrothendieckForgetToCatInv {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : ULift.downFunctor.comp (toPGrpd A) = Functor.comp (var' A) (ULift.downFunctor.comp PGrpd.isoGrothendieckForgetToCatInv)

theorem CategoryTheory.Grothendieck.Groupoidal.isPullback {Γ : Type u} [Category.{u, u} Γ] (A : Functor Γ Grpd) : IsPullback (Cat.homOf (ULift.downFunctor.comp (toPGrpd A))) (IsPullback.uLiftGrothendieckForget (Groupoid.compForgetToCat A)) (Cat.homOf PGrpd.forgetToGrpd) (Cat.homOf (ULift.downFunctor.comp A))

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.ιCompPre {Γ : Type u₂} [Category.{v₂, u₂} Γ] {Δ : Type u₃} [Category.{v₃, u₃} Δ] (σ : Functor Δ Γ) (A : Functor Γ Grpd) (x : Δ) : (ι (σ.comp A) x).comp (pre A σ) = ι A (σ.obj x)

def CategoryTheory.Grothendieck.Groupoidal.sec {Γ : Grpd} (α : Functor (↑Γ) PGrpd) : Functor (↑Γ) (Groupoidal (α.comp PGrpd.forgetToGrpd))

sec is the universal lift in the following diagram, which is a section of Groupoidal.forget α ===== Γ -------α--------------¬ ‖ ↓ sec V ‖ M.ext A ⋯ -------------> PGrpd ‖ | | ‖ | | ‖ forget forgetToGrpd ‖ | | ‖ V V ===== Γ --α ≫ forgetToGrpd--> Grpd

Equations

• CategoryTheory.Grothendieck.Groupoidal.sec α = CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.lift α (CategoryTheory.Functor.id ↑Γ) ⋯

@[simp]

def CategoryTheory.Grothendieck.Groupoidal.sec_toPGrpd {Γ : Grpd} (α : Functor (↑Γ) PGrpd) : (sec α).comp (toPGrpd (α.comp PGrpd.forgetToGrpd)) = α

Equations

• ⋯ = ⋯

@[simp]

def CategoryTheory.Grothendieck.Groupoidal.sec_forget {Γ : Grpd} (α : Functor (↑Γ) PGrpd) : (sec α).comp (forget (Groupoid.compForgetToCat (α.comp PGrpd.forgetToGrpd))) = Functor.id ↑Γ

Equations

• ⋯ = ⋯