preservesFiniteColimits_rightOp — Mathlib

English

If F preserves finite limits, then F.rightOp preserves finite colimits.

Русский

Если F сохраняет конечные пределы, то F.rightOp сохраняет конечные колимиты.

LaTeX

$$$\operatorname{PreservesFiniteLimits}(F) \Rightarrow \operatorname{PreservesFiniteColimits}(F^{\mathrm{rightOp}})$$$

Lean4

/-- If `F : Cᵒᵖ ⥤ D` preserves finite limits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
colimits. -/
theorem preservesFiniteColimits_rightOp (F : Cᵒᵖ ⥤ D) [PreservesFiniteLimits F] : PreservesFiniteColimits F.rightOp
    where preservesFiniteColimits J _ _ := preservesColimitsOfShape_rightOp J F

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