coconeOfCoconeFiberwiseColimit — Mathlib

Lean4
/-- 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.ι (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 }
Похожие утверждения