preservesLimit_op — Mathlib

English

If F preserves colimits of K.leftOp, then the opposite functor F.op preserves limits of K; i.e., PreservesLimit K F.op.

Русский

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

LaTeX

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

Lean4

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

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