Commit 2021-04-03 03:51 b630c513

View on Github →

feat(category_theory/kernels): mild generalization of lemma (#6930) Relaxes some is_iso assumptions to mono or epi. I've also added some TODOs about related generalizations and instances which could be provided. I don't intend to get to them immediately.

Estimated changes

Modified src/algebra/homology/image_to_kernel_map.lean

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

added def category_theory.limits.cokernel_epi_comp

deleted def category_theory.limits.cokernel_is_iso_comp

deleted theorem category_theory.limits.cokernel_π_comp_cokernel_comp_is_iso_hom

deleted theorem category_theory.limits.cokernel_π_comp_cokernel_comp_is_iso_inv

deleted theorem category_theory.limits.cokernel_π_comp_cokernel_is_iso_comp_hom

deleted theorem category_theory.limits.cokernel_π_comp_cokernel_is_iso_comp_inv

deleted def category_theory.limits.kernel_comp_is_iso

deleted theorem category_theory.limits.kernel_comp_is_iso_hom_comp_kernel_ι

deleted theorem category_theory.limits.kernel_comp_is_iso_inv_comp_kernel_ι

added def category_theory.limits.kernel_comp_mono

deleted theorem category_theory.limits.kernel_is_iso_comp_hom_comp_kernel_ι

deleted theorem category_theory.limits.kernel_is_iso_comp_inv_comp_kernel_ι