preservesFiniteCoproducts_unop — Mathlib

English

If F preserves finite products, then F.unop preserves finite coproducts.

Русский

Если F сохраняет конечные произведения, то F.unop сохраняет конечные копродукты.

LaTeX

$$$\operatorname{PreservesFiniteProducts}(F) \Rightarrow \operatorname{PreservesFiniteCoproducts}(F^{unop})$$$

Lean4

/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite products, then `F.unop : C ⥤ D` preserves finite
coproducts. -/
theorem preservesFiniteCoproducts_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesFiniteProducts F] : PreservesFiniteCoproducts F.unop
    where
  preserves
    _ := by
    apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_unop
    exact preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

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