preservesColimitsOfSize_of_unop — Mathlib

English

Let F: C → D be a functor. If the unop of F preserves limits, then F, viewed as a functor Cᵒᵖ → Dᵒᵖ, preserves colimits.

Русский

Пусть F: C → D — функтор. Если F^{unop} сохраняет пределы, то F: C^{op} → D^{op} сохраняет колимиты.

LaTeX

$$$\operatorname{PreservesLimits}(F^{\mathrm{unop}}) \Rightarrow \operatorname{PreservesColimits}(F)$$$

Lean4

/-- If `F.unop : C ⥤ D` preserves limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits. -/
theorem preservesColimitsOfSize_of_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesLimitsOfSize.{w, w'} F.unop] :
    PreservesColimitsOfSize.{w, w'} F where preservesColimitsOfShape {_} _ := preservesColimitsOfShape_of_unop _ _

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