preservesFiniteCoproducts_leftOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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