hasColimitsOfShape_op_of_hasLimitsOfShape

English

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

Русский

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

LaTeX

$$$\\text{HasColimitsOfShape }J\\, C^{\\mathrm{op}}\\quad\\text{whence}\\quad \\text{HasColimitsOfShape }J\\, C^{\\mathrm{op}}$$$

Lean4

/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
-/
instance hasColimitsOfShape_op_of_hasLimitsOfShape [HasLimitsOfShape Jᵒᵖ C] : HasColimitsOfShape J Cᵒᵖ where
  has_colimit F := hasColimit_of_hasLimit_leftOp F

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