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.
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
Instances For
The tensor product of two homological complexes.
Instances For
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
Instances For
The tensor product of two morphisms of homological complexes.
Equations
Instances For
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
Instances For
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
Instances For
The associator isomorphism for the tensor product of homological complexes.
Equations
Instances For
The unit of the tensor product of homological complexes.
Instances For
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.
Instances For
Auxiliary definition for leftUnitor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left unitor for the tensor product of homological complexes.
Equations
Instances For
Auxiliary definition for rightUnitor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right unitor for the tensor product of homological complexes.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
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.