Commit 2020-05-27 13:41 c812ebeb

View on Github →

feat(category_theory/abelian): abelian categories (#2817) ~~Depends on #2779.~~ Closes #2178. I will give instances for AddCommGroup and Module, but since this PR is large already, I'll wait until the next PR with that.

Estimated changes

Modified docs/references.bib

Created src/category_theory/abelian/basic.lean

added def category_theory.abelian.biproduct_to_pushout_is_cokernel.biproduct_to_pushout

added def category_theory.abelian.biproduct_to_pushout_is_cokernel.biproduct_to_pushout_cofork

added def category_theory.abelian.biproduct_to_pushout_is_cokernel.is_colimit_biproduct_to_pushout

added def category_theory.abelian.coimage_iso_image

added def category_theory.abelian.coimage_strong_epi_mono_factorisation

added def category_theory.abelian.epi_is_cokernel_of_kernel

added theorem category_theory.abelian.full_image_factorisation

added def category_theory.abelian.has_pullbacks

added def category_theory.abelian.has_pushouts

added theorem category_theory.abelian.image_eq_image

added def category_theory.abelian.image_strong_epi_mono_factorisation

added def category_theory.abelian.is_iso_of_mono_of_epi

added def category_theory.abelian.mono_is_kernel_of_cokernel

added def category_theory.abelian.pullback_to_biproduct_is_kernel.is_limit_pullback_to_biproduct

added def category_theory.abelian.pullback_to_biproduct_is_kernel.pullback_to_biproduct

added def category_theory.abelian.pullback_to_biproduct_is_kernel.pullback_to_biproduct_fork

added def category_theory.abelian.strong_epi_of_epi

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

added theorem category_theory.limits.biprod.hom_ext'

added theorem category_theory.limits.biprod.hom_ext

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

added theorem category_theory.limits.cofork.π_eq_app_one

added theorem category_theory.limits.fork.ι_eq_app_zero

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

added def category_theory.is_iso_of_mono_of_strong_epi

deleted def category_theory.mono_strong_epi_is_iso

Modified src/category_theory/preadditive.lean

modified theorem category_theory.preadditive.comp_neg

modified theorem category_theory.preadditive.comp_sub

modified theorem category_theory.preadditive.neg_comp

modified theorem category_theory.preadditive.neg_comp_neg

modified theorem category_theory.preadditive.sub_comp