reflectsSmallestColimits_of_reflectsColimits

English

If colimits are reflected at every universe, then colimits are reflected at universe 0. In particular, ReflectsColimitsOfSize^{0,0} F holds whenever F reflects colimits of all sizes.

Русский

Если колимиты отражаются при любой вселенной, то и при вселенной 0 отражаются. Конкретно: ReflectsColimitsOfSize^{0,0} F.

LaTeX

$$$\\text{If } ReflectsColimitsOfSize F \\text{ holds for all sizes, then } ReflectsColimitsOfSize^{0,0}F.$$$

Lean4

/-- Reflecting colimits at any universe implies reflecting colimits at universe `0`. -/
theorem reflectsSmallestColimits_of_reflectsColimits (F : C ⥤ D) [ReflectsColimitsOfSize.{v₃, u₃} F] :
    ReflectsColimitsOfSize.{0, 0} F :=
  reflectsColimitsOfSize_shrink F

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