hasFilteredColimitsOfSize_of_univLE

English

If UnivLE bounds hold, cofiltered limits exist for the reduced universe indices.

Русский

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

LaTeX

$$$[UnivLE^{w,w_2}] [UnivLE^{w',w_2'}] [HasCofilteredLimitsOfSize^{w_2',w_2} C] \Rightarrow HasCofilteredLimitsOfSize^{w',w} C$$$

Lean4

theorem hasFilteredColimitsOfSize_of_univLE [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}]
    [HasFilteredColimitsOfSize.{w₂', w₂} C] : HasFilteredColimitsOfSize.{w', w} C where
  HasColimitsOfShape
    J :=
    haveI :=
      IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂'} J).trans <| Shrink.equivalence.{w₂} (ShrinkHoms.{w} J))
    hasColimitsOfShape_of_equivalence
      ((ShrinkHoms.equivalence.{w₂'} J).trans <| Shrink.equivalence.{w₂} (ShrinkHoms.{w} J)).symm

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