preservesCofilteredLimitsOfSize_of_univLE

English

A functor preserving larger cofiltered limits also preserves smaller cofiltered limits in universe LE.

Русский

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

LaTeX

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

Lean4

/-- A functor preserving larger cofiltered limits also preserves smaller cofiltered limits. -/
theorem preservesCofilteredLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [PreservesCofilteredLimitsOfSize.{w', w₂'} F] : PreservesCofilteredLimitsOfSize.{w, w₂} F where
  preserves_cofiltered_limits J _
    _ := by
    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
    haveI := IsCofiltered.of_equivalence e.symm
    exact preservesLimitsOfShape_of_equiv e F

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