preservesColimitsOfShape_of_eval — Mathlib

English

A functor D ⥤ HC preserves colimits of shape J if, for every i, the composed functor D ⥤ HC ⥤ C with eval at i preserves colimits of shape J.

Русский

Функтор D ⥤ HC сохраняет колимиты формы J, если для каждого i композиция D ⥤ HC ⥤ C с eval_i сохраняет колимиты формы J.

LaTeX

$$$\forall i,\ \bigl(G\circ \mathrm{eval}_{C,c,i}\bigr)\text{ preserves colimits of shape } J \Rightarrow G\text{ preserves colimits of shape } J$$$

Lean4

/-- A functor `D ⥤ HomologicalComplex C c` preserves colimits of shape `J`
if for any `i`, `G ⋙ eval C c i` does. -/
theorem preservesColimitsOfShape_of_eval {D : Type*} [Category D] (G : D ⥤ HomologicalComplex C c)
    (_ : ∀ (i : ι), PreservesColimitsOfShape J (G ⋙ eval C c i)) : PreservesColimitsOfShape J G :=
  ⟨fun {_} => ⟨fun hs ↦ ⟨isColimitOfEval _ _ (fun i => isColimitOfPreserves (G ⋙ eval C c i) hs)⟩⟩⟩

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