reflectsCofilteredLimitsOfSize_of_univLE

English

If a functor reflects cofiltered limits at larger universes, then it reflects them at smaller universes as well.

Русский

Если функтор отражает когильтрованные пределы в больших вселенных, то он отражает их и в меньших вселенных.

LaTeX

$$$\text{ReflectsCofilteredLimitsOfSize}(F; w, w')$ следует из предположений $UnivLE$$$

Lean4

/-- A functor reflecting larger cofiltered limits also reflects smaller cofiltered limits. -/
theorem reflectsCofilteredLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [ReflectsCofilteredLimitsOfSize.{w', w₂'} F] : ReflectsCofilteredLimitsOfSize.{w, w₂} F where
  reflects_cofiltered_limits J _
    _ := by
    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
    haveI := IsCofiltered.of_equivalence e.symm
    exact reflectsLimitsOfShape_of_equiv e F

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