Commit 2020-05-13 10:27 506a71f9

View on Github →

feat(category_theory): preadditive categories (#2663) As discussed, here is the pedestrian definition of preadditive categories. Hopefully, it is not here to stay, but it will allow me to start PRing abelian categories.

Estimated changes

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

Created src/algebra/category/Group/preadditive.lean

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

Modified src/algebra/category/Module/basic.lean

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

added theorem category_theory.limits.cofork.π_of_π

added theorem category_theory.limits.fork.ι_of_ι

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

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

deleted theorem category_theory.limits.zero_of_comp_epi

modified theorem category_theory.limits.zero_of_comp_mono

added theorem category_theory.limits.zero_of_epi_comp

Created src/category_theory/preadditive.lean

added theorem category_theory.preadditive.comp_neg

added theorem category_theory.preadditive.comp_sub

added theorem category_theory.preadditive.epi_iff_cancel_zero

added theorem category_theory.preadditive.epi_of_cancel_zero

added def category_theory.preadditive.has_coequalizers_of_has_cokernels

added def category_theory.preadditive.has_colimit_parallel_pair

added def category_theory.preadditive.has_equalizers_of_has_kernels

added def category_theory.preadditive.has_limit_parallel_pair

added def category_theory.preadditive.left_comp

added theorem category_theory.preadditive.mono_iff_cancel_zero

added theorem category_theory.preadditive.mono_of_cancel_zero

added theorem category_theory.preadditive.neg_comp

added theorem category_theory.preadditive.neg_comp_neg

added def category_theory.preadditive.right_comp

added theorem category_theory.preadditive.sub_comp