Commit 2024-04-18 09:26 a6439961

View on Github →

feat(Algebra/Homology): compatibilities of homology and shifts (#11782) This PR studies the compatibilities of homology and shifts. This results into ShiftSequence instances for the homology functor in the CochainComplex and HomotopyCategory namespaces.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean

added def CochainComplex.shiftEval

Created Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

added theorem CochainComplex.ShiftSequence.shiftIso_hom_app

added theorem CochainComplex.ShiftSequence.shiftIso_inv_app

added def CochainComplex.shiftShortComplexFunctor'

added theorem CochainComplex.shiftShortComplexFunctorIso_add'_hom_app

added theorem CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app

added theorem HomotopyCategory.homologyShiftIso_hom_app

Modified Mathlib/CategoryTheory/Preadditive/Basic.lean

modified theorem CategoryTheory.Preadditive.smul_iso_hom

modified theorem CategoryTheory.Preadditive.smul_iso_inv