isColimitCoconeFiberwiseColimitOfCocone

Lean4
/-- If `c` is a colimit cocone on `G : Grothendieck 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 <| natTransIntoForgetCompFiberwiseColimit 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,
        natTransIntoForgetCompFiberwiseColimit_app, whiskerLeft_app]
      simp only [coconeFiberwiseColimitOfCocone_pt, Functor.const_obj_obj, coconeFiberwiseColimitOfCocone_ι_app] at this
      simp [← this]
Похожие утверждения