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.

Implementation notes

• To avoid Grpd.forgetToCat cluttering the user's context, although we use Grothendieck to define Grothendieck.Groupoidal, all definitions and lemmas are restated. This probably also means that Lean has an easier time when type checking, as long as the user does not unfold down to Grothendieck definitions.

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

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

def CategoryTheory.Functor.Groupoidal.Functor.simpIdComp : Lean.Meta.Simp.DSimproc

A dsimp rule that reduces 𝟭 _ ⋙ F to F even if the domain categories are not syntactically equal.

Equations

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

def CategoryTheory.Functor.Groupoidal.Functor.simpCompId : Lean.Meta.Simp.DSimproc

A dsimp rule that reduces F ⋙ 𝟭 _ to F even if the codomain categories are not syntactically equal.

Equations

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

def CategoryTheory.Functor.Groupoidal.«term∫_» : Lean.ParserDescr

Equations

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

def CategoryTheory.Functor.Groupoidal.Hom {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (x y : F.Groupoidal) : Type (max v₁ v₂)

A morphism in the groupoidal Grothendieck category F : C ⥤ Grpd is defined to be a morphism in the Grothendieck category F ⋙ Grpd.forgetToCat.

Equations

• x.Hom y = CategoryTheory.Functor.Grothendieck.Hom x y

def CategoryTheory.Functor.Groupoidal.id {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (x : F.Groupoidal) : x.Hom x

Equations

• x.id = CategoryTheory.Functor.Grothendieck.Hom.id x

def CategoryTheory.Functor.Groupoidal.comp {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {x y z : F.Groupoidal} (f : x.Hom y) (g : y.Hom z) : x.Hom z

Equations

• CategoryTheory.Functor.Groupoidal.comp f g = CategoryTheory.Functor.Grothendieck.Hom.comp f g

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

Equations

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

def CategoryTheory.Functor.Groupoidal.base {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (p : F.Groupoidal) : C

Equations

• p.base = p.base

def CategoryTheory.Functor.Groupoidal.fiber {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (p : F.Groupoidal) : ↑(F.obj p.base)

Equations

• p.fiber = p.fiber

def CategoryTheory.Functor.Groupoidal.Hom.base {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {x y : F.Groupoidal} (f : x.Hom y) : x.base ⟶ y.base

The morphism between base objects.

Equations

• f.base = f.base

def CategoryTheory.Functor.Groupoidal.Hom.fiber {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {x y : F.Groupoidal} (f : x.Hom y) : (F.map f.base).obj x.fiber ⟶ y.fiber

The morphism from the pushforward to the source fiber object to the target fiber object.

Equations

• f.fiber = f.fiber

def CategoryTheory.Functor.Groupoidal.forget {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} : Functor F.Groupoidal C

Equations

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

@[simp]

theorem CategoryTheory.Functor.Groupoidal.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (x : F.Groupoidal) : forget.obj x = x.base

@[simp]

theorem CategoryTheory.Functor.Groupoidal.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {x y : F.Groupoidal} (f : x ⟶ y) : forget.map f = Hom.base f

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

We should use this to introduce objects, rather than the API for Grothendieck. This might seem redundant, but it simplifies the goal when making a point so that it does not show the composition with Grpd.forgetToCat

Equations

• CategoryTheory.Functor.Groupoidal.objMk c x = { base := c, fiber := x }

@[simp]

theorem CategoryTheory.Functor.Groupoidal.objMk_base {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (c : C) (x : ↑(F.obj c)) : (objMk c x).base = c

@[simp]

theorem CategoryTheory.Functor.Groupoidal.objMk_fiber {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (c : C) (x : ↑(F.obj c)) : (objMk c x).fiber = x

def CategoryTheory.Functor.Groupoidal.homMk {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (fb : X.base ⟶ Y.base) (ff : (F.map fb).obj X.fiber ⟶ Y.fiber) : X ⟶ Y

We should use this to introduce morphisms, rather than the API for Grothendieck. This might seem redundant, but it simplifies the goal when making a path in the fiber so that it does not show the composition with Grpd.forgetToCat

Equations

• CategoryTheory.Functor.Groupoidal.homMk fb ff = { base := fb, fiber := ff }

@[simp]

theorem CategoryTheory.Functor.Groupoidal.homMk_base {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (fb : X.base ⟶ Y.base) (ff : (F.map fb).obj X.fiber ⟶ Y.fiber) : Hom.base (homMk fb ff) = fb

@[simp]

theorem CategoryTheory.Functor.Groupoidal.homMk_fiber {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (fb : X.base ⟶ Y.base) (ff : (F.map fb).obj X.fiber ⟶ Y.fiber) : Hom.fiber (homMk fb ff) = ff

@[simp]

theorem CategoryTheory.Functor.Groupoidal.id_base {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (X : F.Groupoidal) : Hom.base (CategoryStruct.id X) = CategoryStruct.id X.base

@[simp]

theorem CategoryTheory.Functor.Groupoidal.id_fiber {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} (X : F.Groupoidal) : Hom.fiber (CategoryStruct.id X) = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.Groupoidal.comp_base {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y Z : F.Groupoidal} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.base (CategoryStruct.comp f g) = CategoryStruct.comp (Hom.base f) (Hom.base g)

@[simp]

theorem CategoryTheory.Functor.Groupoidal.comp_fiber {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y Z : F.Groupoidal} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.fiber (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (Hom.base g)).map (Hom.fiber f)) (Hom.fiber g))

@[simp]

theorem CategoryTheory.Functor.Groupoidal.base_eqToHom {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (h : X = Y) : Hom.base (eqToHom h) = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.Groupoidal.fiber_eqToHom {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (h : X = Y) : Hom.fiber (eqToHom h) = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.Groupoidal.Grothendieck.Groupoidal.eta {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A : Functor Γ Grpd} (x : A.Groupoidal) : objMk x.base x.fiber = x

@[simp]

theorem CategoryTheory.Functor.Groupoidal.Grothendieck.Groupoidal.Hom.eta {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A : Functor Γ Grpd} {x y : A.Groupoidal} (f : x ⟶ y) : homMk (Hom.base f) (Hom.fiber f) = f

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

Equations

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

def CategoryTheory.Functor.Groupoidal.transport {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : F.Groupoidal

If F : C ⥤ Grpd is a functor and t : c ⟶ d is a morphism in C, then transport maps each c-based element of ∫(F) to a d-based element.

Equations

• x.transport t = CategoryTheory.Functor.Grothendieck.transport x t

@[simp]

theorem CategoryTheory.Functor.Groupoidal.transport_base {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : (x.transport t).base = c

@[simp]

theorem CategoryTheory.Functor.Groupoidal.transport_fiber {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : (x.transport t).fiber = (F.map t).obj x.fiber

def CategoryTheory.Functor.Groupoidal.toTransport {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : x ⟶ x.transport t

If F : C ⥤ Cat is a functor and t : c ⟶ d is a morphism in C, then transport maps each c-based element x of Grothendieck F to a d-based element x.transport t.

toTransport is the morphism x ⟶ x.transport t induced by t and the identity on fibers.

Equations

• x.toTransport t = CategoryTheory.Functor.Grothendieck.toTransport x t

@[simp]

theorem CategoryTheory.Functor.Groupoidal.toTransport_base {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : Hom.base (x.toTransport t) = t

@[simp]

theorem CategoryTheory.Functor.Groupoidal.toTransport_fiber {C : Type u₁} [Groupoid C] {F : Functor C Grpd} (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : Hom.fiber (x.toTransport t) = CategoryStruct.id ((F.map t).obj x.fiber)

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ι_obj_base {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) (d : ↑(F.obj c)) : ((ι F c).obj d).base = c

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ι_obj_fiber {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) (d : ↑(F.obj c)) : ((ι F c).obj d).fiber = d

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ι_map_base {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) {X Y : ↑(F.obj c)} (f : X ⟶ Y) : Hom.base ((ι F c).map f) = CategoryStruct.id ((ι F c).obj X).base

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ι_map_fiber {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) {X Y : ↑(F.obj c)} (f : X ⟶ Y) : Hom.fiber ((ι F c).map f) = CategoryStruct.comp (eqToHom ⋯) f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ι_comp_forget {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) (c : C) : (ι F c).comp forget = (const ↑(F.obj c)).obj c

theorem CategoryTheory.Functor.Groupoidal.hext {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {x y : F.Groupoidal} (hbase : x.base = y.base) (hfiber : x.fiber ≍ y.fiber) : x = y

theorem CategoryTheory.Functor.Groupoidal.hext_iff {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {x y : F.Groupoidal} : x.base = y.base ∧ x.fiber ≍ y.fiber ↔ x = y

theorem CategoryTheory.Functor.Groupoidal.Hom.hext {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : f.fiber ≍ g.fiber) : f = g

theorem CategoryTheory.Functor.Groupoidal.Hom.hext_iff {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} (x y : F.Groupoidal) (f g : x ⟶ y) : base f = base g ∧ fiber f ≍ fiber g ↔ f = g

theorem CategoryTheory.Functor.Groupoidal.Hom.ext {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y : F.Groupoidal} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : f.fiber = CategoryStruct.comp (eqToHom ⋯) g.fiber) : f = g

theorem CategoryTheory.Functor.Groupoidal.Hom.ext_iff {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} (x y : F.Groupoidal) (f g : x ⟶ y) : (∃ (w_base : base f = base g), fiber f = CategoryStruct.comp (eqToHom ⋯) (fiber g)) ↔ f = g

theorem CategoryTheory.Functor.Groupoidal.hext' {C : Type u} [Category.{v, u} C] {F F' : Functor C Grpd} (h : F = F') {x : F.Groupoidal} {y : F'.Groupoidal} (hbase : x.base ≍ y.base) (hfiber : x.fiber ≍ y.fiber) : x ≍ y

theorem CategoryTheory.Functor.Groupoidal.Hom.hext' {C : Type u} [Category.{v, u} C] {F F' : Functor C Grpd} (h : F = F') {X Y : F.Groupoidal} {X' Y' : F'.Groupoidal} (hX : X ≍ X') (hY : Y ≍ Y') (f : X.Hom Y) (g : X'.Hom Y') (w_base : f.base ≍ g.base) (w_fiber : f.fiber ≍ g.fiber) : f ≍ g

theorem CategoryTheory.Functor.Groupoidal.FunctorTo.hext {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {D : Type u_1} [Category.{u_2, u_1} D] (G H : Functor D F.Groupoidal) (hbase : G.comp forget = H.comp forget) (hfiber_obj : ∀ (x : D), (G.obj x).fiber ≍ (H.obj x).fiber) (hfiber_map : ∀ {x y : D} (f : x ⟶ y), Hom.fiber (G.map f) ≍ Hom.fiber (H.map f)) : G = H

def CategoryTheory.Functor.Groupoidal.ιNatTrans {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y : C} (f : X ⟶ Y) : ι F X ⟶ Functor.comp (F.map f) (ι F Y)

Every morphism f : X ⟶ Y in the base category induces a natural transformation from the fiber inclusion ι F X to the composition F.map f ⋙ ι F Y.

Equations

• CategoryTheory.Functor.Groupoidal.ιNatTrans f = CategoryTheory.Functor.Grothendieck.ιNatTrans f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ιNatTrans_id_app {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X : C} {a : ↑(F.obj X)} : (ιNatTrans (CategoryStruct.id X)).app a = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ιNatTrans_comp_app {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {a : ↑(F.obj X)} : (ιNatTrans (CategoryStruct.comp f g)).app a = CategoryStruct.comp ((ιNatTrans f).app a) (CategoryStruct.comp ((ιNatTrans g).app ((F.map f).obj a)) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ιNatTrans_app_base {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : Hom.base ((ιNatTrans f).app d) = f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ιNatTrans_app_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : Hom.fiber ((ιNatTrans f).app d) = CategoryStruct.id ((F.map f).obj ((ι F X).obj d).fiber)

def CategoryTheory.Functor.Groupoidal.functorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) : Functor F.Groupoidal E

Construct a functor from Groupoidal F to another category E by providing a family of functors on the fibers of Groupoidal F, a family of natural transformations on morphisms in the base of Groupoidal F and coherence data for this family of natural transformations.

Equations

• CategoryTheory.Functor.Groupoidal.functorFrom fib hom hom_id hom_comp = CategoryTheory.Functor.Grothendieck.functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorFrom_obj {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) (X : F.Groupoidal) : (functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp).obj X = (fib X.base).obj X.fiber

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorFrom_map {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {X Y : F.Groupoidal} (f : X ⟶ Y) : (functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp).map f = CategoryStruct.comp ((hom (Hom.base f)).app X.fiber) ((fib Y.base).map (Hom.fiber f))

def CategoryTheory.Functor.Groupoidal.ιCompFunctorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) (c : C) : (ι F c).comp (functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp) ≅ fib c

Groupoidal.ι F c composed with Groupoidal.functorFrom is isomorphic a functor on a fiber on F supplied as the first argument to Groupoidal.functorFrom.

Equations

• CategoryTheory.Functor.Groupoidal.ιCompFunctorFrom fib hom hom_id hom_comp c = CategoryTheory.Functor.Grothendieck.ιCompFunctorFrom fib (fun {c c' : C} => hom) hom_id hom_comp c

def CategoryTheory.Functor.Groupoidal.fib' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (c : C) : Functor (↑((F.comp Grpd.forgetToCat).obj c)) E

Equations

• CategoryTheory.Functor.Groupoidal.fib' fib c = fib c

def CategoryTheory.Functor.Groupoidal.hom' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] {fib : (c : C) → Functor (↑(F.obj c)) E} (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) {c c' : C} (f : c ⟶ c') : fib' fib c ⟶ Functor.comp ((F.comp Grpd.forgetToCat).map f) (fib' fib c')

Equations

• CategoryTheory.Functor.Groupoidal.hom' hom f = hom f

def CategoryTheory.Functor.Groupoidal.functorFrom_comp_fib' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) {D : Type u_2} [Category.{u_4, u_2} D] (G : Functor E D) (c : C) : Functor (↑((F.comp Grpd.forgetToCat).obj c)) D

Equations

• CategoryTheory.Functor.Groupoidal.functorFrom_comp_fib' fib G c = CategoryTheory.Functor.Grothendieck.functorFrom_comp_fib (CategoryTheory.Functor.Groupoidal.fib' fib) G c

def CategoryTheory.Functor.Groupoidal.functorFrom_comp_fib {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) {D : Type u_2} [Category.{u_4, u_2} D] (G : Functor E D) (c : C) : Functor (↑(F.obj c)) D

Equations

• CategoryTheory.Functor.Groupoidal.functorFrom_comp_fib fib G c = CategoryTheory.Functor.Groupoidal.functorFrom_comp_fib' fib G c

def CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) {D : Type u_2} [Category.{u_4, u_2} D] (G : Functor E D) {c c' : C} (f : c ⟶ c') : functorFrom_comp_fib' fib G c ⟶ Functor.comp ((F.comp Grpd.forgetToCat).map f) (functorFrom_comp_fib' fib G c')

Equations

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

def CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) {D : Type u_2} [Category.{u_4, u_2} D] (G : Functor E D) {c c' : C} (f : c ⟶ c') : functorFrom_comp_fib' fib G c ⟶ Functor.comp (F.map f) (functorFrom_comp_fib' fib G c')

Equations

• CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom fib hom G f = CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom' fib (fun {c c' : C} => hom) G f

theorem CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom_id {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor E D) (c : C) : functorFrom_comp_hom fib (fun {c c' : C} => hom) G (CategoryStruct.id c) = eqToHom ⋯

theorem CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor E D) (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃) : functorFrom_comp_hom fib (fun {c c' : C} => hom) G (CategoryStruct.comp f g) = CategoryStruct.comp (functorFrom_comp_hom fib (fun {c c' : C} => hom) G f) (CategoryStruct.comp (whiskerLeft (F.map f) (functorFrom_comp_hom fib (fun {c c' : C} => hom) G g)) (eqToHom ⋯))

theorem CategoryTheory.Functor.Groupoidal.functorFrom_comp_hom_eq {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor E D) {c c' : C} (f : c ⟶ c') : functorFrom_comp_hom fib (fun {c c' : C} => hom) G f = whiskerRight (hom f) G

theorem CategoryTheory.Functor.Groupoidal.functorFrom_comp' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor E D) : (functorFrom (fib' fib) (fun {c c' : C} => hom' fun {c c' : C} => hom) hom_id hom_comp).comp G = functorFrom (functorFrom_comp_fib' fib G) (fun {c c' : C} => functorFrom_comp_hom' fib (fun {c c' : C} => hom) G) ⋯ ⋯

theorem CategoryTheory.Functor.Groupoidal.functorFrom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_4, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor E D) : (functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp).comp G = functorFrom (functorFrom_comp_fib fib G) (fun {c c' : C} => functorFrom_comp_hom fib (fun {c c' : C} => hom) G) ⋯ ⋯

def CategoryTheory.Functor.Groupoidal.asFunctorFrom_fib {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) (c : C) : Functor (↑(F.obj c)) E

Equations

• CategoryTheory.Functor.Groupoidal.asFunctorFrom_fib K c = CategoryTheory.Functor.Grothendieck.asFunctorFrom_fib K c

theorem CategoryTheory.Functor.Groupoidal.asFunctorFrom_fib' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) (c : C) : asFunctorFrom_fib K c = (ι F c).comp K

def CategoryTheory.Functor.Groupoidal.asFunctorFrom_hom {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) {c c' : C} (f : c ⟶ c') : asFunctorFrom_fib K c ⟶ Functor.comp (F.map f) (asFunctorFrom_fib K c')

Equations

• CategoryTheory.Functor.Groupoidal.asFunctorFrom_hom K f = CategoryTheory.Functor.Grothendieck.asFunctorFrom_hom K f

theorem CategoryTheory.Functor.Groupoidal.asFunctorFrom_hom' {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) {c c' : C} (f : c ⟶ c') : asFunctorFrom_hom K f = whiskerRight (ιNatTrans f) K

theorem CategoryTheory.Functor.Groupoidal.asFunctorFrom_hom_app {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) {c c' : C} (f : c ⟶ c') (p : ↑(F.obj c)) : (asFunctorFrom_hom K f).app p = K.map ((ιNatTrans f).app p)

theorem CategoryTheory.Functor.Groupoidal.asFunctorFrom_hom_id {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) (c : C) : asFunctorFrom_hom K (CategoryStruct.id c) = eqToHom ⋯

theorem CategoryTheory.Functor.Groupoidal.asFunctorFrom_hom_comp {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃) : asFunctorFrom_hom K (CategoryStruct.comp f g) = CategoryStruct.comp (asFunctorFrom_hom K f) (CategoryStruct.comp (whiskerLeft (F.map f) (asFunctorFrom_hom K g)) (eqToHom ⋯))

theorem CategoryTheory.Functor.Groupoidal.asFunctorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] (K : Functor F.Groupoidal E) : functorFrom (asFunctorFrom_fib K) (fun {c c' : C} => asFunctorFrom_hom K) ⋯ ⋯ = K

Groupoidal version of Grothendieck.asFunctorFrom

theorem CategoryTheory.Functor.Groupoidal.functorFrom_ext {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] {K K' : Functor F.Groupoidal E} (hfib : asFunctorFrom_fib K = asFunctorFrom_fib K') (hhom : ∀ {c c' : C} (f : c ⟶ c'), CategoryStruct.comp (asFunctorFrom_hom K f) (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (asFunctorFrom_hom K' f)) : K = K'

theorem CategoryTheory.Functor.Groupoidal.functorFrom_hext {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {E : Type u_1} [Category.{u_3, u_1} E] {K K' : Functor F.Groupoidal E} (hfib : asFunctorFrom_fib K = asFunctorFrom_fib K') (hhom : ∀ {c c' : C} (f : c ⟶ c'), asFunctorFrom_hom K f ≍ asFunctorFrom_hom K' f) : K = K'

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

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

Equations

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

theorem CategoryTheory.Functor.Groupoidal.map_obj_objMk {C : Type u} [Category.{v, u} C] {F G : Functor C Grpd} {α : F ⟶ G} (xb : C) (xf : ↑(F.obj xb)) : (map α).obj (objMk xb xf) = objMk xb ((α.app xb).obj xf)

theorem CategoryTheory.Functor.Groupoidal.map_id_eq {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} : map (CategoryStruct.id F) = Functor.id ↑(Cat.of F.Groupoidal)

theorem CategoryTheory.Functor.Groupoidal.map_forget {C : Type u} [Category.{v, u} C] {F G : Functor C Grpd} (α : F ⟶ G) : (map α).comp forget = forget

@[simp]

theorem CategoryTheory.Functor.Groupoidal.map_obj_base {C : Type u} [Category.{v, u} C] {F G : Functor C Grpd} {α : F ⟶ G} (X : F.Groupoidal) : ((map α).obj X).base = X.base

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.Groupoidal.map_map_base {C : Type u} [Category.{v, u} C] {F G : Functor C Grpd} {α : F ⟶ G} {X Y : F.Groupoidal} (f : X ⟶ Y) : Hom.base ((map α).map f) = Hom.base f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.map_map_fiber {C : Type u} [Category.{v, u} C] {F G : Functor C Grpd} {α : F ⟶ G} {X Y : F.Groupoidal} (f : X ⟶ Y) : Hom.fiber ((map α).map f) = CategoryStruct.comp (eqToHom ⋯) ((α.app Y.base).map (Hom.fiber f))

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

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.Groupoidal.pre_obj_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) (G : Functor D C) (x : (G.comp F).Groupoidal) : ((pre F G).obj x).base = G.obj x.base

@[simp]

theorem CategoryTheory.Functor.Groupoidal.pre_obj_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) (G : Functor D C) (x : (G.comp F).Groupoidal) : ((pre F G).obj x).fiber = x.fiber

@[simp]

theorem CategoryTheory.Functor.Groupoidal.pre_map_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) (G : Functor D C) {x y : (G.comp F).Groupoidal} (f : x ⟶ y) : Hom.base ((pre F G).map f) = G.map (Hom.base f)

@[simp]

theorem CategoryTheory.Functor.Groupoidal.pre_map_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) (G : Functor D C) {x y : (G.comp F).Groupoidal} (f : x ⟶ y) : Hom.fiber ((pre F G).map f) = Hom.fiber f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.pre_id {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) : pre F (Functor.id C) = Functor.id ((Functor.id C).comp F).Groupoidal

def CategoryTheory.Functor.Groupoidal.preNatIso {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) : pre F G ≅ (map (whiskerRight α.hom F)).comp (pre F H)

An natural isomorphism between functors G ≅ H induces a natural isomorphism between the canonical morphism pre F G and pre F H, up to composition with ∫(G ⋙ F) ⥤ ∫(H ⋙ F).

Equations

• CategoryTheory.Functor.Groupoidal.preNatIso F α = CategoryTheory.Functor.Grothendieck.preNatIso (F.comp CategoryTheory.Grpd.forgetToCat) α

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

Given an equivalence of categories G, preInv _ G is the (weak) inverse of the pre _ G.functor.

Equations

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

theorem CategoryTheory.Functor.Groupoidal.pre_comp_map {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (G : Functor D C) {H : Functor C Grpd} (α : F ⟶ H) : (pre F G).comp (map α) = (map (G.whiskerLeft α)).comp (pre H G)

theorem CategoryTheory.Functor.Groupoidal.pre_comp_map_assoc {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (G : Functor D C) {H : Functor C Grpd} (α : F ⟶ H) {E : Type u_1} [Category.{u_2, u_1} E] (K : Functor H.Groupoidal E) : (pre F G).comp ((map α).comp K) = (map (G.whiskerLeft α)).comp ((pre H G).comp K)

@[simp]

theorem CategoryTheory.Functor.Groupoidal.pre_comp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) {E : Type u_1} [Category.{u_2, u_1} E] (G : Functor D C) (H : Functor E D) : pre F (H.comp G) = (pre (G.comp F) H).comp (pre F G)

theorem CategoryTheory.Functor.Groupoidal.pre_comp_forget {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (α : Functor D C) (A : Functor C Grpd) : (pre A α).comp forget = forget.comp α

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ι_comp_pre {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) {D : Type u_1} [Category.{u_2, u_1} D] (G : Functor D C) (x : D) : (ι (G.comp F) x).comp (pre F G) = ι F (G.obj x)

theorem CategoryTheory.Functor.Groupoidal.comp_forget_naturality {Γ : Type u_1} [Category.{u_4, u_1} Γ] {F G : Functor Γ Grpd} {α : F ⟶ G} {X Y : Γ} (f : X ⟶ Y) : CategoryStruct.comp ((F.comp Grpd.forgetToCat).map f) (Grpd.forgetToCat.map (α.app Y)) = CategoryStruct.comp (Grpd.forgetToCat.map (α.app X)) ((G.comp Grpd.forgetToCat).map f)

theorem CategoryTheory.Functor.Groupoidal.map_map_eqToHom {Γ : Type u_1} [Category.{u_4, u_1} Γ] {F G : Functor Γ Grpd} {α : F ⟶ G} {X Y : F.Groupoidal} (f : X ⟶ Y) : ((G.comp Grpd.forgetToCat).map (Hom.base f)).obj ((map α).obj X).fiber = (α.app Y.base).obj (((F.comp Grpd.forgetToCat).map (Hom.base f)).obj X.fiber)

@[simp]

theorem CategoryTheory.Functor.Groupoidal.eqToHom_comp_fiber {C : Type u} [Category.{v, u} C] {A : Functor C Grpd} {p q r : A.Groupoidal} (h : p = q) {f : q ⟶ r} : Hom.fiber (CategoryStruct.comp (eqToHom h) f) = CategoryStruct.comp (eqToHom ⋯) (Hom.fiber f)

theorem CategoryTheory.Functor.Groupoidal.congr {C : Type u} [Category.{v, u} C] {F : Functor C Grpd} {X Y : F.Groupoidal} {f g : X ⟶ Y} (h : f = g) : Hom.fiber f = CategoryStruct.comp (eqToHom ⋯) (Hom.fiber g)

theorem CategoryTheory.Functor.Groupoidal.map_comp_eq {C : Type u} [Category.{v, u} C] (F : Functor C Grpd) {G H : Functor C Grpd} (α : F ⟶ G) (β : G ⟶ H) : map (CategoryStruct.comp α β) = (map α).comp (map β)

theorem CategoryTheory.Functor.Groupoidal.preNatIso_congr {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} (h : α = β) : preNatIso F α = preNatIso F β ≪≫ eqToIso ⋯

@[simp]

theorem CategoryTheory.Functor.Groupoidal.preNatIso_eqToIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) {G H : Functor D C} {h : G = H} : preNatIso F (eqToIso h) = eqToIso ⋯

theorem CategoryTheory.Functor.Groupoidal.preNatIso_comp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Grpd) {G1 G2 G3 : Functor D C} (α : G1 ≅ G2) (β : G2 ≅ G3) : preNatIso F (α ≪≫ β) = preNatIso F α ≪≫ (map (whiskerRight α.hom F)).isoWhiskerLeft (preNatIso F β) ≪≫ eqToIso ⋯

theorem CategoryTheory.Functor.Groupoidal.map_eqToHom_base {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {G1 G2 : A.Groupoidal} (eq : G1 = G2) : A.map (Hom.base (eqToHom eq)) = eqToHom ⋯

def CategoryTheory.Functor.Groupoidal.ιNatIso {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {X Y : Γ} (f : X ⟶ Y) : ι A X ≅ Functor.comp (A.map f) (ι A Y)

Every morphism f : X ⟶ Y in the base category induces a natural transformation from the fiber inclusion ι F X to the composition F.map f ⋙ ι F Y.

Equations

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

theorem CategoryTheory.Functor.Groupoidal.ιNatIso_hom {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {x y : Γ} (f : x ⟶ y) : (ιNatIso A f).hom = ιNatTrans f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.ιNatIso_id {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) (x : Γ) : ιNatIso A (CategoryStruct.id x) = eqToIso ⋯

theorem CategoryTheory.Functor.Groupoidal.ιNatIso_comp {Γ : Type u} [Groupoid Γ] (A : Functor Γ Grpd) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : ιNatIso A (CategoryStruct.comp f g) = ιNatIso A f ≪≫ isoWhiskerLeft (A.map f) (ιNatIso A g) ≪≫ eqToIso ⋯

theorem CategoryTheory.Functor.Groupoidal.functorTo_map_id_aux {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (x : D) : ((A.comp F).map (CategoryStruct.id x)).obj (fibObj x) = fibObj x

theorem CategoryTheory.Functor.Groupoidal.functorTo_map_comp_aux {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) {x y z : D} (f : x ⟶ y) (g : y ⟶ z) : ((A.comp F).map (CategoryStruct.comp f g)).obj (fibObj x) = (F.map (A.map g)).obj (((A.comp F).map f).obj (fibObj x))

def CategoryTheory.Functor.Groupoidal.functorTo {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) : Functor D F.Groupoidal

To define a functor into Grothendieck F we can make use of an existing functor into the base.

Equations

• CategoryTheory.Functor.Groupoidal.functorTo A fibObj fibMap map_id map_comp = CategoryTheory.Functor.Grothendieck.functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorTo_obj_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) (x : D) : ((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).obj x).base = A.obj x

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorTo_obj_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) (x : D) : ((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).obj x).fiber = fibObj x

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorTo_map_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) {x y : D} (f : x ⟶ y) : Hom.base ((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).map f) = A.map f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorTo_map_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} (A : Functor D C) (fibObj : (x : D) → ↑((A.comp F).obj x)) (fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))) {x y : D} (f : x ⟶ y) : Hom.fiber ((functorTo A fibObj (fun {x y : D} => fibMap) map_id ⋯).map f) = fibMap f

@[simp]

theorem CategoryTheory.Functor.Groupoidal.functorTo_forget {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Grpd} {A : Functor D C} {fibObj : (x : D) → ↑((A.comp F).obj x)} {fibMap : {x y : D} → (f : x ⟶ y) → ((A.comp F).map f).obj (fibObj x) ⟶ fibObj y} {map_id : ∀ (x : D), fibMap (CategoryStruct.id x) = eqToHom ⋯} {map_comp : ∀ {x y z : D} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map (A.map g)).map (fibMap f)) (fibMap g))} : (functorTo A fibObj fibMap map_id ⋯).comp (Grothendieck.forget (F.comp Grpd.forgetToCat)) = A

theorem CategoryTheory.Functor.Groupoidal.eqToHom_eq_homOf_map {Γ : Type u_1} [Groupoid Γ] {F G : Functor Γ Grpd} (h : F = G) : eqToHom ⋯ = Grpd.homOf (map (eqToHom h))

theorem CategoryTheory.Functor.Groupoidal.map_eqToHom_heq_id_dom {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A A' : Functor Γ Grpd} (h : A = A') : map (eqToHom h) ≍ Functor.id A.Groupoidal

theorem CategoryTheory.Functor.Groupoidal.map_eqToHom_heq_id_cod {Γ : Type u_1} [Category.{u_2, u_1} Γ] {A A' : Functor Γ Grpd} (h : A = A') : map (eqToHom h) ≍ Functor.id A'.Groupoidal

theorem CategoryTheory.Functor.Groupoidal.map_eqToHom_comp_heq {Γ : Type u_1} {D : Type u_2} [Category.{u_3, u_1} Γ] [Category.{u_4, u_2} D] {A A' : Functor Γ Grpd} (h : A = A') (F : Functor A'.Groupoidal D) : (map (eqToHom h)).comp F ≍ F

theorem CategoryTheory.Functor.Groupoidal.comp_map_eqToHom_heq {Γ : Type u_1} {D : Type u_2} [Category.{u_3, u_1} Γ] [Category.{u_4, u_2} D] {A A' : Functor Γ Grpd} (h : A = A') (F : Functor D A.Groupoidal) : F.comp (map (eqToHom h)) ≍ F

theorem CategoryTheory.Functor.Groupoidal.pre_congr_functor {Γ : Type u_1} {Δ : Type u_2} [Category.{u_3, u_1} Γ] [Category.{u_4, u_2} Δ] (σ : Functor Δ Γ) {F G : Functor Γ Grpd} (h : F = G) : (map (eqToHom ⋯)).comp ((pre F σ).comp (map (eqToHom h))) = pre G σ