preservesColimitsOfSize_of_univLE

English

A functor preserving larger colimits also preserves smaller colimits.

Русский

Функтор, сохраняющий более крупные колимиты, сохраняет и меньшие.

LaTeX

$$$ \\mathrm{PreservesColimitsOfSize}^{(w,w')} F \\Rightarrow \\mathrm{PreservesColimitsOfSize}^{(w,w_2)} F. $$$

Lean4

/-- A functor preserving larger colimits also preserves smaller colimits. -/
theorem preservesColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [PreservesColimitsOfSize.{w', w₂'} F] : PreservesColimitsOfSize.{w, w₂} F where
  preservesColimitsOfShape
    {J} := preservesColimitsOfShape_of_equiv ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

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