preservesLimit_leftOp — Mathlib

English

If F : C ⥤ Dᵒᵖ preserves colimits of K.leftOp, then F.leftOp preserves limits of K.

Русский

Если F : C ⥤ Dᵒᵖ сохраняет колимиты K.leftOp, тогда F.leftOp сохраняет пределы K.

LaTeX

$$$\\operatorname{PreservesLimit} K\\ F^{\\mathrm{leftOp}}$$$

Lean4

/-- If `F : C ⥤ Dᵒᵖ` preserves colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D`
preserves limits of `K : J ⥤ Cᵒᵖ`. -/
theorem preservesLimit_leftOp (K : J ⥤ Cᵒᵖ) (F : C ⥤ Dᵒᵖ) [PreservesColimit K.leftOp F] : PreservesLimit K F.leftOp
    where preserves {_} hc := ⟨isLimitConeUnopOfCocone _ (isColimitOfPreserves F (isColimitCoconeLeftOpOfCone _ hc))⟩

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