preservesCoproductsOfShape_of_preservesBiproductsOfShape

English

If a functor preserves coproducts for shape J, it preserves biproducts of shape J.

Русский

Если функтор сохраняет coproducts формы J, он сохраняет биопродукты формы J.

LaTeX

$$$[PreservesCoproductsOfShape J F] \Rightarrow [PreservesBiproductsOfShape J F]$$$

Lean4

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

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