Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 10:16 aa11589a

View on Github →

feat(algebra/homology, category_theory/abelian): expand API on exactness (#4256)

Estimated changes

Modified src/algebra/homology/exact.lean

deleted theorem category_theory.exact.w_assoc

added theorem category_theory.exact_comp_hom_inv_comp

added theorem category_theory.exact_comp_hom_inv_comp_iff

added theorem category_theory.exact_comp_mono

added theorem category_theory.exact_epi_comp

added theorem category_theory.exact_kernel

added theorem category_theory.exact_zero_left_of_mono

added theorem category_theory.kernel_ι_eq_zero_of_exact_zero_left

Modified src/algebra/homology/image_to_kernel_map.lean

added theorem category_theory.image_to_kernel_map_comp_hom_inv_comp

added theorem category_theory.image_to_kernel_map_comp_left

added theorem category_theory.image_to_kernel_map_comp_right

modified theorem category_theory.image_to_kernel_map_epi_of_epi_of_zero

modified theorem category_theory.image_to_kernel_map_epi_of_zero_of_mono

Modified src/category_theory/abelian/basic.lean

added theorem category_theory.abelian.epi_of_cokernel_π_eq_zero

added theorem category_theory.abelian.epi_of_zero_cokernel

added theorem category_theory.abelian.mono_of_kernel_ι_eq_zero

added theorem category_theory.abelian.mono_of_zero_kernel

Modified src/category_theory/abelian/exact.lean

added theorem category_theory.abelian.epi_iff_cokernel_π_eq_zero

added theorem category_theory.abelian.epi_iff_exact_zero_right

added theorem category_theory.abelian.exact_cokernel

added theorem category_theory.abelian.mono_iff_exact_zero_left

added theorem category_theory.abelian.mono_iff_kernel_ι_eq_zero

added theorem category_theory.abelian.tfae_epi

added theorem category_theory.abelian.tfae_mono

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

added def category_theory.limits.image.post_comp_is_iso

added theorem category_theory.limits.image.post_comp_is_iso_hom_comp_image_ι

added theorem category_theory.limits.image.post_comp_is_iso_inv_comp_image_ι

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