preservesLimitsOfShape_of_eval — Mathlib

English

A functor D ⥤ HC preserves limits of shape J if, for every i, the composed functor D ⥤ HC ⥤ C with eval at i preserves limits 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 limits of shape } J \Rightarrow G\text{ preserves limits of shape } J$$$

Lean4

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

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