Behavior of the action of a bifunctor on cochain complexes with respect to shifts

In this file, given cochain complexes K₁ : CochainComplex C₁ ℤ, K₂ : CochainComplex C₂ ℤ and a functor F : C₁ ⥤ C₂ ⥤ D, we define an isomorphism of cochain complexes in D:

• CochainComplex.mapBifunctorShift₁Iso K₁ K₂ F x of type mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧ for x : ℤ.
• CochainComplex.mapBifunctorShift₂Iso K₁ K₂ F y of type mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧ for y : ℤ.

In the lemma CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, we obtain that the two ways to deduce an isomorphism mapBifunctor (K₁⟦x⟧) (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦x + y⟧ differ by the sign (x * y).negOnePow.

@[reducible, inline]

abbrev CochainComplex.HasMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] : Prop

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

Equations

• K₁.HasMapBifunctor K₂ F = HomologicalComplex.HasMapBifunctor K₁ K₂ F (ComplexShape.up ℤ)

@[reducible, inline]

noncomputable abbrev CochainComplex.mapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] [K₁.HasMapBifunctor K₂ F] : CochainComplex D ℤ

Given K₁ : CochainComplex C₁ ℤ, K₂ : CochainComplex C₂ ℤ, a bifunctor F : C₁ ⥤ C₂ ⥤ D, this mapBifunctor K₁ K₂ F : CochainComplex D ℤ is the total complex of the bicomplex obtained by applying F to K₁ and K₂.

Equations

• K₁.mapBifunctor K₂ F = HomologicalComplex.mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)

@[reducible, inline]

noncomputable abbrev CochainComplex.ιMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] [K₁.HasMapBifunctor K₂ F] (n₁ : ℤ) (n₂ : ℤ) (n : ℤ) (h : n₁ + n₂ = n) : (F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (K₁.mapBifunctor K₂ F).X n

The inclusion of a summand (F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n of the total cochain complex when n₁ + n₂ = n.

Equations

• K₁.ιMapBifunctor K₂ F n₁ n₂ n h = HomologicalComplex.ιMapBifunctor K₁ K₂ F (ComplexShape.up ℤ) n₁ n₂ n h

@[simp]

theorem CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) (i : ℤ) : ∀ (x_1 : ℤ), ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom.f i).f x_1 = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))

@[simp]

theorem CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) (i : ℤ) : ∀ (x_1 : ℤ), ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).inv.f i).f x_1 = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))

def CochainComplex.mapBifunctorHomologicalComplexShift₁Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) : ((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj K₂ ≅ (HomologicalComplex₂.shiftFunctor₁ D x).obj (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)

Auxiliary definition for mapBifunctorShift₁Iso.

Equations

• One or more equations did not get rendered due to their size.

instance CochainComplex.instHasMapBifunctorObjIntShiftFunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [K₁.HasMapBifunctor K₂ F] : ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).HasMapBifunctor K₂ F

Equations

• ⋯ = ⋯

noncomputable def CochainComplex.mapBifunctorShift₁Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [K₁.HasMapBifunctor K₂ F] : ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctor K₂ F ≅ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (K₁.mapBifunctor K₂ F)

The canonical isomorphism mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧. This isomorphism does not involve signs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) (i : ℤ) (i : ℤ) : ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).inv.f i✝).f i = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X i✝)).obj (K₂.X (i + y)))

@[simp]

theorem CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) (i : ℤ) (i : ℤ) : ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom.f i✝).f i = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X i✝)).obj (K₂.X (i + y)))

def CochainComplex.mapBifunctorHomologicalComplexShift₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) : ((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂) ≅ (HomologicalComplex₂.shiftFunctor₂ D y).obj (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)

Auxiliary definition for mapBifunctorShift₂Iso.

Equations

• One or more equations did not get rendered due to their size.

instance CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1 {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [K₁.HasMapBifunctor K₂ F] : K₁.HasMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F

Equations

• ⋯ = ⋯

noncomputable def CochainComplex.mapBifunctorShift₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [K₁.HasMapBifunctor K₂ F] : K₁.mapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F ≅ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor K₂ F)

The canonical isomorphism mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧. This isomorphism involves signs: on the summand (F.obj (K₁.X p)).obj (K₂.X q), it is given by the multiplication by (p * y).negOnePow.

Equations

• One or more equations did not get rendered due to their size.

theorem CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_4, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (x : ℤ) (y : ℤ) [K₁.HasMapBifunctor K₂ F] : K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) = (x * y).negOnePow • ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F)