reflectsFilteredColimitsOfSize_of_univLE

English

A functor that reflects larger filtered colimits also reflects smaller filtered colimits in a controlled universe setting.

Русский

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

LaTeX

$$$ReflectsFilteredColimitsOfSize.{w, w'} F \\Rightarrow ReflectsFilteredColimitsOfSize.{0,0} F$$$

Lean4

/-- A functor reflecting larger filtered colimits also reflects smaller filtered colimits. -/
theorem reflectsFilteredColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [ReflectsFilteredColimitsOfSize.{w', w₂'} F] : ReflectsFilteredColimitsOfSize.{w, w₂} F where
  reflects_filtered_colimits J _
    _ := by
    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
    haveI := IsFiltered.of_equivalence e.symm
    exact reflectsColimitsOfShape_of_equiv e F

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