preservesColimit_leftOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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