hasLimits_op_of_hasColimits — Mathlib

English

If C has colimits of size in a given size class, then C^op has limits of the same shape; this is formulated as HasLimitsOfSize in the opposite category.

Русский

Если C имеет колимиты заданного размера, то в C^op существуют пределы такой же формы; формулируется через HasLimitsOfSize в противоположной категории.

LaTeX

$$$$\\mathrm{HasLimitsOfSize}^{op}(J, C) \\iff \\mathrm{HasColimitsOfSize}(J, C^{op}).$$$$

Lean4

/-- If `C` has colimits, we can construct limits for `Cᵒᵖ`.
-/
instance hasLimits_op_of_hasColimits [HasColimitsOfSize.{v₂, u₂} C] : HasLimitsOfSize.{v₂, u₂} Cᵒᵖ :=
  ⟨fun _ => inferInstance⟩

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