Commit 2025-02-02 19:39 83b6fa7e

View on Github →

feat(CategoryTheory): preservation of coimage-image comparisons (#21348)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Abelian/Images.lean

Modified Mathlib/CategoryTheory/Abelian/Transfer.lean

deleted def CategoryTheory.AbelianOfAdjunction.coimageIsoImage

deleted def CategoryTheory.AbelianOfAdjunction.coimageIsoImageAux

deleted theorem CategoryTheory.AbelianOfAdjunction.coimageIsoImage_hom

deleted def CategoryTheory.AbelianOfAdjunction.cokernelIso

Created Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean

added theorem CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom

added theorem CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv

added theorem CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison

added def CategoryTheory.Abelian.PreservesCoimage.iso

added theorem CategoryTheory.Abelian.PreservesCoimage.iso_hom_π

added theorem CategoryTheory.Abelian.PreservesCoimage.iso_inv_π

added def CategoryTheory.Abelian.PreservesCoimageImageComparison.iso

added theorem CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_hom

added theorem CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_inv

added def CategoryTheory.Abelian.PreservesImage.iso

added theorem CategoryTheory.Abelian.PreservesImage.iso_hom_ι

added theorem CategoryTheory.Abelian.PreservesImage.iso_inv_ι

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean

added theorem CategoryTheory.Limits.PreservesCokernel.π_iso_hom

added theorem CategoryTheory.Limits.PreservesKernel.iso_inv_ι