preservesSmallestColimits_of_preservesColimits

English

Preserving colimits at all sizes implies preserving the smallest colimits (0,0).

Русский

Сохранение колимитов при любых размерах влечет сохранение самых малых колимитов (0,0).

LaTeX

$$$ \\mathrm{PreservesColimitsOfSize}^{(v_3,u_3)}(F) \\Rightarrow \\mathrm{PreservesColimitsOfSize}^{(0,0)}(F). $$$

Lean4

/-- Preserving colimits at any universe implies preserving colimits at universe `0`. -/
theorem preservesSmallestColimits_of_preservesColimits (F : C ⥤ D) [PreservesColimitsOfSize.{v₃, u₃} F] :
    PreservesColimitsOfSize.{0, 0} F :=
  preservesColimitsOfSize_shrink F

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