preservesFiniteColimits_of_evaluation

English

Let F: C ⥤ D ⥤ E. If for every d ∈ D, F ∘ evaluation_d preserves finite colimits, then F preserves finite colimits.

Русский

Пусть F: C ⥤ D ⥤ E. Если для каждого d ∈ D отображение F ∘ evaluation_d сохраняет конечные колимиты, тогда F сохраняет конечные колимиты.

LaTeX

$$$\\operatorname{preservesFiniteColimits}\\left(F : C \\to D \\to E\\right) \\Rightarrow \\forall d, \\operatorname{preservesFiniteColimits}\\left(F \\circ (\\mathrm{evaluation}\\; D\\; E)_{\\!d}\\right)$$$

Lean4

/-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`. -/
theorem preservesFiniteColimits_of_evaluation {D : Type*} [Category D] {E : Type*} [Category E] (F : C ⥤ D ⥤ E)
    (h : ∀ d : D, PreservesFiniteColimits (F ⋙ (evaluation D E).obj d)) : PreservesFiniteColimits F :=
  ⟨fun J _ _ => preservesColimitsOfShape_of_evaluation F J fun k => (h k).preservesFiniteColimits _⟩

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