Commit 2024-02-23 17:24 29cdb910

View on Github →

feat(Algebra/Homology): the total complex functor (#10711) In this PR, the construction of the total complex of a bicomplex is extended to a functor HomologicalComplex₂.totalFunctor : HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂.

Estimated changes

Modified Mathlib/Algebra/Homology/HomologicalBicomplex.lean

added def HomologicalComplex₂.toGradedObjectFunctor

added def HomologicalComplex₂.toGradedObjectMap

added theorem HomologicalComplex₂.toGradedObjectMap_apply

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Modified Mathlib/Algebra/Homology/TotalComplex.lean

added theorem HomologicalComplex₂.total.d₁_mapMap

added theorem HomologicalComplex₂.total.d₂_mapMap

added theorem HomologicalComplex₂.total.forget_map

added theorem HomologicalComplex₂.total.hom_ext

added theorem HomologicalComplex₂.total.mapMap_D₁

added theorem HomologicalComplex₂.total.mapMap_D₂

added theorem HomologicalComplex₂.total.map_comp

added theorem HomologicalComplex₂.total.map_id

added theorem HomologicalComplex₂.ιTotalOrZero_map

added theorem HomologicalComplex₂.ιTotal_map

added theorem HomologicalComplex₂.ι_totalDesc

Modified Mathlib/CategoryTheory/GradedObject.lean

added theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap