has_filtered_colimits_op_of_has_cofiltered_limits

English

If C^op has cofiltered limits of a given size, then C^op has filtered colimits of that size.

Русский

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

LaTeX

$$$[HasCofilteredLimitsOfSize\\; C] \\Rightarrow [HasFilteredColimitsOfSize\\; C^{\\mathrm{op}}]$$$

Lean4

instance has_filtered_colimits_op_of_has_cofiltered_limits [HasCofilteredLimitsOfSize.{v₂, u₂} C] :
    HasFilteredColimitsOfSize.{v₂, u₂} Cᵒᵖ where HasColimitsOfShape _ _ _ := inferInstance

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