Commit 2023-05-13 13:28 95ba50fc

View on Github →

feat: port/CategoryTheory.Abelian.Homology (#3882)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/Homology.lean

added theorem homology.condition_ι

added theorem homology.condition_π'

added def homology.desc'

added theorem homology.hom_from_ext

added theorem homology.hom_to_ext

added def homology.lift

added theorem homology.lift_ι

added theorem homology.map_eq_desc'_lift_left

added theorem homology.map_eq_desc'_lift_right

added theorem homology.map_eq_lift_desc'_left

added theorem homology.map_eq_lift_desc'_right

added theorem homology.map_ι

added def homology.ι

added def homology.π'

added theorem homology.π'_desc'

added theorem homology.π'_eq_π

added theorem homology.π'_map

added theorem homology.π'_ι

added def homologyIsoKernelDesc