Commit 2023-11-24 11:47 b112cb6b

View on Github →

feat: the homology functor on the homotopy category for the new API (#8595)

Estimated changes

Modified Mathlib/Algebra/Homology/Homotopy.lean

added def HomologicalComplex.homotopyEquivalences

added theorem Homotopy.homologyMap_eq

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/Algebra/Homology/QuasiIso.lean

added def HomologicalComplex.qis

added theorem HomologicalComplex.qis_iff

added theorem homotopyEquivalences_subset_qis

Modified Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

added theorem HomologicalComplex.homologyMap_add

added theorem HomologicalComplex.homologyMap_neg

added theorem HomologicalComplex.homologyMap_sub

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

added theorem CategoryTheory.Functor.additive_of_comp_faithful

added theorem CategoryTheory.Functor.additive_of_full_essSurj_comp

added theorem CategoryTheory.Functor.additive_of_iso

Modified Mathlib/CategoryTheory/Quotient.lean