Mathlib Changelog
v3
Changelog
About
Github
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