preservesColimit_rightOp — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{PreservesLimit} K F$$$

Lean4

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

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