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 : ℤ.

TODO

• obtain various compatibilities

@[inline, reducible]

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)) [CategoryTheory.Functor.PreservesZeroMorphisms F] [∀ (X₁ : C₁), CategoryTheory.Functor.PreservesZeroMorphisms (F.obj X₁)] : Prop

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

Equations

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

@[inline, reducible]

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)) [CategoryTheory.Functor.PreservesZeroMorphisms F] [∀ (X₁ : C₁), CategoryTheory.Functor.PreservesZeroMorphisms (F.obj X₁)] [CochainComplex.HasMapBifunctor K₁ 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

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

@[inline, reducible]

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)) [CategoryTheory.Functor.PreservesZeroMorphisms F] [∀ (X₁ : C₁), CategoryTheory.Functor.PreservesZeroMorphisms (F.obj X₁)] [CochainComplex.HasMapBifunctor K₁ K₂ F] (n₁ : ℤ) (n₂ : ℤ) (n : ℤ) (h : n₁ + n₂ = n) : (F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (CochainComplex.mapBifunctor K₁ 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

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

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)) [CategoryTheory.Functor.Additive F] [∀ (X₁ : C₁), CategoryTheory.Functor.PreservesZeroMorphisms (F.obj X₁)] (x : ℤ) : ((CategoryTheory.Functor.mapBifunctorHomologicalComplex F (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj K₂ ≅ (HomologicalComplex₂.shiftFunctor₁ D x).obj (((CategoryTheory.Functor.mapBifunctorHomologicalComplex F (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.

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)) [CategoryTheory.Functor.Additive F] [∀ (X₁ : C₁), CategoryTheory.Functor.PreservesZeroMorphisms (F.obj X₁)] (x : ℤ) [CochainComplex.HasMapBifunctor K₁ K₂ F] [CochainComplex.HasMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁) K₂ F] [HomologicalComplex₂.HasTotal ((HomologicalComplex₂.shiftFunctor₁ D x).obj (((CategoryTheory.Functor.mapBifunctorHomologicalComplex F (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)) (ComplexShape.up ℤ)] : CochainComplex.mapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁) K₂ F ≅ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (CochainComplex.mapBifunctor K₁ 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.

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)) [CategoryTheory.Functor.PreservesZeroMorphisms F] [∀ (X₁ : C₁), CategoryTheory.Functor.Additive (F.obj X₁)] (y : ℤ) : ((CategoryTheory.Functor.mapBifunctorHomologicalComplex F (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂) ≅ (HomologicalComplex₂.shiftFunctor₂ D y).obj (((CategoryTheory.Functor.mapBifunctorHomologicalComplex F (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.

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)) [CategoryTheory.Functor.PreservesZeroMorphisms F] [∀ (X₁ : C₁), CategoryTheory.Functor.Additive (F.obj X₁)] (y : ℤ) [CochainComplex.HasMapBifunctor K₁ K₂ F] [CochainComplex.HasMapBifunctor K₁ ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F] [HomologicalComplex₂.HasTotal ((HomologicalComplex₂.shiftFunctor₂ D y).obj (((CategoryTheory.Functor.mapBifunctorHomologicalComplex F (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)) (ComplexShape.up ℤ)] : CochainComplex.mapBifunctor K₁ ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F ≅ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (CochainComplex.mapBifunctor K₁ 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.