Commit 2024-08-12 13:06 40b6b147

View on Github →

feat(Algebra/Homology): develop the API for the action of bifunctors on homological complexes (#15712)

Estimated changes

Modified Mathlib/Algebra/Homology/Bifunctor.lean

added theorem HomologicalComplex.mapBifunctor.d_eq

added theorem HomologicalComplex.mapBifunctor.d₁_eq'

added theorem HomologicalComplex.mapBifunctor.d₁_eq

added theorem HomologicalComplex.mapBifunctor.d₁_eq_zero'

added theorem HomologicalComplex.mapBifunctor.d₁_eq_zero

added theorem HomologicalComplex.mapBifunctor.d₂_eq'

added theorem HomologicalComplex.mapBifunctor.d₂_eq

added theorem HomologicalComplex.mapBifunctor.d₂_eq_zero'

added theorem HomologicalComplex.mapBifunctor.d₂_eq_zero

added theorem HomologicalComplex.mapBifunctor.hom_ext

added theorem HomologicalComplex.mapBifunctor.ι_D₁

added theorem HomologicalComplex.mapBifunctor.ι_D₂

added theorem HomologicalComplex.ι_mapBifunctorDesc

Modified Mathlib/Algebra/Homology/BifunctorHomotopy.lean

Modified Mathlib/Algebra/Homology/TotalComplex.lean

Modified Mathlib/Algebra/Homology/TotalComplexShift.lean

Modified Mathlib/Algebra/Homology/TotalComplexSymmetry.lean

Modified Mathlib/CategoryTheory/GradedObject/Trifunctor.lean

modified theorem CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext

modified theorem CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext

added theorem CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc

added theorem CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc