The action of a bifunctor on homological complexes

Given a bifunctor F : C₁ ⥤ C₂ ⥤ D and complexes shapes c₁ : ComplexShape I₁ and c₂ : ComplexShape I₂, we define a bifunctor mapBifunctorHomologicalComplex F c₁ c₂ of type HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂.

Then, when K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and c : ComplexShape J are such that we have TotalComplexShape c₁ c₂ c, we introduce a typeclass HasMapBifunctor K₁ K₂ F c which allows to define mapBifunctor K₁ K₂ F c : HomologicalComplex D c as the total complex of the bicomplex (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).

def CategoryTheory.Functor.mapBifunctorHomologicalComplexObj {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) : Functor (HomologicalComplex C₂ c₂) (HomologicalComplex₂ D c₁ c₂)

Auxiliary definition for mapBifunctorHomologicalComplex.

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) {K₂ K₂' : HomologicalComplex C₂ c₂} {φ : K₂ ⟶ K₂'} (i₁ : I₁) (i₂ : I₂) : (((F.mapBifunctorHomologicalComplexObj c₂ K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂) : (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁) (i₂ : I₂) : (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ i₂' : I₂) : (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')

def CategoryTheory.Functor.mapBifunctorHomologicalComplex {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] : Functor (HomologicalComplex C₁ c₁) (Functor (HomologicalComplex C₂ c₂) (HomologicalComplex₂ D c₁ c₂))

Given a functor F : C₁ ⥤ C₂ ⥤ D, this is the bifunctor which sends K₁ : HomologicalComplex C₁ c₁ and K₂ : HomologicalComplex C₂ c₂ to the bicomplex which is degree (i₁, i₂) consists of (F.obj (K₁.X i₁)).obj (K₂.X i₂).

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) {K₂ K₂' : HomologicalComplex C₂ c₂} {φ : K₂ ⟶ K₂'} (i₁ : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ i₂' : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {K₁ K₁' : HomologicalComplex C₁ c₁} (f : K₁ ⟶ K₁') (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂) : ((((F.mapBifunctorHomologicalComplex c₁ c₂).map f).app K₂).f i₁).f i₂ = (F.map (f.f i₁)).app (K₂.X i₂)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Limits.HasZeroMorphisms D] (F : Functor C₁ (Functor C₂ D)) {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) : (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).toGradedObject = ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X

@[reducible, inline]

abbrev HomologicalComplex.HasMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] : Prop

The condition that ((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂ has a total complex.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.mapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] : HomologicalComplex D c

Given K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂, a bifunctor F : C₁ ⥤ C₂ ⥤ D and a complex shape ComplexShape J such that we have [TotalComplexShape c₁ c₂ c], this mapBifunctor K₁ K₂ F c : HomologicalComplex D c is the total complex of the bicomplex obtained by applying F to K₁ and K₂.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.ιMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j

The inclusion of a summand of (mapBifunctor K₁ K₂ F c).X j.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.ιMapBifunctorOrZero {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j

The inclusion of a summand of (mapBifunctor K₁ K₂ F c).X j, or zero.

theorem HomologicalComplex.ιMapBifunctorOrZero_eq {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) : K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = K₁.ιMapBifunctor K₂ F c i₁ i₂ j h

theorem HomologicalComplex.ιMapBifunctorOrZero_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) ≠ j) : K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = 0

noncomputable def HomologicalComplex.mapBifunctorDesc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {A : D} {j : J} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)) : (K₁.mapBifunctor K₂ F c).X j ⟶ A

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

@[simp]

theorem HomologicalComplex.ι_mapBifunctorDesc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {A : D} {j : J} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (mapBifunctorDesc f) = f i₁ i₂ h

@[simp]

theorem HomologicalComplex.ι_mapBifunctorDesc_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {A : D} {j : J} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp (mapBifunctorDesc f) h✝) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ h) h✝

theorem HomologicalComplex.mapBifunctor.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {Y : D} {j : J} {f g : (K₁.mapBifunctor K₂ F c).X j ⟶ Y} (h : ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j), CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) f = CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) g) : f = g

theorem HomologicalComplex.mapBifunctor.hom_ext_iff {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {Y : D} {j : J} {f g : (K₁.mapBifunctor K₂ F c).X j ⟶ Y} : f = g ↔ ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j), CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) f = CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) g

noncomputable def HomologicalComplex.mapBifunctor.D₁ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) : (K₁.mapBifunctor K₂ F c).X j ⟶ (K₁.mapBifunctor K₂ F c).X j'

The first differential on mapBifunctor K₁ K₂ F c

noncomputable def HomologicalComplex.mapBifunctor.D₂ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) : (K₁.mapBifunctor K₂ F c).X j ⟶ (K₁.mapBifunctor K₂ F c).X j'

The second differential on mapBifunctor K₁ K₂ F c

theorem HomologicalComplex.mapBifunctor.d_eq {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) : (K₁.mapBifunctor K₂ F c).d j j' = D₁ K₁ K₂ F c j j' + D₂ K₁ K₂ F c j j'

noncomputable def HomologicalComplex.mapBifunctor.d₁ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j

The first differential on a summand of mapBifunctor K₁ K₂ F c

noncomputable def HomologicalComplex.mapBifunctor.d₂ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j

The second differential on a summand of mapBifunctor K₁ K₂ F c

theorem HomologicalComplex.mapBifunctor.d₁_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : ¬c₁.Rel i₁ (c₁.next i₁)) : d₁ K₁ K₂ F c i₁ i₂ j = 0

theorem HomologicalComplex.mapBifunctor.d₂_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : ¬c₂.Rel i₂ (c₂.next i₂)) : d₂ K₁ K₂ F c i₁ i₂ j = 0

theorem HomologicalComplex.mapBifunctor.d₁_eq_zero' {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) (h' : c₁.π c₂ c (i₁', i₂) ≠ j) : d₁ K₁ K₂ F c i₁ i₂ j = 0

theorem HomologicalComplex.mapBifunctor.d₂_eq_zero' {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) (h' : c₁.π c₂ c (i₁, i₂') ≠ j) : d₂ K₁ K₂ F c i₁ i₂ j = 0

theorem HomologicalComplex.mapBifunctor.d₁_eq' {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) : d₁ K₁ K₂ F c i₁ i₂ j = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctorOrZero K₂ F c i₁' i₂ j)

theorem HomologicalComplex.mapBifunctor.d₂_eq' {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) : d₂ K₁ K₂ F c i₁ i₂ j = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂' j)

theorem HomologicalComplex.mapBifunctor.d₁_eq {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) (h' : c₁.π c₂ c (i₁', i₂) = j) : d₁ K₁ K₂ F c i₁ i₂ j = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h')

theorem HomologicalComplex.mapBifunctor.d₂_eq {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) (h' : c₁.π c₂ c (i₁, i₂') = j) : d₂ K₁ K₂ F c i₁ i₂ j = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h')

@[simp]

theorem HomologicalComplex.mapBifunctor.ι_D₁ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (D₁ K₁ K₂ F c j j') = d₁ K₁ K₂ F c i₁ i₂ j'

@[simp]

theorem HomologicalComplex.mapBifunctor.ι_D₁_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h✝ : (K₁.mapBifunctor K₂ F c).X j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp (D₁ K₁ K₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (d₁ K₁ K₂ F c i₁ i₂ j') h✝

@[simp]

theorem HomologicalComplex.mapBifunctor.ι_D₂ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (D₂ K₁ K₂ F c j j') = d₂ K₁ K₂ F c i₁ i₂ j'

@[simp]

theorem HomologicalComplex.mapBifunctor.ι_D₂_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h✝ : (K₁.mapBifunctor K₂ F c).X j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp (D₂ K₁ K₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (d₂ K₁ K₂ F c i₁ i₂ j') h✝

noncomputable def HomologicalComplex.mapBifunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] [DecidableEq J] : K₁.mapBifunctor K₂ F c ⟶ L₁.mapBifunctor L₂ F c

The morphism mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c induced by morphisms of complexes K₁ ⟶ L₁ and K₂ ⟶ L₂.

@[simp]

theorem HomologicalComplex.ι_mapBifunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) ((mapBifunctorMap f₁ f₂ F c).f j) = CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctor L₂ F c i₁ i₂ j h))

@[simp]

theorem HomologicalComplex.ι_mapBifunctorMap_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h✝ : (L₁.mapBifunctor L₂ F c).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp ((mapBifunctorMap f₁ f₂ F c).f j) h✝) = CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (CategoryTheory.CategoryStruct.comp (L₁.ιMapBifunctor L₂ F c i₁ i₂ j h) h✝))