hasColimits_op_of_hasLimits — Mathlib

English

If C has limits, then the opposite category C^op has colimits.

Русский

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

LaTeX

$$$\\text{HasColimits } C^{\\mathrm{op}}$ from $\\text{HasLimits } C$$$

Lean4

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

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