hasLimitsOfShape_op_of_hasColimitsOfShape

English

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

Русский

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

LaTeX

$$$$\\mathrm{HasLimitsOfShape}(J, C)^{op} \\text{ is realized by } \\mathrm{HasColimitsOfShape}(J^{op}, C^{op}).$$$$

Lean4

/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
-/
theorem hasLimitsOfShape_op_of_hasColimitsOfShape [HasColimitsOfShape Jᵒᵖ C] : HasLimitsOfShape J Cᵒᵖ :=
  { has_limit := fun F => hasLimit_of_hasColimit_leftOp F }

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