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 theorem AddCommGrp.exact_iff
deleted theorem ModuleCat.exact_iff
deleted structure CategoryTheory.Exact
deleted def boundariesFunctor
deleted def cycles'Functor
deleted theorem cycles'Map_arrow
deleted theorem cycles'Map_comp
deleted theorem cycles'Map_id
deleted def homology'Functor
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 ModuleCat.cycles'_ext
deleted theorem ModuleCat.homology'_ext'
deleted theorem ModuleCat.homology'_ext
deleted def homology'Op
deleted def homology'Unop
deleted theorem HomotopyEquiv.toQuasiIso'
deleted theorem quasiIso'_of_comp_left
deleted theorem quasiIso'_of_comp_right
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'.π'_ι