preservesColimits_of_evaluation — Mathlib

English

If F: D ⥤ K ⥤ C preserves all colimits whenever it preserves them after composing with each evaluation ev_k, then F preserves all colimits.

Русский

Если F: D ⥤ K ⥤ C сохраняет все колимиты, когда она сохраняет их после композиции с каждой оценкой ev_k, то F сохраняет все колимиты.

LaTeX

$$$\\Big(\\forall k, \\operatorname{PreservesColimitsOfSize}(F \\circ ((\\mathrm{evaluation}\\; K\\; C).obj\\; k))\\Big) \\Rightarrow \\operatorname{PreservesColimitsOfSize} F.$$$

Lean4

/-- `F : D ⥤ K ⥤ C` preserves all colimits if it does for each `k : K`. -/
theorem preservesColimits_of_evaluation (F : D ⥤ K ⥤ C)
    (_ : ∀ k : K, PreservesColimitsOfSize.{w', w} (F ⋙ (evaluation K C).obj k)) : PreservesColimitsOfSize.{w', w} F :=
  ⟨fun {L} _ => preservesColimitsOfShape_of_evaluation F L fun _ => PreservesColimitsOfSize.preservesColimitsOfShape⟩

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