preservesLimit_rightOp — Mathlib

English

If F preserves colimits of K.leftOp, then F.rightOp preserves limits of K.

Русский

Если F сохраняет колимиты для K.leftOp, тогда F.rightOp сохраняет пределы для K.

LaTeX

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

Lean4

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

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