preservesBiproductsOfShape_of_preservesCoproductsOfShape

English

A dual statement: preserves biproducts implies preserves coproducts for shape J.

Русский

Двойная формулировка: сохранение биопродуктов влечет сохранение coproducts формы J.

LaTeX

$$$[PreservesBiproductsOfShape J F] \Rightarrow [PreservesColimitsOfShape (Discrete J) F]$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
preserves finite biproducts. -/
theorem preservesBiproductsOfShape_of_preservesCoproductsOfShape [PreservesColimitsOfShape (Discrete J) F] :
    PreservesBiproductsOfShape J F where preserves {_} := preservesBiproduct_of_preservesCoproduct F

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