preservesLimitsOfShape_of_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `F.unop : C ⥤ D` preserves colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits
of shape `J`. -/
theorem preservesLimitsOfShape_of_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesColimitsOfShape Jᵒᵖ F.unop] :
    PreservesLimitsOfShape J F where preservesLimit {K} := preservesLimit_of_unop K F

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