The Grothendieck construction as a pullback of categories

• CategoryTheory.Grothendieck.Groupoidal.isPullback shows that Grothendieck.forget A is classified by PGrpd.forgetToGrpd as the (meta-theoretic) 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

   ∫(A) ------- toPGrpd ---------> PGrpd
    |                                 |
    |                                 |
  

  forget PGrpd.forgetToGrpd | | v v Γ--------------A---------------> Grpd

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

toPGrpd is the lift induced by the pullback property of PGrpd ∫(A) ------- toPGrpd ---------> PGrpd --------> PCat | | | | | | forget PGrpd.forgetToGrpd PCat.forgetToCat | | | | | | v v v Γ--------------A---------------> Grpd --------> Cat

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.toPGrpd_obj_base {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (x : ∫(A)) : ((toPGrpd A).obj x).base = A.obj x.base

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.toPGrpd_obj_fiber {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (x : ∫(A)) : ((toPGrpd A).obj x).fiber = x.fiber

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.toPGrpd_map_base {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) {x y : ∫(A)} (f : x ⟶ y) : ((toPGrpd A).map f).base = A.map (Hom.base f)

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.toPGrpd_map_fiber {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) {x y : ∫(A)} (f : x ⟶ y) : ((toPGrpd A).map f).fiber = Hom.fiber f

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

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

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

We also provide a definition of toPGrpd as the universal lift of the pullback PGrpd.

Equations

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

def CategoryTheory.Grothendieck.Groupoidal.isPullback' {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : (toPGrpd' A).IsPullback forget PGrpd.forgetToGrpd A

The left square is a pullback since the right square and outer square are. ∫(A) ------- toPGrpd ---------> PGrpd --------> PCat | | | | | | forget PGrpd.forgetToGrpd PCat.forgetToCat | | | | | | v v v Γ--------------A---------------> Grpd --------> Cat

Equations

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

theorem CategoryTheory.Grothendieck.Groupoidal.toPGrpd_eq_toPGrpd' {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : toPGrpd A = toPGrpd' A

def CategoryTheory.Grothendieck.Groupoidal.isPullback {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) : (toPGrpd A).IsPullback forget PGrpd.forgetToGrpd A

Equations

• CategoryTheory.Grothendieck.Groupoidal.isPullback A = cast ⋯ (CategoryTheory.Grothendieck.Groupoidal.isPullback' A)

def CategoryTheory.Grothendieck.Groupoidal.sec {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) : Functor Γ ∫(A)

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

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.sec_obj_base {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) (x : Γ) : ((sec A α h).obj x).base = x

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.sec_obj_fiber {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) (x : Γ) : ((sec A α h).obj x).fiber = PGrpd.objFiber' h x

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.sec_map_base {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) {x y : Γ} {f : x ⟶ y} : Hom.base ((sec A α h).map f) = f

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.sec_map_fiber {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) {x y : Γ} {f : x ⟶ y} : Hom.fiber ((sec A α h).map f) = PGrpd.mapFiber' h f

@[simp]

def CategoryTheory.Grothendieck.Groupoidal.sec_toPGrpd {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) : (sec A α h).comp (toPGrpd A) = α

Equations

• ⋯ = ⋯

@[simp]

def CategoryTheory.Grothendieck.Groupoidal.sec_forget {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) : (sec A α h).comp forget = Functor.id Γ

Equations

• ⋯ = ⋯

theorem CategoryTheory.Grothendieck.Groupoidal.sec_eq_lift {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) : sec A α h = (isPullback A).lift α (Functor.id Γ) ⋯

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.pre_toPGrpd {Γ : Type u} [Category.{v, u} Γ] {Δ : Type u₃} [Category.{v₃, u₃} Δ] (σ : Functor Δ Γ) (A : Functor Γ Grpd) : (pre A σ).comp (toPGrpd A) = toPGrpd (σ.comp A)

theorem CategoryTheory.Grothendieck.Groupoidal.sec_naturality {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (α : Functor Γ PGrpd) (h : α.comp PGrpd.forgetToGrpd = A) {Δ : Type u₃} [Category.{v₃, u₃} Δ] (σ : Functor Δ Γ) : σ.comp (sec A α h) = (sec (σ.comp A) (σ.comp α) ⋯).comp (pre A σ)

theorem CategoryTheory.Grothendieck.Groupoidal.ι_eq_lift {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) : ι F c = (isPullback F).lift ((ι F c).comp (toPGrpd F)) ((ι F c).comp forget) ⋯

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.preNatIso_hom_app_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) {G H : Functor D C} (α : G ≅ H) (x : ∫(G.comp F)) : Hom.base ((preNatIso F α).hom.app x) = α.hom.app x.base

@[simp]

theorem CategoryTheory.Grothendieck.Groupoidal.preNatIso_hom_app_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) {G H : Functor D C} (α : G ≅ H) (x : ∫(G.comp F)) : Hom.fiber ((preNatIso F α).hom.app x) = CategoryStruct.id ((F.map (Hom.base ((preNatIso F α).hom.app x))).obj ((pre F G).obj x).fiber)