preservesBinaryCoproducts_of_preservesBinaryBiproducts

English

If F preserves binary biproducts, it preserves binary coproducts; i.e., structural preservation of sums is maintained under F.

Русский

Если F сохраняет бинарные би-производные, тогда F сохраняет бинарные копроизведения; т.е. сумма сохраняется через F.

LaTeX

$$$$\\PreservesColimitsOfShape(\\mathrm{Discrete WalkingPair}) F \\Rightarrow \\PreservesBinaryCoproducts F.$$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary coproducts. -/
theorem preservesBinaryCoproducts_of_preservesBinaryBiproducts [PreservesBinaryBiproducts F] :
    PreservesColimitsOfShape (Discrete WalkingPair) F where
  preservesColimit {_} := preservesColimit_of_iso_diagram _ (diagramIsoPair _).symm

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