preservesLimitsOfShape_of_discrete

English

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

Русский

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

LaTeX

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

Lean4

/-- If `F` preserves the limit of every `Discrete.functor f`, it preserves all limits of shape
`Discrete J`. -/
theorem preservesLimitsOfShape_of_discrete (F : C ⥤ D) [∀ (f : J → C), PreservesLimit (Discrete.functor f) F] :
    PreservesLimitsOfShape (Discrete J) F where
  preservesLimit := preservesLimit_of_iso_diagram F (Discrete.natIsoFunctor).symm

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