Commit 2023-09-05 16:59 1f3d3886

View on Github →

feat: the shift on the category of cochain complexes (#6626) This PR constructs the shift on the category of cochain complexes.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

added theorem HomologicalComplex.XIsoOfEq_hom_naturality

added theorem HomologicalComplex.XIsoOfEq_inv_naturality

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

added theorem CochainComplex.XIsoOfEq_shift

added def CochainComplex.shiftFunctor

added def CochainComplex.shiftFunctorAdd'

added theorem CochainComplex.shiftFunctorAdd'_eq

added theorem CochainComplex.shiftFunctorAdd'_hom_app_f'

added theorem CochainComplex.shiftFunctorAdd'_inv_app_f'

added theorem CochainComplex.shiftFunctorAdd_eq

added theorem CochainComplex.shiftFunctorAdd_hom_app_f

added theorem CochainComplex.shiftFunctorAdd_inv_app_f

added theorem CochainComplex.shiftFunctorComm_hom_app_f

added def CochainComplex.shiftFunctorObjXIso

added def CochainComplex.shiftFunctorZero'

added theorem CochainComplex.shiftFunctorZero_eq

added theorem CochainComplex.shiftFunctorZero_hom_app_f

added theorem CochainComplex.shiftFunctorZero_inv_app_f

added theorem CochainComplex.shiftFunctor_map_f'

added theorem CochainComplex.shiftFunctor_obj_d'