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.
@[reducible, inline]
abbrev
CategoryTheory.GradedObject.HasTensor
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
(X₁ : CategoryTheory.GradedObject I C)
(X₂ : CategoryTheory.GradedObject I 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
@[reducible, inline]
noncomputable abbrev
CategoryTheory.GradedObject.Monoidal.tensorObj
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
(X₁ : CategoryTheory.GradedObject I C)
(X₂ : CategoryTheory.GradedObject I C)
[X₁.HasTensor X₂]
:
The tensor product of two graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.GradedObject.Monoidal.ιTensorObj
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
(X₁ : CategoryTheory.GradedObject I C)
(X₂ : CategoryTheory.GradedObject I C)
[X₁.HasTensor X₂]
(i₁ : I)
(i₂ : I)
(i₁₂ : I)
(h : i₁ + i₂ = i₁₂)
:
CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ i₁₂
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
theorem
CategoryTheory.GradedObject.Monoidal.tensorObj_ext
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
[X₁.HasTensor X₂]
{A : C}
{j : I}
(f : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A)
(g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A)
(h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) g)
:
f = g
noncomputable def
CategoryTheory.GradedObject.Monoidal.tensorObjDesc
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
[X₁.HasTensor X₂]
{A : C}
{k : I}
(f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A))
:
Constructor for morphisms from a tensor product of two graded objects.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc_assoc
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
[X₁.HasTensor X₂]
{A : C}
{k : I}
(f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A))
(i₁ : I)
(i₂ : I)
(hi : i₁ + i₂ = k)
{Z : C}
(h : A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
[X₁.HasTensor X₂]
{A : C}
{k : I}
(f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A))
(i₁ : I)
(i₂ : I)
(hi : i₁ + i₂ = k)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi)
(CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) = f i₁ i₂ hi
noncomputable def
CategoryTheory.GradedObject.Monoidal.tensorHom
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
[X₁.HasTensor Y₁]
[X₂.HasTensor Y₂]
:
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
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.ι_tensorHom_assoc
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
[X₁.HasTensor Y₁]
[X₂.HasTensor Y₂]
(i₁ : I)
(i₂ : I)
(i₁₂ : I)
(h : i₁ + i₂ = i₁₂)
{Z : C}
(h : CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y₂ i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f i₁) (g i₂))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h✝) h)
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.ι_tensorHom
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
[X₁.HasTensor Y₁]
[X₂.HasTensor Y₂]
(i₁ : I)
(i₂ : I)
(i₁₂ : I)
(h : i₁ + i₂ = i₁₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h)
(CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f i₁) (g i₂))
(CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)
@[reducible, inline]
noncomputable abbrev
CategoryTheory.GradedObject.Monoidal.whiskerLeft
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
(X : CategoryTheory.GradedObject I C)
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
(φ : Y₁ ⟶ Y₂)
[X.HasTensor Y₁]
[X.HasTensor Y₂]
:
The morphism tensorObj X Y₁ ⟶ tensorObj X Y₂ induced by a morphism of graded objects
φ : Y₁ ⟶ Y₂.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.GradedObject.Monoidal.whiskerRight
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
(φ : X₁ ⟶ X₂)
(Y : CategoryTheory.GradedObject I C)
[X₁.HasTensor Y]
[X₂.HasTensor Y]
:
The morphism tensorObj X₁ Y ⟶ tensorObj X₂ Y induced by a morphism of graded objects
φ : X₁ ⟶ X₂.
Equations
Instances For
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.tensor_id
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
(X : CategoryTheory.GradedObject I C)
(Y : CategoryTheory.GradedObject I C)
[X.HasTensor Y]
:
theorem
CategoryTheory.GradedObject.Monoidal.tensor_comp_assoc
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
{X₃ : CategoryTheory.GradedObject I C}
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
{Y₃ : CategoryTheory.GradedObject I C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
[X₁.HasTensor Y₁]
[X₂.HasTensor Y₂]
[X₃.HasTensor Y₃]
{Z : CategoryTheory.GradedObject I C}
(h : CategoryTheory.GradedObject.Monoidal.tensorObj X₃ Y₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
(CategoryTheory.CategoryStruct.comp g₁ g₂))
h = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂) h)
theorem
CategoryTheory.GradedObject.Monoidal.tensor_comp
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
{X₃ : CategoryTheory.GradedObject I C}
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
{Y₃ : CategoryTheory.GradedObject I C}
(f₁ : X₁ ⟶ X₂)
(f₂ : X₂ ⟶ X₃)
(g₁ : Y₁ ⟶ Y₂)
(g₂ : Y₂ ⟶ Y₃)
[X₁.HasTensor Y₁]
[X₂.HasTensor Y₂]
[X₃.HasTensor Y₃]
:
theorem
CategoryTheory.GradedObject.Monoidal.tensorHom_def
{I : Type u}
[AddMonoid I]
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
{X₁ : CategoryTheory.GradedObject I C}
{X₂ : CategoryTheory.GradedObject I C}
{Y₁ : CategoryTheory.GradedObject I C}
{Y₂ : CategoryTheory.GradedObject I C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
[X₁.HasTensor Y₁]
[X₂.HasTensor Y₂]
[X₂.HasTensor Y₁]
: