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
.
Under suitable assumptions about the existence of coproducts and the
preservation of certain coproducts by the tensor products in C
, we
obtain a monoidal category structure on GradedObject I C
.
In particular, if C
has finite coproducts to which the tensor
product commutes, we obtain a monoidal category structure on GradedObject ℕ C
.
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
The isomorphism tensorObj X₁ Y₁ ≅ tensorObj X₂ Y₂
induced by isomorphisms of graded
objects e : X₁ ≅ X₂
and e' : Y₁ ≅ Y₂
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is the addition map I × I × I → I
for an additive monoid I
.
Equations
- CategoryTheory.GradedObject.Monoidal.r₁₂₃ (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 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 associator isomorphism for graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given Z : C
and three graded objects X₁
, X₂
and X₃
in GradedObject I C
,
this typeclass expresses that functor Z ⊗ _
commutes with the coproduct of
the objects X₁ i₁ ⊗ (X₂ i₂ ⊗ X₃ i₃)
such that i₁ + i₂ + i₃ = j
for a certain j
.
See lemma left_tensor_tensorObj₃_ext
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion
X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⊗ X₄ i₄ ⟶ tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j
when i₁ + i₂ + i₃ + i₄ = j
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given four graded objects, this is the condition
HasLeftTensor₃ObjExt (X₁ i₁) X₂ X₃ X₄ i₂₃₄
for all indices i₁
and i₂₃₄
,
see the lemma tensorObj₄_ext
.
Equations
- X₁.HasTensor₄ObjExt X₂ X₃ X₄ = ∀ (i₁ i₂₃₄ : I), CategoryTheory.GradedObject.HasLeftTensor₃ObjExt (X₁ i₁) X₂ X₃ X₄ i₂₃₄
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
The left unitor isomorphism for graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right unitor isomorphism for graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.GradedObject.monoidalCategory = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The monoidal category structure on GradedObject ℕ C
can be inferred
from the assumptions [HasFiniteCoproducts C]
,
[∀ (X : C), PreservesFiniteCoproducts ((curriedTensor C).obj X)]
and
[∀ (X : C), PreservesFiniteCoproducts ((curriedTensor C).flip.obj X)]
.
This requires importing Mathlib.CategoryTheory.Limits.Preserves.Finite
.