colimitCocone — Mathlib

Lean4
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
-/
@[simps]
def colimitCocone (F : J ⥤ PresheafedSpace.{_, _, v} C) : Cocone F
    where
  pt := colimit F
  ι :=
    { app := fun j =>
        { base := colimit.ι (F ⋙ PresheafedSpace.forget C) j
          c := limit.π _ (op j) }
      naturality := fun {j j'} f => by
        ext1
        · ext x
          exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x
        · ext ⟨U, hU⟩
          dsimp [-Presheaf.comp_app]
          rw [PresheafedSpace.id_c_app, map_id]
          erw [id_comp]
          rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app, eqToHom_app, ←
            congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op), NatTrans.comp_app,
            Functor.leftOp_map, pushforwardDiagramToColimit_map]
          simp }
Похожие утверждения