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₄] : Prop

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

• HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄ = CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G (c₁.ρ₁₂ c₂ c₃ c₁₂ c₄) K₁.X K₂.X K₃.X

@[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₄] : Prop

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

• HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ = CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ (c₁.ρ₂₃ c₂ c₃ c₁₂ c₂₃ c₄) K₁.X K₂.X K₃.X

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₁₂)

Equations

• ⋯ = ⋯

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₄)

Equations

• ⋯ = ⋯

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₄)

Equations

• ⋯ = ⋯

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.

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

• HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h = CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G (c₁.ρ₁₂ c₂ c₃ c₁₂ c₄) K₁.X K₂.X K₃.X i₁ i₂ i₃ j h

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.

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

• HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f = CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f

@[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) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f) = f i₁ i₂ i₃ h

@[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) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f) h✝) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h) h✝

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.

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.

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.

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.

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.

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

• HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = HomologicalComplex.mapBifunctor.D₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ j j'

@[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

• HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h = CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ (c₁.ρ₂₃ c₂ c₃ c₁₂ c₂₃ c₄) K₁.X K₂.X K₃.X i₁ i₂ i₃ j h

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.

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

• HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc c₁₂ f = CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f

@[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) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc c₁₂ f) h✝) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h) h✝

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.

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.

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.

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

• HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' = HomologicalComplex.mapBifunctor.D₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ j 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₄] (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.

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.

@[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

• HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ = HomologicalComplex.Hom.isoOfComponents (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄) ⋯