hasColimitsOfSizeOfUnivLE — Mathlib

English

If a category has colimits of a large size, then it also has colimits of a smaller size, provided universe level relations hold (via Shrink constructions).

Русский

Если категория обладает колимитами большего размера, она обладает колимитами меньшего размера при условии соблюдения отношений уровней вселенной (через конструкцию Shrink).

LaTeX

$$$ \\text{HasColimitsOfSize}^{\\text{small}} C \\Rightarrow \\text{HasColimitsOfSize}^{\\text{large}} C $$$

Lean4

/-- A category that has larger colimits also has smaller colimits. -/
theorem hasColimitsOfSizeOfUnivLE [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [HasColimitsOfSize.{v₁, u₁} C] :
    HasColimitsOfSize.{v₂, u₂} C where
  has_colimits_of_shape J
    {_} := hasColimitsOfShape_of_equivalence ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

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