Commit 2024-09-27 15:51 4da4503a

View on Github →

feat(Algebra/Homology): study of the source of the associator isomorphism for the action of bifunctors on homological complexes (#16298) In this PR, we decompose the differential on a homological complex of the form mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄ into three components.

Estimated changes

Modified Mathlib/Algebra/Homology/BifunctorAssociator.lean

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

added theorem HomologicalComplex.mapBifunctor₁₂.d₂_eq_zero

added theorem HomologicalComplex.mapBifunctor₁₂.d₃_eq

added theorem HomologicalComplex.mapBifunctor₁₂.d₃_eq_zero

added theorem HomologicalComplex.mapBifunctor₁₂.ι_D₁

added theorem HomologicalComplex.mapBifunctor₁₂.ι_D₂

added theorem HomologicalComplex.mapBifunctor₁₂.ι_D₃