Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-22 06:26 749e39fe

View on Github →

feat(category_theory): preadditive binary biproducts (#2747) This PR introduces "preadditive binary biproducts", which correspond to the second definition of biproducts given in #2177.

Preadditive binary biproducts are binary biproducts.
In a preadditive category, a binary product is a preadditive binary biproduct.
This directly implies that AddCommGroup has preadditive binary biproducts. The existence of binary coproducts in AddCommGroup is then a consequence of abstract nonsense.

Estimated changes

Modified src/algebra/category/Group/biproducts.lean

Modified src/category_theory/limits/shapes/biproducts.lean

added theorem category_theory.limits.biprod.fst_add_snd

added theorem category_theory.limits.biprod.inl_add_inr

added theorem category_theory.limits.biprod.inl_fst

added theorem category_theory.limits.biprod.inl_snd

added theorem category_theory.limits.biprod.inr_fst

added theorem category_theory.limits.biprod.inr_snd

added theorem category_theory.limits.biprod.lift_desc

added theorem category_theory.limits.biprod.total

added def category_theory.limits.has_preadditive_binary_biproduct.of_has_colimit_pair

added def category_theory.limits.has_preadditive_binary_biproduct.of_has_limit_pair

added def category_theory.limits.has_preadditive_binary_biproducts_of_has_binary_coproducts

added def category_theory.limits.has_preadditive_binary_biproducts_of_has_binary_products