evaluationJointlyReflectsColimits

Lean4
/-- A cocone in the category `PresheafOfModules R` is colimit if it is so after the application
of the functors `evaluation R X` for all `X`. -/
def evaluationJointlyReflectsColimits (c : Cocone F) (hc : ∀ (X : Cᵒᵖ), IsColimit ((evaluation R X).mapCocone c)) :
    IsColimit c
    where
  desc
    s :=
    { app := fun X => (hc X).desc ((evaluation R X).mapCocone s)
      naturality := fun {X Y} f ↦
        (hc X).hom_ext
          (fun j ↦ by
            rw [(hc X).fac_assoc ((evaluation R X).mapCocone s) j]
            have h₁ := (c.ι.app j).naturality f
            have h₂ := (hc Y).fac ((evaluation R Y).mapCocone s)
            dsimp at h₁ h₂ ⊢
            simp only [← reassoc_of% h₁, ← Functor.map_comp, h₂, Hom.naturality]) }
  fac s
    j := by
    ext1 X
    exact (hc X).fac ((evaluation R X).mapCocone s) j
  uniq s m
    hm := by
    ext1 X
    apply (hc X).uniq ((evaluation R X).mapCocone s)
    intro j
    dsimp
    rw [← hm]
    rfl
Похожие утверждения