preservesFiniteLimits_of_leftOp — Mathlib

English

Let F: C → D^{op}. If the leftOp of F preserves finite colimits, then F preserves finite limits.

Русский

Пусть F: C → D^{op}. Если F.leftOp сохраняет конечные колимиты, то F сохраняет конечные пределы.

LaTeX

$$$\operatorname{PreservesFiniteColimits}(F.leftOp) \Rightarrow \operatorname{PreservesFiniteLimits}(F)$$$

Lean4

/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves finite colimits, then `F : C ⥤ Dᵒᵖ` preserves finite
limits. -/
theorem preservesFiniteLimits_of_leftOp (F : C ⥤ Dᵒᵖ) [PreservesFiniteColimits F.leftOp] : PreservesFiniteLimits F where
  preservesFiniteLimits J _ _ := preservesLimitsOfShape_of_leftOp J F

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