preservesColimitsOfSize_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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