Commit 2023-07-31 16:57 795a5ff1

View on Github →

feat: the short complexes attached to homological complexes (#6039) If K is an homological complex and i some degree, this PR defines the short complex K.sc i which is `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)``.

depends on: #6008

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

added def HomologicalComplex.XIsoOfEq

added theorem HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom

added theorem HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv

added theorem HomologicalComplex.XIsoOfEq_hom_comp_d

added theorem HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom

added theorem HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv

added theorem HomologicalComplex.XIsoOfEq_inv_comp_d

added theorem HomologicalComplex.XIsoOfEq_rfl

added theorem HomologicalComplex.d_comp_XIsoOfEq_hom

added theorem HomologicalComplex.d_comp_XIsoOfEq_inv

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

added def HomologicalComplex.shortComplexFunctor'