Documentation

Mathlib.Algebra.Homology.BifunctorAssociator

The associator for actions of bifunctors on homological complexes #

In this file, we shall adapt the results of the file CategoryTheory.GradedObject.Associator to the case of homological complexes. Given functors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, F : C₁ ⥤ C₂₃ ⥤ C₄, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃ equipped with an isomorphism associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃ (which informally means that we have natural isomorphisms G(F₁₂(X₁, X₂), X₃) ≅ F(X₁, G₂₃(X₂, X₃))), we define an isomorphism mapBifunctorAssociator from mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄ to mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄ when we have three homological complexes K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and K₃ : HomologicalComplex C₃ c₃, assumptions TotalComplexShape c₁ c₂ c₁₂, TotalComplexShape c₁₂ c₃ c₄, TotalComplexShape c₂ c₃ c₂₃, TotalComplexShape c₁ c₂₃ c₄, and ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄ about the complex shapes, and technical assumptions [HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] and [HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] about the commutation of certain functors to certain coproducts.

The main application of these results shall be the construction of the associator for the monoidal category structure on homological complexes.

@[reducible, inline]
abbrev HomologicalComplex.HasGoodTrifunctor₁₂Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] :

Given bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, homological complexes K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and K₃ : HomologicalComplex C₃ c₃, and complexes shapes c₁₂, c₄, this asserts that for all i₁₂ : ι₁₂ and i₃ : ι₃, the functor G(-, K₃.X i₃) commutes with the coproducts of the F₁₂(X₁ i₁, X₂ i₂) such that π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂.

Equations
Instances For
    @[reducible, inline]
    abbrev HomologicalComplex.HasGoodTrifunctor₂₃Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] :

    Given bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃, homological complexes K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and K₃ : HomologicalComplex C₃ c₃, and complexes shapes c₁₂, c₂₃, c₄ with ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄, this asserts that for all i₁ : ι₁ and i₂₃ : ι₂₃, the functor F(K₁.X i₁, _) commutes with the coproducts of the G₂₃(K₂.X i₂, K₃.X i₃) such that π c₂ c₃ c₂₃ ⟨i₂, i₃⟩ = i₂₃.

    Equations
    Instances For
      instance HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₁₂ : Type u_10} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (c₁₂ : ComplexShape ι₁₂) [TotalComplexShape c₁ c₂ c₁₂] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] :
      (((CategoryTheory.GradedObject.mapBifunctor F₁₂ ι₁ ι₂).obj K₁.X).obj K₂.X).HasMap (c₁ c₂ c₁₂)
      instance HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] :
      (((CategoryTheory.GradedObject.mapBifunctor G ι₁₂ ι₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ (c₁ c₂ c₁₂) K₁.X K₂.X)).obj K₃.X).HasMap (c₁₂ c₃ c₄)
      instance HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_17, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₂₃ : Type u_11} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] :
      (((CategoryTheory.GradedObject.mapBifunctor F ι₁ ι₂₃).obj K₁.X).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ (c₂ c₃ c₂₃) K₂.X K₃.X)).HasMap (c₁ c₂₃ c₄)
      noncomputable def HomologicalComplex.mapBifunctorAssociatorX {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [H₁₂ : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [H₂₃ : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j : ι₄) :
      ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

      The associator isomorphism for the action of bifunctors on homological complexes, in each degree.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def HomologicalComplex.mapBifunctor₁₂.ι {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

        The inclusion of a summand in mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

        Equations
        Instances For
          theorem HomologicalComplex.mapBifunctor₁₂.ι_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (i₁₂ : ι₁₂) (j : ι₄) (h₁₂ : c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) (h : c₁₂ c₃ c₄ (i₁₂, i₃) = j) :
          HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = CategoryTheory.CategoryStruct.comp ((G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ i₁₂ h₁₂)).app (K₃.X i₃)) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).ιMapBifunctor K₃ G c₄ i₁₂ i₃ j h)
          noncomputable def HomologicalComplex.mapBifunctor₁₂.ιOrZero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
          (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

          The inclusion of a summand in mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄, or zero.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
            HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h
            theorem HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) j) :
            HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
            theorem HomologicalComplex.mapBifunctor₁₂.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} {f g : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j A} (hfg : ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) g) :
            f = g
            noncomputable def HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) A)) :
            ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j A

            Constructor for morphisms from (mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j.

            Equations
            Instances For
              @[simp]
              theorem HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) A)) (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
              @[simp]
              theorem HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) A)) (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : A Z) :
              noncomputable def HomologicalComplex.mapBifunctor₁₂.d₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
              (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

              The first differential on a summand of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem HomologicalComplex.mapBifunctor₁₂.d₁_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₁.Rel i₁ (c₁.next i₁)) :
                HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
                theorem HomologicalComplex.mapBifunctor₁₂.d₁_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] {i₁ i₁' : ι₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = (c₁₂.ε₁ c₃ c₄ (c₁ c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃)) (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j)
                noncomputable def HomologicalComplex.mapBifunctor₁₂.d₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

                The second differential on a summand of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem HomologicalComplex.mapBifunctor₁₂.d₂_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₂.Rel i₂ (c₂.next i₂)) :
                  HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
                  theorem HomologicalComplex.mapBifunctor₁₂.d₂_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) {i₂ i₂' : ι₂} (h₂ : c₂.Rel i₂ i₂') (i₃ : ι₃) (j : ι₄) :
                  HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = (c₁₂.ε₁ c₃ c₄ (c₁ c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))).app (K₃.X i₃)) (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂' i₃ j)
                  noncomputable def HomologicalComplex.mapBifunctor₁₂.d₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                  (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

                  The third differential on a summand of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem HomologicalComplex.mapBifunctor₁₂.d₃_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₃.Rel i₃ (c₃.next i₃)) :
                    HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
                    theorem HomologicalComplex.mapBifunctor₁₂.d₃_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃} (h₃ : c₃.Rel i₃ i₃') (j : ι₄) :
                    HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = c₁₂.ε₂ c₃ c₄ (c₁ c₂ c₁₂ (i₁, i₂), i₃) CategoryTheory.CategoryStruct.comp ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ i₃')) (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃' j)
                    noncomputable def HomologicalComplex.mapBifunctor₁₂.D₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] (j j' : ι₄) :
                    ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j'

                    The first differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      noncomputable def HomologicalComplex.mapBifunctor₁₂.D₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] (j j' : ι₄) :
                      ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j'

                      The second differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        noncomputable def HomologicalComplex.mapBifunctor₁₂.D₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (j j' : ι₄) :
                        ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j'

                        The third differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

                        Equations
                        Instances For
                          @[simp]
                          theorem HomologicalComplex.mapBifunctor₁₂.ι_D₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] :
                          CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
                          @[simp]
                          theorem HomologicalComplex.mapBifunctor₁₂.ι_D₁_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {Z : C₄} (h✝ : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' Z) :
                          CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h✝
                          @[simp]
                          theorem HomologicalComplex.mapBifunctor₁₂.ι_D₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] :
                          CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
                          @[simp]
                          theorem HomologicalComplex.mapBifunctor₁₂.ι_D₂_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {Z : C₄} (h✝ : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' Z) :
                          CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h✝
                          @[simp]
                          theorem HomologicalComplex.mapBifunctor₁₂.ι_D₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
                          CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
                          @[simp]
                          theorem HomologicalComplex.mapBifunctor₁₂.ι_D₃_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' Z) :
                          CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h✝
                          theorem HomologicalComplex.mapBifunctor₁₂.d_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [DecidableEq ι₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (j j' : ι₄) [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] :
                          ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).d j j' = HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j'
                          noncomputable def HomologicalComplex.mapBifunctor₂₃.ι {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
                          (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

                          The inclusion of a summand in mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                          Equations
                          Instances For
                            theorem HomologicalComplex.mapBifunctor₂₃.ι_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (i₂₃ : ι₂₃) (j : ι₄) (h₂₃ : c₂ c₃ c₂₃ (i₂, i₃) = i₂₃) (h : c₁ c₂₃ c₄ (i₁, i₂₃) = j) :
                            HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ i₂₃ h₂₃)) (K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ i₂₃ j h)
                            noncomputable def HomologicalComplex.mapBifunctor₂₃.ιOrZero {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                            (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

                            The inclusion of a summand in mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄, or zero.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
                              HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h
                              theorem HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) j) :
                              HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = 0
                              theorem HomologicalComplex.mapBifunctor₂₃.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_17, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄} {f g : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j A} (hfg : ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) g) :
                              f = g
                              noncomputable def HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j((F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) A)) :
                              (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j A

                              Constructor for morphisms from (mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j.

                              Equations
                              Instances For
                                @[simp]
                                theorem HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j((F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) A)) (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
                                CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc c₁₂ f) = f i₁ i₂ i₃ h
                                @[simp]
                                theorem HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j((F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) A)) (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : A Z) :
                                noncomputable def HomologicalComplex.mapBifunctor₂₃.d₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                                (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

                                The first differential on a summand of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem HomologicalComplex.mapBifunctor₂₃.d₁_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₁.Rel i₁ (c₁.next i₁)) :
                                  HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = 0
                                  theorem HomologicalComplex.mapBifunctor₂₃.d₁_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] {i₁ i₁' : ι₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                                  HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = c₁.ε₁ c₂₃ c₄ (i₁, c₂ c₃ c₂₃ (i₂, i₃)) CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃))) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁' i₂ i₃ j)
                                  noncomputable def HomologicalComplex.mapBifunctor₂₃.d₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                                  (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

                                  The second differential on a summand of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem HomologicalComplex.mapBifunctor₂₃.d₂_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₂.Rel i₂ (c₂.next i₂)) :
                                    HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = 0
                                    theorem HomologicalComplex.mapBifunctor₂₃.d₂_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) {i₂ i₂' : ι₂} (h₂ : c₂.Rel i₂ i₂') (i₃ : ι₃) (j : ι₄) :
                                    HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = (c₁.ε₂ c₂₃ c₄ (i₁, c₂ c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃)) CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map ((G₂₃.map (K₂.d i₂ i₂')).app (K₃.X i₃))) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂' i₃ j)
                                    noncomputable def HomologicalComplex.mapBifunctor₂₃.d₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                                    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

                                    The third differential on a summand of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem HomologicalComplex.mapBifunctor₂₃.d₃_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₃.Rel i₃ (c₃.next i₃)) :
                                      HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = 0
                                      theorem HomologicalComplex.mapBifunctor₂₃.d₃_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃} (h₃ : c₃.Rel i₃ i₃') (j : ι₄) :
                                      HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j = (c₁.ε₂ c₂₃ c₄ (i₁, c₂ c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)) CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map ((G₂₃.obj (K₂.X i₂)).map (K₃.d i₃ i₃'))) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃' j)
                                      noncomputable def HomologicalComplex.mapBifunctor₂₃.D₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄) :
                                      (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j'

                                      The first differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                                      Equations
                                      Instances For
                                        noncomputable def HomologicalComplex.mapBifunctor₂₃.D₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄) [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] :
                                        (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j'

                                        The second differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          noncomputable def HomologicalComplex.mapBifunctor₂₃.D₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄) [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] :
                                          (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j'

                                          The third differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem HomologicalComplex.mapBifunctor₂₃.ι_D₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') = HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
                                            @[simp]
                                            theorem HomologicalComplex.mapBifunctor₂₃.ι_D₁_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j') h✝
                                            @[simp]
                                            theorem HomologicalComplex.mapBifunctor₂₃.ι_D₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
                                            @[simp]
                                            theorem HomologicalComplex.mapBifunctor₂₃.ι_D₂_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {Z : C₄} (h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j') h✝
                                            @[simp]
                                            theorem HomologicalComplex.mapBifunctor₂₃.ι_D₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
                                            @[simp]
                                            theorem HomologicalComplex.mapBifunctor₂₃.ι_D₃_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_16, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {Z : C₄} (h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j') h✝
                                            theorem HomologicalComplex.mapBifunctor₂₃.d_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_17, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) :
                                            (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).d j j' = HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' + HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' + HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j'
                                            @[simp]
                                            theorem HomologicalComplex.ι_mapBifunctorAssociatorX_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃)) (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h)
                                            @[simp]
                                            theorem HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom h✝) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) h✝)
                                            @[simp]
                                            theorem HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j) (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃)) (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j)
                                            @[simp]
                                            theorem HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) {Z : C₄} (h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom h) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j) h)
                                            theorem HomologicalComplex.mapBifunctorAssociatorX_hom_D₁ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom (HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom
                                            theorem HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) {Z : C₄} (h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom h)
                                            theorem HomologicalComplex.mapBifunctorAssociatorX_hom_D₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom (HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom
                                            theorem HomologicalComplex.mapBifunctorAssociatorX_hom_D₂_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) {Z : C₄} (h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom h)
                                            theorem HomologicalComplex.mapBifunctorAssociatorX_hom_D₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom (HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom
                                            theorem HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄) {Z : C₄} (h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' Z) :
                                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom h)
                                            noncomputable def HomologicalComplex.mapBifunctorAssociator {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [DecidableEq ι₁₂] [DecidableEq ι₂₃] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] :
                                            (K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄ K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄

                                            The associator isomorphism for the action of bifunctors on homological complexes.

                                            Equations
                                            Instances For