Commit 2024-11-20 13:18 159918f8
View on Github →feat: the monoidal category structure on homological complexes (#15695)
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 eqquiped 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.