preservesFiniteProducts_leftOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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