preservesFilteredColimitsOfSize_of_univLE

English

A functor preserving larger filtered colimits also preserves filtered colimits for smaller sizes (universes).

Русский

Функтор, сохраняющий более крупные фильтрованные колимиты, также сохраняет фильтрованные колимиты для меньших размеров (вселенных).

LaTeX

$$$PreservesFilteredColimitsOfSize.{w, w'} F \\Rightarrow PreservesFilteredColimitsOfSize.{w, w'} F$$$

Lean4

/-- A functor preserving larger filtered colimits also preserves smaller filtered colimits. -/
theorem preservesFilteredColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [PreservesFilteredColimitsOfSize.{w', w₂'} F] : PreservesFilteredColimitsOfSize.{w, w₂} F where
  preserves_filtered_colimits J _
    _ := by
    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
    haveI := IsFiltered.of_equivalence e.symm
    exact preservesColimitsOfShape_of_equiv e F

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