preservesColimitsOfShape_unop — Mathlib

English

Let F: C^{op} → D^{op}. If F preserves limits of shape J^{op}, then the unop of F, denoted F.unop: C → D, preserves colimits of shape J.

Русский

Пусть F: C^{op} → D^{op}. Если F сохраняет пределы формы 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 : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` preserves colimits
of shape `J`. -/
theorem preservesColimitsOfShape_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesLimitsOfShape Jᵒᵖ F] : PreservesColimitsOfShape J F.unop
    where preservesColimit {K} := preservesColimit_unop K F

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