English
Let F: D ⥤ K ⥤ C and G: J ⥤ D. If for every k ∈ K, the induced functor preserves the colimit of G, i.e. PreservesColimit G (F ⋙ ev_k), then PreservesColimit G F.
Русский
Пусть F: D ⥤ K ⥤ C и G: J ⥤ D. Если для каждого k ∈ K соответствующий композиционный функтор сохраняет колимит диаграммы G, то F сохраняет колимит диаграммы G.
LaTeX
$$$\\forall k, \\operatorname{PreservesColimit} G \\big( F \\;\\circ\\; ((\\mathrm{evaluation}\\; K\\; C).\\mathrm{obj}\\; k) \\big) \\Rightarrow \\operatorname{PreservesColimit} G \\; F.$$$
Lean4
/-- `F : D ⥤ K ⥤ C` preserves the colimit of some `G : J ⥤ D` if it does for each `k : K`. -/
theorem preservesColimit_of_evaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
(H : ∀ k, PreservesColimit G (F ⋙ (evaluation K C).obj k)) : PreservesColimit G F :=
⟨fun {c} hc =>
⟨by
apply evaluationJointlyReflectsColimits
intro X
haveI := H X
change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)
exact isColimitOfPreserves _ hc⟩⟩
