preservesLimits_leftOp — Mathlib

English

If F: C → Dᵒᵖ preserves colimits, then F.leftOp: Cᵒᵖ → D preserves limits.

Русский

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

LaTeX

$$$\operatorname{PreservesColimits}(F) \Rightarrow \operatorname{PreservesLimits}(F^{\mathrm{leftOp}})$$$

Lean4

/-- If `F : C ⥤ Dᵒᵖ` preserves colimits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves limits. -/
theorem preservesLimits_leftOp (F : C ⥤ Dᵒᵖ) [PreservesColimits F] : PreservesLimits F.leftOp where
  preservesLimitsOfShape {_} _ := preservesLimitsOfShape_leftOp _ _

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