Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-16 03:40 9d1ab69f

View on Github →

refactor(category_theory/images): improvements (#7198) Some improvements to the images API, from homology2.

Estimated changes

Modified src/algebra/homology/image_to_kernel_map.lean

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

added def category_theory.limits.image.comp_iso

added theorem category_theory.limits.image.comp_iso_hom_comp_image_ι

added theorem category_theory.limits.image.comp_iso_inv_comp_image_ι

deleted def category_theory.limits.image.post_comp_is_iso

deleted theorem category_theory.limits.image.post_comp_is_iso_hom_comp_image_ι

deleted theorem category_theory.limits.image.post_comp_is_iso_inv_comp_image_ι

added def category_theory.limits.mono_factorisation.comp_mono

added def category_theory.limits.mono_factorisation.iso_comp

added def category_theory.limits.mono_factorisation.of_comp_iso

added def category_theory.limits.mono_factorisation.of_iso_comp