Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 10:15 313f4055

View on Github →

feat(category_theory/*): preserves biproducts implies additive (#12014)

Estimated changes

Created src/category_theory/limits/preserves/shapes/biproducts.lean

added def category_theory.functor.map_bicone

added def category_theory.functor.map_binary_bicone

added def category_theory.functor.map_biprod

added theorem category_theory.functor.map_biprod_hom

added theorem category_theory.functor.map_biprod_inv

added def category_theory.functor.map_biproduct

added theorem category_theory.functor.map_biproduct_hom

added theorem category_theory.functor.map_biproduct_inv

added theorem category_theory.limits.biprod.lift_map_biprod

added theorem category_theory.limits.biprod.map_biprod_hom_desc

added theorem category_theory.limits.biprod.map_biprod_inv_map_desc

added theorem category_theory.limits.biprod.map_lift_map_biprod

added theorem category_theory.limits.biproduct.map_biproduct_hom_desc

added theorem category_theory.limits.biproduct.map_biproduct_inv_map_desc

added theorem category_theory.limits.biproduct.map_lift_map_biprod

added def category_theory.limits.is_bilimit_of_preserves

added def category_theory.limits.is_binary_bilimit_of_preserves

added def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct

added def category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product

added def category_theory.limits.preserves_binary_biproduct_of_preserves_biproduct

added def category_theory.limits.preserves_binary_biproducts_of_preserves_binary_coproducts

added def category_theory.limits.preserves_binary_biproducts_of_preserves_binary_products

added def category_theory.limits.preserves_binary_biproducts_of_preserves_biproducts

added def category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct

added def category_theory.limits.preserves_binary_coproducts_of_preserves_binary_biproducts

added def category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct

added def category_theory.limits.preserves_binary_products_of_preserves_binary_biproducts

added def category_theory.limits.preserves_biproduct_of_preserves_coproduct

added def category_theory.limits.preserves_biproduct_of_preserves_product

added def category_theory.limits.preserves_biproducts_of_shape_of_preserves_coproducts_of_shape

added def category_theory.limits.preserves_biproducts_of_shape_of_preserves_products_of_shape

added def category_theory.limits.preserves_coproduct_of_preserves_biproduct

added def category_theory.limits.preserves_coproducts_of_shape_of_preserves_biproducts_of_shape

added def category_theory.limits.preserves_product_of_preserves_biproduct

added def category_theory.limits.preserves_products_of_shape_of_preserves_biproducts_of_shape

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

Modified src/category_theory/preadditive/Mat.lean

Modified src/category_theory/preadditive/additive_functor.lean

added theorem category_theory.functor.additive_of_preserves_binary_biproducts

deleted def category_theory.functor.map_biproduct