Commit 2023-10-27 14:12 c5fe4511

View on Github →

refactor: introduce the new homology API for homological complex and rename the old one (#7954) This PR renames definitions of the current homology API (adding a ' to homology, cycles, QuasiIso) so as to create space for the development of the new homology API of homological complexes: this PR also contains the new definition of HomologicalComplex.homology which involves the homology theory of short complexes.

Estimated changes

deleted theorem ChainComplex.mk_d_2_0
added theorem ChainComplex.mk_d_2_1
added def cycles'Functor
added theorem cycles'Map_arrow
added theorem cycles'Map_comp
added theorem cycles'Map_id
deleted def cyclesFunctor
deleted theorem cyclesMap_arrow
deleted theorem cyclesMap_comp
deleted theorem cyclesMap_id
added def homology'Functor
deleted def homologyFunctor
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 theorem homology'.π_map_apply
added def homology'
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 homologyOfZeroLeft
deleted def homologyOfZeroRight
deleted def homologyZeroZero
added theorem ModuleCat.cycles'_ext
deleted theorem ModuleCat.cycles_ext
deleted theorem ModuleCat.homology_ext'
deleted theorem ModuleCat.homology_ext
added def homology'Op
added def homology'Unop
deleted def homologyOp
deleted def homologyUnop
deleted theorem HomotopyEquiv.toQuasiIso
added theorem quasiIso'_of_comp_left
deleted theorem quasiIso_of_comp_left
deleted theorem quasiIso_of_comp_right
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_ι
added def homology'.ι
added def homology'.π'
added theorem homology'.π'_desc'
added theorem homology'.π'_eq_π
added theorem homology'.π'_map
added theorem homology'.π'_ι
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.π'_ι