Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Module docstring

{"# (Co)limits on the (strict) Grothendieck Construction

Shows that if a functor G : Grothendieck F ⥤ H, with F : C ⥤ Cat, has a colimit, and every fiber of G has a colimit, then so does the fiberwise colimit functor C ⥤ H.
Vice versa, if a each fiber of G has a colimit and the fiberwise colimit functor has a colimit, then G has a colimit.
Shows that colimits of functors on the Grothendieck construction are colimits of \"fibered colimits\", i.e. of applying the colimit to each fiber of the functor.
Derives HasColimitsOfShape (Grothendieck F) H with F : C ⥤ Cat from the presence of colimits on each fiber shape F.obj X and on the base category C.

CategoryTheory.Limits.hasColimit_ι_comp theorem

: ∀ X, HasColimit (Grothendieck.ι F X ⋙ G)

Full source

@[local instance]
lemma hasColimit_ι_comp : ∀ X, HasColimit (Grothendieck.ιGrothendieck.ι F X ⋙ G) :=
  fun X => hasColimit_of_iso (F := F.map (𝟙 _) ⋙ Grothendieck.ι F X ⋙ G) <|
    (Functor.leftUnitor (Grothendieck.ι F X ⋙ G)).symm ≪≫
    (isoWhiskerRight (eqToIso (F.map_id X).symm) (Grothendieck.ι F X ⋙ G))

Existence of Colimits for Compositions with Fiber Inclusions in the Grothendieck Construction

Informal description

For every object $X$ in the base category $C$, the composition of the inclusion functor $\iota_F(X) \colon F(X) \to \int F$ with the functor $G \colon \int F \to H$ has a colimit in the category $H$.

CategoryTheory.Limits.fiberwiseColimit definition

: C ⥤ H

Full source

/-- A functor taking a colimit on each fiber of a functor `G : Grothendieck F ⥤ H`. -/
@[simps]
def fiberwiseColimit : C ⥤ H where
  obj X := colimit (Grothendieck.ιGrothendieck.ι F X ⋙ G)
  map {X Y} f := colimMapcolimMap (whiskerRight (Grothendieck.ιNatTrans f) G ≫
    (Functor.associator _ _ _).hom) ≫ colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f)
  map_id X := by
    ext d
    simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]
    conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ιGrothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).obj d) (by simp)]
    rw [← eqToHom_map G (by simp), Grothendieck.eqToHom_eq]
    rfl
  map_comp {X Y Z} f g := by
    ext d
    simp only [Functor.comp_obj, Grothendieck.ιNatTrans, ι_colimMap_assoc, NatTrans.comp_app,
      whiskerRight_app, Functor.associator_hom_app, Category.comp_id, colimit.ι_pre, Category.assoc,
      colimit.ι_pre_assoc]
    rw [← Category.assoc, ← G.map_comp]
    conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ιGrothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).obj d) (by simp)]
    rw [← Category.assoc, ← eqToHom_map G (by simp), ← G.map_comp, Grothendieck.eqToHom_eq]
    congr 2
    fapply Grothendieck.ext
    · simp only [Cat.comp_obj, eqToHom_refl, Category.assoc, Grothendieck.comp_base,
        Category.comp_id]
    · simp only [Grothendieck.ι_obj, Cat.comp_obj, eqToHom_refl, Cat.id_obj,
        Grothendieck.comp_base, Category.comp_id, Grothendieck.comp_fiber, Functor.map_id]
      conv_rhs => enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z))]
      conv_rhs => rw [eqToHom_trans, eqToHom_trans]

Fiberwise colimit functor

Informal description

Given a functor $F \colon C \to \mathrm{Cat}$ and a functor $G \colon \int F \to H$ from the Grothendieck construction of $F$ to a category $H$, the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$ is defined by: - On objects: For each $X \in C$, $\mathrm{fiberwiseColimit}\, G\, X$ is the colimit of the composition $ι_F(X) \circ G \colon F(X) \to H$, where $ι_F(X) \colon F(X) \to \int F$ is the inclusion functor of the fiber. - On morphisms: For each $f \colon X \to Y$ in $C$, the induced morphism is constructed using the universal property of colimits applied to the natural transformation induced by $f$ between the fiber inclusion functors.

CategoryTheory.Limits.fiberwiseColim definition

[∀ c, HasColimitsOfShape (F.obj c) H] : (Grothendieck F ⥤ H) ⥤ (C ⥤ H)

Full source

/-- Similar to `colimit` and `colim`, taking fiberwise colimits is a functor
`(Grothendieck F ⥤ H) ⥤ (C ⥤ H)` between functor categories. -/
@[simps]
def fiberwiseColim [∀ c, HasColimitsOfShape (F.obj c) H] : (Grothendieck F ⥤ H) ⥤ (C ⥤ H) where
  obj G := fiberwiseColimit G
  map α :=
    { app := fun c => colim.map (whiskerLeft _ α)
      naturality := fun c₁ c₂ f => by apply colimit.hom_ext; simp }
  map_id G := by ext; simp; apply Functor.map_id colim
  map_comp α β := by ext; simp; apply Functor.map_comp colim

Fiberwise colimit functor for the Grothendieck construction

Informal description

Given a functor $F \colon C \to \mathrm{Cat}$ and a category $H$ such that for every object $c$ in $C$, the fiber category $F(c)$ has colimits in $H$, the fiberwise colimit functor $\mathrm{fiberwiseColim}$ is a functor from the category of functors $\int F \to H$ to the category of functors $C \to H$. For a functor $G \colon \int F \to H$, the functor $\mathrm{fiberwiseColim}\, G \colon C \to H$ is defined by: - On objects: For each $c \in C$, $(\mathrm{fiberwiseColim}\, G)(c)$ is the colimit of the composition $ι_F(c) \circ G \colon F(c) \to H$, where $ι_F(c) \colon F(c) \to \int F$ is the inclusion functor of the fiber. - On morphisms: For each morphism $f \colon c \to c'$ in $C$, the induced morphism is given by the universal property of colimits applied to the natural transformation induced by $f$. For a natural transformation $\alpha \colon G \Rightarrow G'$ between functors $G, G' \colon \int F \to H$, the induced natural transformation $\mathrm{fiberwiseColim}\, \alpha \colon \mathrm{fiberwiseColim}\, G \Rightarrow \mathrm{fiberwiseColim}\, G'$ has components at each $c \in C$ given by the colimit of the whiskered transformation $\mathrm{whiskerLeft}\, ι_F(c)\, \alpha \colon ι_F(c) \circ G \Rightarrow ι_F(c) \circ G'$.

CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit definition

: G ⟶ Grothendieck.forget F ⋙ fiberwiseColimit G

Full source

/-- Every functor `G : Grothendieck F ⥤ H` induces a natural transformation from `G` to the
composition of the forgetful functor on `Grothendieck F` with the fiberwise colimit on `G`. -/
@[simps]
def natTransIntoForgetCompFiberwiseColimit :
    G ⟶ Grothendieck.forget F ⋙ fiberwiseColimit G where
  app X := colimit.ι (Grothendieck.ιGrothendieck.ι F X.base ⋙ G) X.fiber
  naturality _ _ f := by
    simp only [Functor.comp_obj, Grothendieck.forget_obj, fiberwiseColimit_obj, Functor.comp_map,
      Grothendieck.forget_map, fiberwiseColimit_map, ι_colimMap_assoc, Grothendieck.ι_obj,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]
    rw [← colimit.w (Grothendieck.ιGrothendieck.ι F _ ⋙ G) f.fiber]
    simp only [← Category.assoc, Functor.comp_obj, Functor.comp_map, ← G.map_comp]
    congr 2
    apply Grothendieck.ext <;> simp

Natural transformation from a functor to the composition of forgetful and fiberwise colimit functors

Informal description

For a functor $G \colon \int F \to H$ from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$, there is a natural transformation from $G$ to the composition of the forgetful functor $\mathrm{Grothendieck.forget}\, F \colon \int F \to C$ with the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$. At each object $X = (c, x)$ in $\int F$, the component of this natural transformation is given by the coprojection morphism $\iota_x \colon G(X) \to \mathrm{colimit}\, (\iota_F(c) \circ G)$, where $\iota_F(c) \colon F(c) \to \int F$ is the inclusion functor of the fiber over $c$.

CategoryTheory.Limits.coconeFiberwiseColimitOfCocone definition

(c : Cocone G) : Cocone (fiberwiseColimit G)

Full source

/-- A cocone on a functor `G : Grothendieck F ⥤ H` induces a cocone on the fiberwise colimit
on `G`. -/
@[simps]
def coconeFiberwiseColimitOfCocone (c : Cocone G) : Cocone (fiberwiseColimit G) where
  pt := c.pt
  ι := { app := fun X => colimit.desc _ (c.whisker (Grothendieck.ι F X)),
         naturality := fun _ _ f => by dsimp; ext; simp }

Cocone over fiberwise colimit induced by a cocone over the Grothendieck construction

Informal description

Given a cocone $c$ over a functor $G \colon \int F \to H$ from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$, the cocone $\mathrm{coconeFiberwiseColimitOfCocone}\, c$ is a cocone over the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$ with the same apex as $c$. The cocone's natural transformation is constructed by applying the universal property of colimits to the whiskered cocone $c.\mathrm{whisker}\, (\iota_F(X))$ for each object $X$ in $C$, where $\iota_F(X) \colon F(X) \to \int F$ is the inclusion functor of the fiber.

CategoryTheory.Limits.isColimitCoconeFiberwiseColimitOfCocone definition

{c : Cocone G} (hc : IsColimit c) : IsColimit (coconeFiberwiseColimitOfCocone c)

Full source

/-- If `c` is a colimit cocone on `G : Grockendieck F ⥤ H`, then the induced cocone on the
fiberwise colimit on `G` is a colimit cocone, too. -/
def isColimitCoconeFiberwiseColimitOfCocone {c : Cocone G} (hc : IsColimit c) :
    IsColimit (coconeFiberwiseColimitOfCocone c) where
  desc s := hc.desc <| Cocone.mk s.pt <| natTransIntoForgetCompFiberwiseColimitnatTransIntoForgetCompFiberwiseColimit G ≫
    whiskerLeft (Grothendieck.forget F) s.ι
  fac s c := by dsimp; ext; simp
  uniq s m hm := hc.hom_ext fun X => by
    have := hm X.base
    simp only [Functor.const_obj_obj, IsColimit.fac, NatTrans.comp_app, Functor.comp_obj,
      Grothendieck.forget_obj, fiberwiseColim_obj, natTransIntoForgetCompFiberwiseColimit_app,
      whiskerLeft_app]
    simp only [fiberwiseColim_obj, coconeFiberwiseColimitOfCocone_pt, Functor.const_obj_obj,
      coconeFiberwiseColimitOfCocone_ι_app] at this
    simp [← this]

Fiberwise colimit cocone induced by a colimit cocone is a colimit

Informal description

Given a cocone $c$ over a functor $G \colon \int F \to H$ from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$, if $c$ is a colimit cocone, then the induced cocone $\mathrm{coconeFiberwiseColimitOfCocone}\, c$ over the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$ is also a colimit cocone.

CategoryTheory.Limits.hasColimit_fiberwiseColimit theorem

[HasColimit G] : HasColimit (fiberwiseColimit G)

Full source

lemma hasColimit_fiberwiseColimit [HasColimit G] : HasColimit (fiberwiseColimit G) where
  exists_colimit := ⟨⟨_, isColimitCoconeFiberwiseColimitOfCocone (colimit.isColimit _)⟩⟩

Existence of Colimit for Fiberwise Colimit Functor

Informal description

If a functor $G \colon \int F \to H$ from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$ has a colimit, then the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$ also has a colimit.

CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit definition

(c : Cocone (fiberwiseColimit G)) : Cocone G

Full source

/-- For a functor `G : Grothendieck F ⥤ H`, every cocone over `fiberwiseColimit G` induces a
cocone over `G` itself. -/
@[simps]
def coconeOfCoconeFiberwiseColimit (c : Cocone (fiberwiseColimit G)) : Cocone G where
  pt := c.pt
  ι := { app := fun X => colimit.ιcolimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ c.ι.app X.base
         naturality := fun {X Y} ⟨f, g⟩ => by
          simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id]
          rw [← Category.assoc, ← c.w f, ← Category.assoc]
          simp only [fiberwiseColimit_obj, fiberwiseColimit_map, ι_colimMap_assoc,
            Functor.comp_obj, Grothendieck.ι_obj, NatTrans.comp_app, whiskerRight_app,
            Functor.associator_hom_app, Category.comp_id, colimit.ι_pre]
          rw [← colimit.w _ g, ← Category.assoc, Functor.comp_map, ← G.map_comp]
          congr <;> simp }

Cocone over `G` induced by a cocone over its fiberwise colimit

Informal description

Given a cocone `c` over the fiberwise colimit functor `fiberwiseColimit G`, this constructs a cocone over the original functor `G : Grothendieck F ⥤ H`. The apex of the new cocone is the same as that of `c`, and the coprojections are defined by composing the coprojections from the fiberwise colimits with the coprojections from `c`.

CategoryTheory.Limits.isColimitCoconeOfFiberwiseCocone definition

{c : Cocone (fiberwiseColimit G)} (hc : IsColimit c) : IsColimit (coconeOfCoconeFiberwiseColimit c)

Full source

/-- If a cocone `c` over a functor `G : Grothendieck F ⥤ H` is a colimit, than the induced cocone
`coconeOfFiberwiseCocone G c` -/
def isColimitCoconeOfFiberwiseCocone {c : Cocone (fiberwiseColimit G)} (hc : IsColimit c) :
    IsColimit (coconeOfCoconeFiberwiseColimit c) where
  desc s := hc.desc <| Cocone.mk s.pt <|
    { app := fun X => colimit.desc (Grothendieck.ι F X ⋙ G) (s.whisker _) }
  uniq s m hm := hc.hom_ext <| fun X => by
    simp only [fiberwiseColimit_obj, Functor.const_obj_obj, fiberwiseColimit_map,
      Functor.const_obj_map, Cocone.whisker_pt, id_eq, Functor.comp_obj, Cocone.whisker_ι,
      whiskerLeft_app, NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app,
      whiskerLeft_twice, eq_mpr_eq_cast, IsColimit.fac]
    simp only [coconeOfCoconeFiberwiseColimit_pt, Functor.const_obj_obj,
      coconeOfCoconeFiberwiseColimit_ι_app, Category.assoc] at hm
    ext d
    simp [hm ⟨X, d⟩]

Colimit cocone induced from fiberwise colimit cocone

Informal description

Given a cocone `c` over the fiberwise colimit functor `fiberwiseColimit G` and a proof `hc` that `c` is a colimit cocone, the induced cocone `coconeOfCoconeFiberwiseColimit c` over the original functor `G : Grothendieck F ⥤ H` is also a colimit cocone. In other words, if the fiberwise colimit functor has a colimit, then the original functor `G` also has a colimit, and the colimit cocone for `G` is constructed from the colimit cocone of the fiberwise colimit functor.

CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit theorem

: HasColimit G

Full source

/-- We can infer that a functor `G : Grothendieck F ⥤ H`, with `F : C ⥤ Cat`, has a colimit from
the fact that each of its fibers has a colimit and that these fiberwise colimits, as a functor
`C ⥤ H` have a colimit. -/
@[local instance]
lemma hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit : HasColimit G where
  exists_colimit := ⟨⟨_, isColimitCoconeOfFiberwiseCocone (colimit.isColimit _)⟩⟩

Existence of Colimit for Functor on Grothendieck Construction via Fiberwise Colimits

Informal description

Given a functor $G \colon \int F \to H$ from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$, if the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$ has a colimit and each fiber of $G$ has a colimit, then $G$ itself has a colimit.

CategoryTheory.Limits.colimitFiberwiseColimitIso definition

: colimit (fiberwiseColimit G) ≅ colimit G

Full source

/-- For every functor `G` on the Grothendieck construction `Grothendieck F`, if `G` has a colimit
and every fiber of `G` has a colimit, then taking this colimit is isomorphic to first taking the
fiberwise colimit and then the colimit of the resulting functor. -/
def colimitFiberwiseColimitIso : colimitcolimit (fiberwiseColimit G) ≅ colimit G :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (fiberwiseColimit G))
    (isColimitCoconeFiberwiseColimitOfCocone (colimit.isColimit _))

Isomorphism between colimit of fiberwise colimit and colimit on Grothendieck construction

Informal description

Given a functor $G \colon \int F \to H$ from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$, if $G$ has a colimit and every fiber of $G$ has a colimit, then the colimit of the fiberwise colimit functor $\mathrm{fiberwiseColimit}\, G \colon C \to H$ is isomorphic to the colimit of $G$ itself. More precisely, there is a canonical isomorphism \[ \mathrm{colimit}\, (\mathrm{fiberwiseColimit}\, G) \cong \mathrm{colimit}\, G \] between these two colimit objects in $H$.

CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom theorem

 (X : C) (d : F.obj X) :
  colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫ (colimitFiberwiseColimitIso G).hom =
    colimit.ι G ⟨X, d⟩

Full source

@[reassoc (attr := simp)]
lemma ι_colimitFiberwiseColimitIso_hom (X : C) (d : F.obj X) :
    colimit.ιcolimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫
      (colimitFiberwiseColimitIso G).hom = colimit.ι G ⟨X, d⟩ := by
  simp [colimitFiberwiseColimitIso]

Compatibility of Fiberwise and Global Colimit Coprojections via Isomorphism

Informal description

For any object $X$ in the base category $C$ and any object $d$ in the fiber category $F(X)$, the composition of the following morphisms: 1. The coprojection $\iota_d : G(X,d) \to \text{colimit}(G \circ \iota_F(X))$ from the fiberwise colimit, 2. The coprojection $\iota_X : \text{colimit}(G \circ \iota_F(X)) \to \text{colimit}(\text{fiberwiseColimit}\, G)$ from the base colimit, and 3. The isomorphism $\text{colimitFiberwiseColimitIso}\, G : \text{colimit}(\text{fiberwiseColimit}\, G) \to \text{colimit}\, G$, equals the coprojection $\iota_{(X,d)} : G(X,d) \to \text{colimit}\, G$ from the global colimit. In symbols: $$ \iota_d \circ \iota_X \circ (\text{colimitFiberwiseColimitIso}\, G).\text{hom} = \iota_{(X,d)}. $$

CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv theorem

 (X : Grothendieck F) :
  colimit.ι G X ≫ (colimitFiberwiseColimitIso G).inv =
    colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base

Full source

@[reassoc (attr := simp)]
lemma ι_colimitFiberwiseColimitIso_inv (X : Grothendieck F) :
    colimit.ιcolimit.ι G X ≫ (colimitFiberwiseColimitIso G).inv =
    colimit.ιcolimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫
      colimit.ι (fiberwiseColimit G) X.base := by
  rw [Iso.comp_inv_eq]
  simp

Compatibility of Global and Fiberwise Colimit Coprojections via Isomorphism Inverse

Informal description

For any object $X = (X_{\mathrm{base}}, X_{\mathrm{fiber}})$ in the Grothendieck construction $\int F$, the composition of the following morphisms: 1. The coprojection $\iota_X : G(X) \to \mathrm{colimit}\, G$ from the global colimit, and 2. The inverse of the isomorphism $\mathrm{colimitFiberwiseColimitIso}\, G : \mathrm{colimit}\, (\mathrm{fiberwiseColimit}\, G) \cong \mathrm{colimit}\, G$, equals the composition of: 1. The coprojection $\iota_{X_{\mathrm{fiber}}} : G(X_{\mathrm{base}}, X_{\mathrm{fiber}}) \to \mathrm{colimit}\, (G \circ \iota_F(X_{\mathrm{base}}))$ from the fiberwise colimit, and 2. The coprojection $\iota_{X_{\mathrm{base}}} : \mathrm{colimit}\, (G \circ \iota_F(X_{\mathrm{base}})) \to \mathrm{colimit}\, (\mathrm{fiberwiseColimit}\, G)$ from the base colimit. In symbols: $$ \iota_X \circ (\mathrm{colimitFiberwiseColimitIso}\, G)^{-1} = \iota_{X_{\mathrm{fiber}}} \circ \iota_{X_{\mathrm{base}}}. $$

CategoryTheory.Limits.hasColimitsOfShape_grothendieck theorem

[∀ X, HasColimitsOfShape (F.obj X) H] [HasColimitsOfShape C H] : HasColimitsOfShape (Grothendieck F) H

Full source

@[instance]
theorem hasColimitsOfShape_grothendieck [∀ X, HasColimitsOfShape (F.obj X) H]
    [HasColimitsOfShape C H] : HasColimitsOfShape (Grothendieck F) H where
  has_colimit _ := hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit _

Existence of Colimits in Grothendieck Construction via Fiberwise and Base Colimits

Informal description

Let $F \colon C \to \mathrm{Cat}$ be a functor and $H$ a category. If for every object $X$ in $C$, the category $H$ has colimits of shape $F(X)$, and $H$ has colimits of shape $C$, then $H$ has colimits of shape $\int F$ (the Grothendieck construction of $F$).

CategoryTheory.Limits.fiberwiseColimCompColimIso definition

: fiberwiseColim F H ⋙ colim ≅ colim

Full source

/-- The isomorphism `colimitFiberwiseColimitIso` induces an isomorphism of functors `(J ⥤ C) ⥤ C`
between `fiberwiseColim F H ⋙ colim` and `colim`. -/
@[simps!]
def fiberwiseColimCompColimIso : fiberwiseColimfiberwiseColim F H ⋙ colimfiberwiseColim F H ⋙ colim ≅ colim :=
  NatIso.ofComponents (fun G => colimitFiberwiseColimitIso G)
    fun _ => by (iterate 2 apply colimit.hom_ext; intro); simp

Isomorphism between fiberwise colimit composition and colimit functor

Informal description

The natural isomorphism between the composition of the fiberwise colimit functor with the colimit functor and the colimit functor itself, for functors from the Grothendieck construction of $F \colon C \to \mathrm{Cat}$ to a category $H$. More precisely, there is a canonical isomorphism \[ \mathrm{fiberwiseColim}\, F\, H \circ \mathrm{colim} \cong \mathrm{colim} \] between these two functors from the category of functors $\int F \to H$ to $H$.

CategoryTheory.Limits.fiberwiseColimCompEvaluationIso definition

(c : C) : fiberwiseColim F H ⋙ (evaluation C H).obj c ≅ (whiskeringLeft _ _ _).obj (Grothendieck.ι F c) ⋙ colim

Full source

/-- Composing `fiberwiseColim F H` with the evaluation functor `(evaluation C H).obj c` is
naturally isomorphic to precomposing the Grothendieck inclusion `Grothendieck.ι` to `colim`. -/
@[simps!]
def fiberwiseColimCompEvaluationIso (c : C) :
    fiberwiseColimfiberwiseColim F H ⋙ (evaluation C H).obj cfiberwiseColim F H ⋙ (evaluation C H).obj c ≅
      (whiskeringLeft _ _ _).obj (Grothendieck.ι F c) ⋙ colim :=
  Iso.refl _

Natural isomorphism between fiberwise colimit and evaluation composition

Informal description

For a functor $F \colon C \to \mathrm{Cat}$ and a category $H$ with appropriate colimits, the composition of the fiberwise colimit functor $\mathrm{fiberwiseColim}\, F\, H$ with the evaluation functor at an object $c \in C$ is naturally isomorphic to the composition of the left whiskering of the Grothendieck inclusion functor $\iota_F(c) \colon F(c) \to \int F$ with the colimit functor $\mathrm{colim} \colon (\int F \to H) \to H$. In other words, for any $c \in C$, there is a natural isomorphism: $$(\mathrm{fiberwiseColim}\, F\, H) \circ \mathrm{eval}_c \cong \mathrm{whiskerLeft}\, \iota_F(c) \circ \mathrm{colim}$$ where $\mathrm{eval}_c$ is the evaluation functor at $c$ and $\mathrm{whiskerLeft}$ denotes left whiskering of natural transformations.