preservesFiniteLimits_of_op — Mathlib

English

Let C and D be categories and F: C → D. If the opposite of F preserves finite colimits, then F preserves finite limits.

Русский

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

LaTeX

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

Lean4

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

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