preservesColimit_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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