English
If F is a functor between preadditive categories that preserves zero morphisms and binary biproducts, then F preserves binary products; equivalently, for every pair X, Y in C the biproduct X ⊞ Y is sent to a product cone on F X and F Y, hence F(X ⊕ Y) ≅ F X ⊕ F Y.
Русский
Если F — функтор между предадитивными категориями, сохраняющий нулевые морфизмы и двоичные би-производные, то F сохраняет двоичные произведения; эквивалентно, для любых X, Y в C би-производство X ⊕ Y переходит в произведение для F X и F Y, то есть F(X ⊕ Y) ≅ F X ⊕ F Y.
LaTeX
$$$$\\text{If $F$ preserves zero morphisms and binary biproducts, then }F(X\\oplus Y) \\cong F X \\oplus F Y\\text{ for all }X,Y.$$$$
Lean4
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary products. -/
theorem preservesBinaryProduct_of_preservesBinaryBiproduct {X Y : C} [PreservesBinaryBiproduct X Y F] :
PreservesLimit (pair X Y) F where
preserves {c}
hc :=
⟨IsLimit.ofIsoLimit
((IsLimit.postcomposeInvEquiv (diagramIsoPair _) _).symm
(isBinaryBilimitOfPreserves F (binaryBiconeIsBilimitOfLimitConeOfIsLimit hc)).isLimit) <|
Cones.ext (by dsimp; rfl) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp⟩
