preservesFiniteCoproducts_rightOp

English

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

Русский

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

LaTeX

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

Lean4

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

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