Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-26 23:54 caf6f192

View on Github →

refactor(category_theory/abelian): deduplicate definitions of (co)image (#12902) Previously we made two separate definitions of the abelian (co)image, as kernel (cokernel.π f) / cokernel (kernel.ι f), once for non_preadditive_abelian C and once for abelian C. This duplication wasn't really necessary, and this PR unifies them.

Estimated changes

Modified src/category_theory/abelian/basic.lean

modified def category_theory.abelian.coimage_iso_image'

modified def category_theory.abelian.coimage_iso_image

added def category_theory.abelian.coimage_strong_epi_mono_factorisation

deleted def category_theory.abelian.coimages.coimage_strong_epi_mono_factorisation

deleted theorem category_theory.abelian.coimages.comp_coimage_π_eq_zero

added theorem category_theory.abelian.comp_coimage_π_eq_zero

modified theorem category_theory.abelian.full_image_factorisation

modified def category_theory.abelian.image_iso_image

added def category_theory.abelian.image_strong_epi_mono_factorisation

added theorem category_theory.abelian.image_ι_comp_eq_zero

deleted def category_theory.abelian.images.image_strong_epi_mono_factorisation

deleted theorem category_theory.abelian.images.image_ι_comp_eq_zero

Modified src/category_theory/abelian/exact.lean

modified def category_theory.abelian.is_colimit_coimage

modified def category_theory.abelian.is_colimit_image

Created src/category_theory/abelian/images.lean

Modified src/category_theory/abelian/non_preadditive.lean

Modified src/category_theory/abelian/pseudoelements.lean