preservesColimitsOfShape_of_discrete

English

Let F: C → D. If F preserves the colimit of every discrete diagram f: J → C, then F preserves all colimits of shape Discrete J.

Русский

Пусть F: C → D. Если F сохраняет колимит каждой дискретной диаграммы f: J → C, то F сохраняет все колимиты формы Discrete J.

LaTeX

$$$(\\forall f: J \\to C)\, PreservesColimit(Discrete.functor f, F) \\Rightarrow PreservesColimitsOfShape(Discrete J, F)$$$

Lean4

/-- If `F` preserves the colimit of every `Discrete.functor f`, it preserves all colimits of shape
`Discrete J`. -/
theorem preservesColimitsOfShape_of_discrete (F : C ⥤ D) [∀ (f : J → C), PreservesColimit (Discrete.functor f) F] :
    PreservesColimitsOfShape (Discrete J) F where
  preservesColimit := preservesColimit_of_iso_diagram F (Discrete.natIsoFunctor).symm

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