preservesFiniteColimits_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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