The monoidal structure of cochain complexes of modules on homogeneous summands

Mathlib's HomologicalComplex.monoidalCategory totalizes the degreewise tensor product, so every structural map of CochainComplex (ModuleCat R) ℤ is assembled from maps on the homogeneous summands X.X p ⊗ Y.X q of X ⊗ Y. Mathlib states the component formulas for the auxiliary constructions the monoidal structure is built from — HomologicalComplex.mapBifunctorMap, HomologicalComplex.leftUnitor', HomologicalComplex.rightUnitor' and HomologicalComplex.mapBifunctorAssociatorX — but not for the whiskerings, λ_, ρ_ and α_ themselves. This file supplies that last step, so that a calculation on homogeneous summands never has to unfold the monoidal structure. The formula for ⊗ₘ holds verbatim for homological complexes of any shape in any monoidal preadditive category, and is stated in that generality.

Main results

• HomologicalComplex.ι_tensorHom: the tensor product of two morphisms on a homogeneous summand, for homological complexes in any monoidal preadditive category and of any shape.
• HomologicalComplex.tensorHom_eq_mapBifunctorMap: ⊗ₘ of homological complexes is the totalization HomologicalComplex.mapBifunctorMap of the two morphisms.
• HomologicalComplex.ι_whiskerLeft and HomologicalComplex.ι_whiskerRight: the two whiskerings on a homogeneous summand.
• HomologicalComplex.leftUnitor_inv_f and HomologicalComplex.rightUnitor_inv_f: the degreewise components of the inverse unitors.
• HomologicalComplex.ι_ι_associator_hom and HomologicalComplex.ι_ι_associator_inv: the associator and its inverse on the summand X.X p ⊗ Y.X q ⊗ Z.X r, with arbitrary intermediate degrees.

The analogous formula for the differential of a tensor product is HomologicalComplex.ι_tensorObj_d in TauCeti/Algebra/Homology/Monoidal/TensorDifferential.lean.

theorem HomologicalComplex.ι_tensorHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [(CategoryTheory.MonoidalCategory.curriedTensor C).Additive] [∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} [c.TensorSigns] [DecidableEq I] {K₁ K₂ L₁ L₂ : HomologicalComplex C c} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) [K₁.HasTensor K₂] [L₁.HasTensor L₂] (i₁ i₂ j : I) (h : i₁ + i₂ = j) : CategoryTheory.CategoryStruct.comp (K₁.ιTensorObj K₂ i₁ i₂ j h) ((tensorHom f₁ f₂).f j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₁.f i₁) (f₂.f i₂)) (L₁.ιTensorObj L₂ i₁ i₂ j h)

The tensor product of two morphisms of homological complexes, restricted to a homogeneous summand, is the tensor product of their components. Mathlib states this only for HomologicalComplex.mapBifunctorMap, by which ⊗ₘ is defined.

theorem HomologicalComplex.ι_tensorHom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [(CategoryTheory.MonoidalCategory.curriedTensor C).Additive] [∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} [c.TensorSigns] [DecidableEq I] {K₁ K₂ L₁ L₂ : HomologicalComplex C c} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) [K₁.HasTensor K₂] [L₁.HasTensor L₂] (i₁ i₂ j : I) (h : i₁ + i₂ = j) {Z : C} (h✝ : (L₁.tensorObj L₂).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιTensorObj K₂ i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp ((tensorHom f₁ f₂).f j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₁.f i₁) (f₂.f i₂)) (CategoryTheory.CategoryStruct.comp (L₁.ιTensorObj L₂ i₁ i₂ j h) h✝)

The tensor product of two morphisms of homological complexes, restricted to a homogeneous summand, is the tensor product of their components. Mathlib states this only for HomologicalComplex.mapBifunctorMap, by which ⊗ₘ is defined.

theorem HomologicalComplex.tensorHom_eq_mapBifunctorMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [(CategoryTheory.MonoidalCategory.curriedTensor C).Additive] [∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] [DecidableEq I] [CategoryTheory.Limits.HasZeroObject C] [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] {K₁ K₂ L₁ L₂ : HomologicalComplex C c} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) : CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂ = mapBifunctorMap f₁ f₂ (CategoryTheory.MonoidalCategory.curriedTensor C) c

In the monoidal category of homological complexes, ⊗ₘ is the totalization of the two morphisms. Mathlib defines HomologicalComplex.monoidalCategory this way, but states no lemma exposing it, so HomologicalComplex.ι_tensorHom does not apply to ⊗ₘ without this rewrite.

theorem HomologicalComplex.whiskerLeft_eq_mapBifunctorMap {R : Type v} [CommRing R] (X : CochainComplex (ModuleCat R) ℤ) {Y Z : CochainComplex (ModuleCat R) ℤ} (g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g = mapBifunctorMap (CategoryTheory.CategoryStruct.id X) g (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ)

Left whiskering in CochainComplex (ModuleCat R) ℤ is the totalization of the identity and the given morphism. Mathlib defines the monoidal structure on homological complexes through HomologicalComplex.mapBifunctorMap, but states no component lemma for ◁.

theorem HomologicalComplex.whiskerRight_eq_mapBifunctorMap {R : Type v} [CommRing R] {X Y : CochainComplex (ModuleCat R) ℤ} (f : X ⟶ Y) (Z : CochainComplex (ModuleCat R) ℤ) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z = mapBifunctorMap f (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ)

Right whiskering in CochainComplex (ModuleCat R) ℤ is the totalization of the given morphism and the identity; the counterpart of HomologicalComplex.whiskerLeft_eq_mapBifunctorMap.

@[simp]

theorem HomologicalComplex.ι_whiskerLeft {R : Type v} [CommRing R] (X : CochainComplex (ModuleCat R) ℤ) {Y Z : CochainComplex (ModuleCat R) ℤ} (g : Y ⟶ Z) (p q j : ℤ) (h : p + q = j) : CategoryTheory.CategoryStruct.comp (ιTensorObj X Y p q j h) ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g).f j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.X p) (g.f q)) (ιTensorObj X Z p q j h)

Left whiskering of cochain complexes of modules, restricted to a homogeneous summand, is left whiskering of the summand.

@[simp]

theorem HomologicalComplex.ι_whiskerLeft_assoc {R : Type v} [CommRing R] (X : CochainComplex (ModuleCat R) ℤ) {Y Z : CochainComplex (ModuleCat R) ℤ} (g : Y ⟶ Z) (p q j : ℤ) (h : p + q = j) {Z✝ : ModuleCat R} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z).X j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (ιTensorObj X Y p q j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g).f j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.X p) (g.f q)) (CategoryTheory.CategoryStruct.comp (ιTensorObj X Z p q j h) h✝)

Left whiskering of cochain complexes of modules, restricted to a homogeneous summand, is left whiskering of the summand.

@[simp]

theorem HomologicalComplex.ι_whiskerRight {R : Type v} [CommRing R] {X Y : CochainComplex (ModuleCat R) ℤ} (f : X ⟶ Y) (Z : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (h : p + q = j) : CategoryTheory.CategoryStruct.comp (ιTensorObj X Z p q j h) ((CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).f j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.f p) (Z.X q)) (ιTensorObj Y Z p q j h)

Right whiskering of cochain complexes of modules, restricted to a homogeneous summand, is right whiskering of the summand.

@[simp]

theorem HomologicalComplex.ι_whiskerRight_assoc {R : Type v} [CommRing R] {X Y : CochainComplex (ModuleCat R) ℤ} (f : X ⟶ Y) (Z : CochainComplex (ModuleCat R) ℤ) (p q j : ℤ) (h : p + q = j) {Z✝ : ModuleCat R} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z).X j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (ιTensorObj X Z p q j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).f j) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.f p) (Z.X q)) (CategoryTheory.CategoryStruct.comp (ιTensorObj Y Z p q j h) h✝)

Right whiskering of cochain complexes of modules, restricted to a homogeneous summand, is right whiskering of the summand.

theorem HomologicalComplex.leftUnitor_inv_f {R : Type v} [CommRing R] (X : CochainComplex (ModuleCat R) ℤ) (j : ℤ) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.f j = (leftUnitor' X).inv j

The degreewise component of the inverse left unitor of cochain complexes of modules is the component of the auxiliary graded isomorphism HomologicalComplex.leftUnitor', whose value is recorded by HomologicalComplex.leftUnitor'_inv.

theorem HomologicalComplex.rightUnitor_inv_f {R : Type v} [CommRing R] (X : CochainComplex (ModuleCat R) ℤ) (j : ℤ) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.f j = (rightUnitor' X).inv j

The degreewise component of the inverse right unitor of cochain complexes of modules is the component of the auxiliary graded isomorphism HomologicalComplex.rightUnitor', whose value is recorded by HomologicalComplex.rightUnitor'_inv.

theorem HomologicalComplex.ι_ι_associator_hom {R : Type v} [CommRing R] (X Y Z : CochainComplex (ModuleCat R) ℤ) (p q r pq qr j : ℤ) (hpq : p + q = pq) (hqr : q + r = qr) (h : pq + r = j) (h' : p + qr = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ιTensorObj X Y p q pq hpq) (Z.X r)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ιTensorObj Z pq r j h) ((CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.f j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X.X p) (Y.X q) (Z.X r)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.X p) (ιTensorObj Y Z q r qr hqr)) (ιTensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) p qr j h'))

The associator of cochain complexes of modules, restricted to the summand indexed by the degrees p, q and r, is the associator of the three summands. The intermediate degrees pq and qr may be any degrees equal to p + q and q + r.

theorem HomologicalComplex.ι_ι_associator_hom_assoc {R : Type v} [CommRing R] (X Y Z : CochainComplex (ModuleCat R) ℤ) (p q r pq qr j : ℤ) (hpq : p + q = pq) (hqr : q + r = qr) (h : pq + r = j) (h' : p + qr = j) {Z✝ : ModuleCat R} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).X j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ιTensorObj X Y p q pq hpq) (Z.X r)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ιTensorObj Z pq r j h) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.f j) h✝)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X.X p) (Y.X q) (Z.X r)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.X p) (ιTensorObj Y Z q r qr hqr)) (CategoryTheory.CategoryStruct.comp (ιTensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) p qr j h') h✝))

The associator of cochain complexes of modules, restricted to the summand indexed by the degrees p, q and r, is the associator of the three summands. The intermediate degrees pq and qr may be any degrees equal to p + q and q + r.

theorem HomologicalComplex.ι_ι_associator_inv {R : Type v} [CommRing R] (X Y Z : CochainComplex (ModuleCat R) ℤ) (p q r pq qr j : ℤ) (hpq : p + q = pq) (hqr : q + r = qr) (h : pq + r = j) (h' : p + qr = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.X p) (ιTensorObj Y Z q r qr hqr)) (CategoryTheory.CategoryStruct.comp (ιTensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) p qr j h') ((CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.f j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X.X p) (Y.X q) (Z.X r)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ιTensorObj X Y p q pq hpq) (Z.X r)) ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ιTensorObj Z pq r j h))

The inverse associator of cochain complexes of modules, restricted to a homogeneous summand with arbitrary intermediate degrees, is the inverse associator of the three summands.

theorem HomologicalComplex.ι_ι_associator_inv_assoc {R : Type v} [CommRing R] (X Y Z : CochainComplex (ModuleCat R) ℤ) (p q r pq qr j : ℤ) (hpq : p + q = pq) (hqr : q + r = qr) (h : pq + r = j) (h' : p + qr = j) {Z✝ : ModuleCat R} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).X j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.X p) (ιTensorObj Y Z q r qr hqr)) (CategoryTheory.CategoryStruct.comp (ιTensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) p qr j h') (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.f j) h✝)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X.X p) (Y.X q) (Z.X r)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ιTensorObj X Y p q pq hpq) (Z.X r)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ιTensorObj Z pq r j h) h✝))

The inverse associator of cochain complexes of modules, restricted to a homogeneous summand with arbitrary intermediate degrees, is the inverse associator of the three summands.