The differential of a tensor product of complexes

Mathlib's HomologicalComplex.monoidalCategory totalizes the degreewise tensor product of complexes, with the tensor signs ε₁ = 1 and ε₂ (p, q) = (-1)^p. This file records the resulting differential on a homogeneous summand, d (x ⊗ y) = d x ⊗ y + (-1)^p x ⊗ d y for x of degree p: as a single rewrite rule for cochain complexes of modules indexed by ℤ, and as its two parts HomologicalComplex.mapBifunctor.D₁ and HomologicalComplex.mapBifunctor.D₂ for chain complexes indexed by ℕ in any monoidal preadditive category, where a part vanishes on a summand whose factor of degree zero it would differentiate.

Main results

• HomologicalComplex.ι_tensorObj_d: the differential of X ⊗ Y restricted to the summand X.X p ⊗ Y.X q, for cochain complexes of modules.
• ChainComplex.ιTensorObj_D₁_succ, ChainComplex.ιTensorObj_D₁_zero, ChainComplex.ιTensorObj_D₂_succ and ChainComplex.ιTensorObj_D₂_zero: the two parts of the differential of K₁ ⊗ K₂ on a homogeneous summand, for chain complexes indexed by ℕ.

Implementation notes

Mathlib.CategoryTheory.Monoidal.Closed.Braided is imported for the colimit-preservation instances that make the tensor product of cochain complexes exist at all, exactly as in TauCeti/Algebra/Homology/Monoidal/Braiding.lean.

@[simp]

theorem HomologicalComplex.ι_tensorObj_d {R : Type v} [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (hpq : p + q = j) : CategoryTheory.CategoryStruct.comp (ιTensorObj X Y p q j hpq) ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).d j (j + 1)) = CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)).map (X.d p (p + 1))).app (Y.X q)) (ιTensorObj X Y (p + 1) q (j + 1) ⋯) + p.negOnePow • CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)).obj (X.X p)).map (Y.d q (q + 1))) (ιTensorObj X Y p (q + 1) (j + 1) ⋯)

The differential of a tensor product of cochain complexes on a homogeneous summand is the sum of the two factor differentials, with the Koszul sign on the second term.

@[simp]

theorem HomologicalComplex.ι_tensorObj_d_assoc {R : Type v} [CommRing R] (X Y : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (hpq : p + q = j) {Z : ModuleCat R} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).X (j + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιTensorObj X Y p q j hpq) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).d j (j + 1)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)).map (X.d p (p + 1))).app (Y.X q)) (ιTensorObj X Y (p + 1) q (j + 1) ⋯) + p.negOnePow • CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)).obj (X.X p)).map (Y.d q (q + 1))) (ιTensorObj X Y p (q + 1) (j + 1) ⋯)) h

The differential of a tensor product of cochain complexes on a homogeneous summand is the sum of the two factor differentials, with the Koszul sign on the second term.

theorem ChainComplex.ιTensorObj_D₁_succ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (r s n : ℕ) (h : r + 1 + s = n + 1) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ (r + 1) s (n + 1) h) (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (K₁.d (r + 1) r) (K₂.X s)) (HomologicalComplex.ιTensorObj K₁ K₂ r s n ⋯)

The first part of the differential of a tensor product of chain complexes, on a summand whose first factor has positive degree, is the differential of the first factor.

theorem ChainComplex.ιTensorObj_D₁_succ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (r s n : ℕ) (h : r + 1 + s = n + 1) {Z : C} (h✝ : (HomologicalComplex.mapBifunctor K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ (r + 1) s (n + 1) h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (K₁.d (r + 1) r) (K₂.X s)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ r s n ⋯) h✝)

The first part of the differential of a tensor product of chain complexes, on a summand whose first factor has positive degree, is the differential of the first factor.

theorem ChainComplex.ιTensorObj_D₁_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ 0 (n + 1) (n + 1) ⋯) (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) = 0

The first part of the differential of a tensor product of chain complexes vanishes on a summand whose first factor has degree zero.

theorem ChainComplex.ιTensorObj_D₁_zero_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (n : ℕ) {Z : C} (h : (HomologicalComplex.mapBifunctor K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ 0 (n + 1) (n + 1) ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) h) = CategoryTheory.CategoryStruct.comp 0 h

The first part of the differential of a tensor product of chain complexes vanishes on a summand whose first factor has degree zero.

theorem ChainComplex.ιTensorObj_D₂_succ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (r s n : ℕ) (h : r + (s + 1) = n + 1) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ r (s + 1) (n + 1) h) (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) = (-1) ^ r • CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (K₁.X r) (K₂.d (s + 1) s)) (HomologicalComplex.ιTensorObj K₁ K₂ r s n ⋯)

The second part of the differential of a tensor product of chain complexes, on a summand whose second factor has positive degree, is the differential of the second factor with the Koszul sign (-1)^r of the degree r of the first factor.

theorem ChainComplex.ιTensorObj_D₂_succ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (r s n : ℕ) (h : r + (s + 1) = n + 1) {Z : C} (h✝ : (HomologicalComplex.mapBifunctor K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ r (s + 1) (n + 1) h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) h✝) = CategoryTheory.CategoryStruct.comp ((-1) ^ r • CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (K₁.X r) (K₂.d (s + 1) s)) (HomologicalComplex.ιTensorObj K₁ K₂ r s n ⋯)) h✝

The second part of the differential of a tensor product of chain complexes, on a summand whose second factor has positive degree, is the differential of the second factor with the Koszul sign (-1)^r of the degree r of the first factor.

theorem ChainComplex.ιTensorObj_D₂_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ (n + 1) 0 (n + 1) ⋯) (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) = 0

The second part of the differential of a tensor product of chain complexes vanishes on a summand whose second factor has degree zero.

theorem ChainComplex.ιTensorObj_D₂_zero_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K₁ K₂ : ChainComplex C ℕ) [HomologicalComplex.HasTensor K₁ K₂] (n : ℕ) {Z : C} (h : (HomologicalComplex.mapBifunctor K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj K₁ K₂ (n + 1) 0 (n + 1) ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (ComplexShape.down ℕ) (n + 1) n) h) = CategoryTheory.CategoryStruct.comp 0 h

The second part of the differential of a tensor product of chain complexes vanishes on a summand whose second factor has degree zero.