preservesLimit_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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