preservesLimitsOfSize_of_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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