isColimitCoconeOfFiberwiseCocone — Mathlib

Lean4

/-- 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, IsColimit.fac]
      simp only [coconeOfCoconeFiberwiseColimit_pt, Functor.const_obj_obj, coconeOfCoconeFiberwiseColimit_ι_app,
        Category.assoc] at hm
      ext d
      simp [hm ⟨X, d⟩]

Похожие утверждения