preservesProductsOfShape_of_preservesBiproductsOfShape

English

If epi(biproductComparison' F f) holds, then f preserves the biproduct.

Русский

Если epi(biproductComparison' F f) верно, тогда f сохраняет биопродукт.

LaTeX

$$$\mathrm{Epi}(\mathrm{biproductComparison}'\ F\ f) \Rightarrow \mathrm{PreservesBiproduct}\ f\ F$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite products. -/
theorem preservesProductsOfShape_of_preservesBiproductsOfShape [PreservesBiproductsOfShape J F] :
    PreservesLimitsOfShape (Discrete J) F where
  preservesLimit {_} := preservesLimit_of_iso_diagram _ Discrete.natIsoFunctor.symm

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