The monoidal category structures on graded objects #
Assuming that C
is a monoidal category and that I
is an additive monoid,
we introduce a partially defined tensor product on the category GradedObject I C
:
given X₁
and X₂
two objects in GradedObject I C
, we define
GradedObject.Monoidal.tensorObj X₁ X₂
under the assumption HasTensor X₁ X₂
that the coproduct of X₁ i ⊗ X₂ j
for i + j = n
exists for any n : I
.
The tensor product of two graded objects X₁
and X₂
exists if for any n
,
the coproduct of the objects X₁ i ⊗ X₂ j
for i + j = n
exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tensor product of two graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion of a summand in a tensor product of two graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for morphisms from a tensor product of two graded objects.
Equations
Instances For
The morphism tensorObj X₁ Y₁ ⟶ tensorObj X₂ Y₂
induced by morphisms of graded
objects f : X₁ ⟶ X₂
and g : Y₁ ⟶ Y₂
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism tensorObj X Y₁ ⟶ tensorObj X Y₂
induced by a morphism of graded objects
φ : Y₁ ⟶ Y₂
.
Equations
Instances For
The morphism tensorObj X₁ Y ⟶ tensorObj X₂ Y
induced by a morphism of graded objects
φ : X₁ ⟶ X₂
.
Equations
Instances For
This is the addition map I × I × I → I
for an additive monoid I
.
Equations
- CategoryTheory.GradedObject.Monoidal.r₁₂₃ x = match x with | (i, j, k) => i + j + k
Instances For
Auxiliary definition for associator
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition for associator
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition for associator
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given three graded objects X₁
, X₂
, X₃
in GradedObject I C
, this is the
assumption that for all i₁₂ : I
and i₃ : I
, the tensor product functor - ⊗ X₃ i₃
commutes with the coproduct of the objects X₁ i₁ ⊗ X₂ i₂
such that i₁ + i₂ = i₁₂
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given three graded objects X₁
, X₂
, X₃
in GradedObject I C
, this is the
assumption that for all i₁ : I
and i₂₃ : I
, the tensor product functor X₁ i₁ ⊗ -
commutes with the coproduct of the objects X₂ i₂ ⊗ X₃ i₃
such that i₂ + i₃ = i₂₃
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The associator isomorphism for graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⟶ tensorObj X₁ (tensorObj X₂ X₃) j
when i₁ + i₂ + i₃ = j
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⟶ tensorObj (tensorObj X₁ X₂) X₃ j
when i₁ + i₂ + i₃ = j
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit of the tensor product on graded objects is (single₀ I).obj (𝟙_ C)
.
Equations
- CategoryTheory.GradedObject.Monoidal.tensorUnit = (CategoryTheory.GradedObject.single₀ I).obj (𝟙_ C)
Instances For
The canonical isomorphism tensorUnit 0 ≅ 𝟙_ C
Equations
- CategoryTheory.GradedObject.Monoidal.tensorUnit₀ = CategoryTheory.GradedObject.singleObjApplyIso 0 (𝟙_ C)
Instances For
tensorUnit i
is an initial object when i ≠ 0
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The left unitor isomorphism for graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The right unitor isomorphism for graded objects.
Equations
- One or more equations did not get rendered due to their size.