preservesFiniteColimits_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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