preservesColimit_of_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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