preservesColimitsOfSize_leftOp — Mathlib

English

If F.leftOp: C^{op} ⥤ D preserves limits of shape J^{op}, then F: C ⥤ D^{op} preserves colimits of shape J.

Русский

Если F.leftOp: C^{op} ⥤ D сохраняет пределы формы J^{op}, тогда F: C ⥤ D^{op} сохраняет колимиты формы J.

LaTeX

$$$(F: C \to D^{op}) [PreservesLimitsOfShape(J^{op}, F.leftOp)] \Rightarrow (F: C^{op} \to D) [PreservesColimitsOfShape(J, F)].$$$

Lean4

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

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