Commit 2023-04-17 21:32 53b35370

View on Github →

feat: port Algebra.Homology.ImageToKernel (#3459)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ImageToKernel.lean

added theorem factorThruImageSubobject_comp_imageToKernel

added theorem homology.comp_right_eq_comp_left

added theorem homology.condition

added def homology.congr

added def homology.desc

added theorem homology.ext

added def homology.map

added def homology.mapIso

added theorem homology.map_comp

added theorem homology.map_desc

added theorem homology.map_id

added def homology.π

added theorem homology.π_desc

added theorem homology.π_map

added def homology

added def homologyIsoCokernelImageToKernel'

added def homologyIsoCokernelLift

added def homologyOfZeroLeft

added def homologyOfZeroRight

added def homologyZeroZero

added theorem imageSubobjectIso_imageToKernel'

added theorem imageSubobjectMap_comp_imageToKernel

added def imageToKernel'

added theorem imageToKernel'_kernelSubobjectIso

added def imageToKernel

added theorem imageToKernel_arrow

added theorem imageToKernel_comp_hom_inv_comp

added theorem imageToKernel_comp_left

added theorem imageToKernel_comp_mono

added theorem imageToKernel_comp_right

added theorem imageToKernel_epi_comp

added theorem imageToKernel_zero_left

added theorem imageToKernel_zero_right

added theorem image_le_kernel

added theorem subobject_ofLE_as_imageToKernel

Modified Mathlib/CategoryTheory/Arrow.lean

added theorem CategoryTheory.Arrow.comp_left

added theorem CategoryTheory.Arrow.comp_right

added theorem CategoryTheory.Arrow.hom_ext