preservesColimitsOfShape_rightOp — Mathlib

English

Let F: C^{op} → D be a functor between categories. If F preserves limits of shape J^{op}, then the induced functor F.rightOp: C → D^{op} preserves colimits of shape J.

Русский

Пусть F: C^{op} → D — функтор между категориями. Тогда, если F сохраняет пределы формы J^{op}, то соответствующий F.rightOp: C → D^{op} сохраняет колимиты формы J.

LaTeX

$$$\bigl( F: \mathcal{C}^{op} \to \mathcal{D} \text{ preserves limits of shape } J^{op} \bigr) \Rightarrow \bigl( F^{\mathrm{rightOp}}: \mathcal{C} \to \mathcal{D}^{op} \text{ preserves colimits of shape } J \bigr).$$$

Lean4

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

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