preservesColimit_of_unop — Mathlib

English

If F.unop preserves limits of K.op, then F leftOp preserves colimits of K, i.e., PreservesColimit K F.leftOp.

Русский

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

LaTeX

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

Lean4

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

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