preservesLimitsOfSize_rightOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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