Commit 2024-07-09 18:31 eb669117

View on Github →

refactor: removing the old homology API (#14569) The now redundant old homology API is removed. (It was already mostly unused.) The only slightly non-trivial changes are in CategoryTheory.Abelian.Exact where some definitions and proofs have been refactored. The proof that the category of abelian groups satisfies Grothendieck's AB5 axiom had to be moved to a separate file Algebra.Category.Grp.AB5.

Estimated changes

deleted structure CategoryTheory.Exact
deleted theorem homology'.condition
deleted def homology'.congr
deleted def homology'.desc
deleted theorem homology'.ext
deleted def homology'.map
deleted def homology'.mapIso
deleted theorem homology'.map_comp
deleted theorem homology'.map_desc
deleted theorem homology'.map_id
deleted def homology'.π
deleted theorem homology'.π_desc
deleted theorem homology'.π_map
deleted theorem homology'.π_map_apply
deleted def homology'
deleted def homology'OfZeroLeft
deleted def homology'ZeroZero
deleted theorem homology'.condition_ι
deleted theorem homology'.condition_π'
deleted def homology'.desc'
deleted theorem homology'.hom_from_ext
deleted theorem homology'.hom_to_ext
deleted def homology'.lift
deleted theorem homology'.lift_ι
deleted theorem homology'.map_ι
deleted def homology'.ι
deleted def homology'.π'
deleted theorem homology'.π'_desc'
deleted theorem homology'.π'_eq_π
deleted theorem homology'.π'_map
deleted theorem homology'.π'_ι