preservesColimitsOfSize_of_rightOp

English

If F.rightOp preserves limits, then F preserves colimits. In particular, PreservesColimitsOfSize F holds under the assumption PreservesLimitsOfSize F.rightOp.

Русский

Если F.rightOp сохраняет пределы, то F сохраняет колимиты. В частности, при предположении PreservesLimitsOfSize F.rightOp выполняется PreservesColimitsOfSize F.

LaTeX

$$$ [PreservesLimitsOfSize\!\{\\, w, w'\} F.rightOp] \Rightarrow \text{PreservesColimitsOfSize}\!\{w, w'\} F. $$$

Lean4

/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves limits, then `F : Cᵒᵖ ⥤ D` preserves colimits. -/
theorem preservesColimitsOfSize_of_rightOp (F : Cᵒᵖ ⥤ D) [PreservesLimitsOfSize.{w, w'} F.rightOp] :
    PreservesColimitsOfSize.{w, w'} F where preservesColimitsOfShape {_} _ := preservesColimitsOfShape_of_rightOp _ _

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