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.Functor.Groupoidal.toPGrpd {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) :

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.

Instances For

source

@[simp]

theorem CategoryTheory.Functor.Groupoidal.toPGrpd_obj_base {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (x : A.Groupoidal) :

((toPGrpd A).obj x).base = A.obj x.base

source

@[simp]

theorem CategoryTheory.Functor.Groupoidal.toPGrpd_obj_fiber {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) (x : A.Groupoidal) :

((toPGrpd A).obj x).fiber = x.fiber

source

@[simp]

theorem CategoryTheory.Functor.Groupoidal.toPGrpd_map_base {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) {x y : A.Groupoidal} (f : x ⟶ y) :

((toPGrpd A).map f).base = A.map (Hom.base f)

source

@[simp]

theorem CategoryTheory.Functor.Groupoidal.toPGrpd_map_fiber {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) {x y : A.Groupoidal} (f : x ⟶ y) :

((toPGrpd A).map f).fiber = Hom.fiber f

source

theorem CategoryTheory.Functor.Groupoidal.toPGrpd_forgetToGrpd {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) :

(toPGrpd A).comp PGrpd.forgetToGrpd = forget.comp A

source

theorem CategoryTheory.Functor.Groupoidal.toPGrpd_forgetToPCat {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Grpd) :

(toPGrpd A).comp PGrpd.forgetToPCat = Grothendieck.toPCat (A.comp Grpd.forgetToCat)

source

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

Functor A.Groupoidal 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.

Instances For

source

def CategoryTheory.Functor.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.

Instances For

source

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

toPGrpd A = toPGrpd' A

source

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

(toPGrpd A).IsPullback forget PGrpd.forgetToGrpd A

Equations

CategoryTheory.Functor.Groupoidal.isPullback A = cast ⋯ (CategoryTheory.Functor.Groupoidal.isPullback' A)

Instances For

source

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

Functor Γ A.Groupoidal

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.

Instances For

source

@[simp]

theorem CategoryTheory.Functor.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

source

@[simp]

theorem CategoryTheory.Functor.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

source

@[simp]

theorem CategoryTheory.Functor.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

source

@[simp]

theorem CategoryTheory.Functor.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

source

@[simp]

def CategoryTheory.Functor.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

⋯ = ⋯

Instances For

source

@[simp]

def CategoryTheory.Functor.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

⋯ = ⋯

Instances For

source

theorem CategoryTheory.Functor.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 Γ) ⋯

source

@[simp]

theorem CategoryTheory.Functor.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)

source

theorem CategoryTheory.Functor.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 σ)

source

theorem CategoryTheory.Functor.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) ⋯

source

@[simp]

theorem CategoryTheory.Functor.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).Groupoidal) :

Hom.base ((preNatIso F α).hom.app x) = α.hom.app x.base

source

@[simp]

theorem CategoryTheory.Functor.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).Groupoidal) :

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)

Documentation

GroupoidModel.Grothendieck.Groupoidal.IsPullback

The Grothendieck construction as a pullback of categories #