reflectsSmallestFilteredColimits_of_reflectsFilteredColimits

English

Reflecting filtered colimits at any universe implies reflecting at the smallest universe.

Русский

Отражение фильтрованных колимитов в любой вселенной влечёт отражение в самой маленькой вселенной.

LaTeX

$$$reflectsSmallestFilteredColimitsOfRef...(F)$$$

Lean4

/-- Reflecting filtered colimits at any universe implies reflecting filtered colimits at universe `0`.
-/
theorem reflectsSmallestFilteredColimits_of_reflectsFilteredColimits (F : C ⥤ D)
    [ReflectsFilteredColimitsOfSize.{w', w} F] : ReflectsFilteredColimitsOfSize.{0, 0} F :=
  reflectsFilteredColimitsOfSize_shrink F

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