Documentation

Mathlib.Algebra.Homology.Bifunctor

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

@[simp]
theorem CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂} {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_d_f {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂ : 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} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂' : I₂) :
(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
@[simp]
theorem CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂)
def CategoryTheory.Functor.mapBifunctorHomologicalComplexObj {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₁) :

Auxiliary definition for mapBifunctorHomologicalComplex.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂ : 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} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂} {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_map_app_f_f {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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 : 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_X_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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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₂' : I₂) :
    ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject {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] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.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 = ((CategoryTheory.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] :

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

      Equations
      • K₁.HasMapBifunctor K₂ F c = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).HasTotal c
      Instances For
        @[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] :

        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₂.

        Equations
        • K₁.mapBifunctor K₂ F c = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).total c
        Instances For
          @[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.

          Equations
          • K₁.ιMapBifunctor K₂ F c i₁ i₂ j h = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h
          Instances For
            @[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.

            Equations
            • K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotalOrZero c i₁ i₂ j
            Instances For
              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.

              Equations
              Instances For
                @[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) :
                @[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) (HomologicalComplex.mapBifunctorDesc f) = f i₁ i₂ h
                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 : (K₁.mapBifunctor K₂ F c).X j Y} {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
                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 : (K₁.mapBifunctor K₂ F c).X j Y} {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
                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' : J) :
                (K₁.mapBifunctor K₂ F c).X j (K₁.mapBifunctor K₂ F c).X j'

                The first differential on mapBifunctor K₁ K₂ F c

                Equations
                Instances For
                  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' : J) :
                  (K₁.mapBifunctor K₂ F c).X j (K₁.mapBifunctor K₂ F c).X j'

                  The second differential on mapBifunctor K₁ K₂ F c

                  Equations
                  Instances For
                    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' : J) :
                    (K₁.mapBifunctor K₂ F c).d j j' = HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j' + HomologicalComplex.mapBifunctor.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

                    Equations
                    Instances For
                      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

                      Equations
                      Instances For
                        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₁)) :
                        HomologicalComplex.mapBifunctor.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₂)) :
                        HomologicalComplex.mapBifunctor.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₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) (h' : c₁ c₂ c (i₁', i₂) j) :
                        HomologicalComplex.mapBifunctor.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₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) (h' : c₁ c₂ c (i₁, i₂') j) :
                        HomologicalComplex.mapBifunctor.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₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) :
                        HomologicalComplex.mapBifunctor.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₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) :
                        HomologicalComplex.mapBifunctor.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₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) (h' : c₁ c₂ c (i₁', i₂) = j) :
                        HomologicalComplex.mapBifunctor.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₂' : I₂} (h : c₂.Rel i₂ i₂') (j : J) (h' : c₁ c₂ c (i₁, i₂') = j) :
                        HomologicalComplex.mapBifunctor.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₁_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' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁ c₂ c (i₁, i₂) = j) {Z : D} (h : (K₁.mapBifunctor K₂ F c).X j' Z) :
                        @[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' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁ c₂ c (i₁, i₂) = j) :
                        CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j') = HomologicalComplex.mapBifunctor.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' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁ c₂ c (i₁, i₂) = j) {Z : D} (h : (K₁.mapBifunctor K₂ F c).X j' Z) :
                        @[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' : J) (i₁ : I₁) (i₂ : I₂) (h : c₁ c₂ c (i₁, i₂) = j) :
                        CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j') = HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j'
                        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₁ : HomologicalComplex C₁ c₁} {L₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {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₂.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[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₁ : HomologicalComplex C₁ c₁} {L₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {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 ((HomologicalComplex.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))
                          @[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₁ : HomologicalComplex C₁ c₁} {L₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {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) ((HomologicalComplex.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))