preservesCofilteredLimitsOfSize_shrink

English

If a functor F preserves cofiltered limits of some large size, then it preserves cofiltered limits of smaller sizes as well.

Русский

Если функтор F сохраняет пределы когильтрованных диаграмм некоторого большого размера, то сохраняет пределы когильтрованных диаграмм меньших размеров.

LaTeX

$$$\Bigl(\exists w_2,w_2'\; \text{PreservesCofilteredLimitsOfSize}(F; \max w w_2, \max w' w_2')\Bigr) \Rightarrow \text{PreservesCofilteredLimitsOfSize}(F; w, w').$$$

Lean4

/-- `PreservesCofilteredLimitsOfSizeShrink.{w, w'} F` tries to obtain
`PreservesCofilteredLimitsOfSize.{w, w'} F` from some other `PreservesCofilteredLimitsOfSize F`.
-/
theorem preservesCofilteredLimitsOfSize_shrink (F : C ⥤ D) [PreservesCofilteredLimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesCofilteredLimitsOfSize.{w, w'} F :=
  preservesCofilteredLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

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