The monoidal category structure on homological complexes

Let c : ComplexShape I with I an additive monoid. If c is equipped with the data and axioms c.TensorSigns, then the category HomologicalComplex C c can be equipped with a monoidal category structure if C is a monoidal category such that C has certain coproducts and both left/right tensoring commute with these.

In particular, we obtain a monoidal category structure on ChainComplex C ℕ when C is an additive monoidal category.

@[reducible, inline]

abbrev HomologicalComplex.HasTensor {C : Type u_1} [CategoryTheory.Category.{u_3, 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] (K₁ K₂ : HomologicalComplex C c) : Prop

If K₁ and K₂ are two homological complexes, this is the property that for all j, the coproduct of K₁ i₁ ⊗ K₂ i₂ for i₁ + i₂ = j exists.

Equations

• K₁.HasTensor K₂ = K₁.HasMapBifunctor K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) c

@[reducible, inline]

noncomputable abbrev HomologicalComplex.tensorObj {C : Type u_1} [CategoryTheory.Category.{u_3, 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₂ : HomologicalComplex C c) [K₁.HasTensor K₂] : HomologicalComplex C c

The tensor product of two homological complexes.

Equations

• K₁.tensorObj K₂ = K₁.mapBifunctor K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) c

@[reducible, inline]

noncomputable abbrev HomologicalComplex.ιTensorObj {C : Type u_1} [CategoryTheory.Category.{u_3, 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₂ : HomologicalComplex C c) [K₁.HasTensor K₂] (i₁ i₂ j : I) (h : i₁ + i₂ = j) : CategoryTheory.MonoidalCategory.tensorObj (K₁.X i₁) (K₂.X i₂) ⟶ (K₁.tensorObj K₂).X j

The inclusion K₁.X i₁ ⊗ K₂.X i₂ ⟶ (tensorObj K₁ K₂).X j of a summand in the tensor product of the homological complexes.

Equations

• K₁.ιTensorObj K₂ i₁ i₂ j h = K₁.ιMapBifunctor K₂ (CategoryTheory.MonoidalCategory.curriedTensor C) c i₁ i₂ j h

@[reducible, inline]

noncomputable abbrev HomologicalComplex.tensorHom {C : Type u_1} [CategoryTheory.Category.{u_3, 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₁) (g : K₂ ⟶ L₂) [K₁.HasTensor K₂] [L₁.HasTensor L₂] : K₁.tensorObj K₂ ⟶ L₁.tensorObj L₂

The tensor product of two morphisms of homological complexes.

Equations

• HomologicalComplex.tensorHom f g = HomologicalComplex.mapBifunctorMap f g (CategoryTheory.MonoidalCategory.curriedTensor C) c

@[reducible, inline]

abbrev HomologicalComplex.HasGoodTensor₁₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} [c.TensorSigns] (K₁ K₂ K₃ : HomologicalComplex C c) : Prop

Given three homological complexes K₁, K₂, and K₃, this asserts that for all j, the functor - ⊗ K₃.X i₃ commutes with the coproduct of the K₁.X i₁ ⊗ K₂.X i₂ such that i₁ + i₂ = j.

Equations

• K₁.HasGoodTensor₁₂ K₂ K₃ = HomologicalComplex.HasGoodTrifunctor₁₂Obj (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensor C) K₁ K₂ K₃ c c

@[reducible, inline]

abbrev HomologicalComplex.HasGoodTensor₂₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} [c.TensorSigns] (K₁ K₂ K₃ : HomologicalComplex C c) : Prop

Given three homological complexes K₁, K₂, and K₃, this asserts that for all j, the functor K₁.X i₁ commutes with the coproduct of the K₂.X i₂ ⊗ K₃.X i₃ such that i₂ + i₃ = j.

Equations

• K₁.HasGoodTensor₂₃ K₂ K₃ = HomologicalComplex.HasGoodTrifunctor₂₃Obj (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensor C) K₁ K₂ K₃ c c c

@[reducible, inline]

noncomputable abbrev HomologicalComplex.associator {C : Type u_1} [CategoryTheory.Category.{u_3, 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₂ K₃ : HomologicalComplex C c) [K₁.HasTensor K₂] [K₂.HasTensor K₃] [(K₁.tensorObj K₂).HasTensor K₃] [K₁.HasTensor (K₂.tensorObj K₃)] [K₁.HasGoodTensor₁₂ K₂ K₃] [K₁.HasGoodTensor₂₃ K₂ K₃] : (K₁.tensorObj K₂).tensorObj K₃ ≅ K₁.tensorObj (K₂.tensorObj K₃)

The associator isomorphism for the tensor product of homological complexes.

Equations

• K₁.associator K₂ K₃ = HomologicalComplex.mapBifunctorAssociator (CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C) K₁ K₂ K₃ c c c

@[reducible, inline]

noncomputable abbrev HomologicalComplex.tensorUnit (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {I : Type u_2} [AddMonoid I] (c : ComplexShape I) [DecidableEq I] : HomologicalComplex C c

The unit of the tensor product of homological complexes.

Equations

• HomologicalComplex.tensorUnit C c = (HomologicalComplex.single C c 0).obj (𝟙_ C)

noncomputable def HomologicalComplex.tensorUnitIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {I : Type u_2} [AddMonoid I] (c : ComplexShape I) [DecidableEq I] : (CategoryTheory.GradedObject.single₀ I).obj (𝟙_ C) ≅ (HomologicalComplex.tensorUnit C c).X

As a graded object, the single complex (single C c 0).obj (𝟙_ C) identifies to the unit (GradedObject.single₀ I).obj (𝟙_ C) of the tensor product of graded objects.

Equations

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

instance HomologicalComplex.instHasTensorOfHasTensorX {C : Type u_1} [CategoryTheory.Category.{u_3, 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] (K₁ K₂ : HomologicalComplex C c) [CategoryTheory.GradedObject.HasTensor K₁.X K₂.X] : K₁.HasTensor K₂

Equations

• ⋯ = inst

instance HomologicalComplex.instHasGoodTensor₁₂OfHasGoodTensor₁₂TensorX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} [c.TensorSigns] (K₁ K₂ K₃ : HomologicalComplex C c) [CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor K₁.X K₂.X K₃.X] : K₁.HasGoodTensor₁₂ K₂ K₃

Equations

• ⋯ = ⋯

instance HomologicalComplex.instHasGoodTensor₂₃OfHasGoodTensorTensor₂₃X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} [c.TensorSigns] (K₁ K₂ K₃ : HomologicalComplex C c) [CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ K₁.X K₂.X K₃.X] : K₁.HasGoodTensor₂₃ K₂ K₃

Equations

• ⋯ = ⋯

instance HomologicalComplex.instHasTensorXTensorUnit {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] : CategoryTheory.GradedObject.HasTensor (HomologicalComplex.tensorUnit C c).X K.X

Equations

• ⋯ = ⋯

instance HomologicalComplex.instHasTensorTensorUnit {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] : (HomologicalComplex.tensorUnit C c).HasTensor K

Equations

• ⋯ = ⋯

@[simp]

theorem HomologicalComplex.unit_tensor_d₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] (i₁ i₂ j : I) : HomologicalComplex.mapBifunctor.d₁ (HomologicalComplex.tensorUnit C c) K (CategoryTheory.MonoidalCategory.curriedTensor C) c i₁ i₂ j = 0

instance HomologicalComplex.instHasTensorXTensorUnit_1 {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {I : Type u_2} [AddMonoid I] {c : ComplexShape I} (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] : CategoryTheory.GradedObject.HasTensor K.X (HomologicalComplex.tensorUnit C c).X

Equations

• ⋯ = ⋯

instance HomologicalComplex.instHasTensorTensorUnit_1 {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] : K.HasTensor (HomologicalComplex.tensorUnit C c)

Equations

• ⋯ = ⋯

@[simp]

theorem HomologicalComplex.tensor_unit_d₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] (i₁ i₂ j : I) : HomologicalComplex.mapBifunctor.d₂ K (HomologicalComplex.tensorUnit C c) (CategoryTheory.MonoidalCategory.curriedTensor C) c i₁ i₂ j = 0

noncomputable def HomologicalComplex.leftUnitor' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] : ((HomologicalComplex.tensorUnit C c).tensorObj K).X ≅ K.X

Auxiliary definition for leftUnitor.

Equations

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

theorem HomologicalComplex.leftUnitor'_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] (i : I) : K.leftUnitor'.inv i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (K.X i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (HomologicalComplex.singleObjXSelf c 0 (𝟙_ C)).inv (K.X i)) ((HomologicalComplex.tensorUnit C c).ιTensorObj K 0 i i ⋯))

theorem HomologicalComplex.leftUnitor'_inv_comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] (i j : I) : CategoryTheory.CategoryStruct.comp (K.leftUnitor'.inv i) (((HomologicalComplex.tensorUnit C c).tensorObj K).d i j) = CategoryTheory.CategoryStruct.comp (K.d i j) (K.leftUnitor'.inv j)

theorem HomologicalComplex.leftUnitor'_inv_comm_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] (i j : I) {Z : C} (h : ((HomologicalComplex.tensorUnit C c).tensorObj K).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.leftUnitor'.inv i) (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.tensorUnit C c).tensorObj K).d i j) h) = CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (K.leftUnitor'.inv j) h)

noncomputable def HomologicalComplex.leftUnitor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] : (HomologicalComplex.tensorUnit C c).tensorObj K ≅ K

The left unitor for the tensor product of homological complexes.

Equations

• K.leftUnitor = (HomologicalComplex.Hom.isoOfComponents (fun (i : I) => (CategoryTheory.GradedObject.eval i).mapIso K.leftUnitor'.symm) ⋯).symm

noncomputable def HomologicalComplex.rightUnitor' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] : (K.tensorObj (HomologicalComplex.tensorUnit C c)).X ≅ K.X

Auxiliary definition for rightUnitor.

Equations

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

theorem HomologicalComplex.rightUnitor'_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] (i : I) : K.rightUnitor'.inv i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (K.X i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (K.X i) (HomologicalComplex.singleObjXSelf c 0 (𝟙_ C)).inv) (K.ιTensorObj (HomologicalComplex.tensorUnit C c) i 0 i ⋯))

theorem HomologicalComplex.rightUnitor'_inv_comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] (i j : I) : CategoryTheory.CategoryStruct.comp (K.rightUnitor'.inv i) ((K.tensorObj (HomologicalComplex.tensorUnit C c)).d i j) = CategoryTheory.CategoryStruct.comp (K.d i j) (K.rightUnitor'.inv j)

noncomputable def HomologicalComplex.rightUnitor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] (K : HomologicalComplex C c) [DecidableEq I] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] : K.tensorObj (HomologicalComplex.tensorUnit C c) ≅ K

The right unitor for the tensor product of homological complexes.

Equations

• K.rightUnitor = (HomologicalComplex.Hom.isoOfComponents (fun (i : I) => (CategoryTheory.GradedObject.eval i).mapIso K.rightUnitor'.symm) ⋯).symm

noncomputable instance HomologicalComplex.monoidalCategoryStruct (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] [∀ (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₃] [DecidableEq I] : CategoryTheory.MonoidalCategoryStruct (HomologicalComplex C c)

Equations

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

noncomputable def HomologicalComplex.Monoidal.inducingFunctorData (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] [∀ (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₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [DecidableEq I] : CategoryTheory.Monoidal.InducingFunctorData (HomologicalComplex.forget C c)

The structure which allows to construct the monoidal category structure on HomologicalComplex C c from the monoidal category structure on graded objects.

Equations

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

noncomputable instance HomologicalComplex.monoidalCategory (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject 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] [∀ (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₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [DecidableEq I] : CategoryTheory.MonoidalCategory (HomologicalComplex C c)

Equations

• HomologicalComplex.monoidalCategory C c = CategoryTheory.Monoidal.induced (HomologicalComplex.forget C c) (HomologicalComplex.Monoidal.inducingFunctorData C c)