- tensor_obj : C → C → C
- tensor_hom : Π {X₁ Y₁ X₂ Y₂ : C}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (X₁ ⊗ X₂ ⟶ Y₁ ⊗ Y₂)
- tensor_id' : (∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)) . "obviously"
- tensor_comp' : (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂), f₁ ≫ g₁ ⊗ f₂ ≫ g₂ = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂)) . "obviously"
- tensor_unit : C
- associator : Π (X Y Z : C), (X ⊗ Y) ⊗ Z ≅ X ⊗ Y ⊗ Z
- associator_naturality' : (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)) . "obviously"
- left_unitor : Π (X : C), 𝟙_ C ⊗ X ≅ X
- left_unitor_naturality' : (∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f) . "obviously"
- right_unitor : Π (X : C), X ⊗ 𝟙_ C ≅ X
- right_unitor_naturality' : (∀ {X Y : C} (f : X ⟶ Y), (f ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f) . "obviously"
- pentagon' : (∀ (W X Y Z : C), ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ (α_ X Y Z).hom) = (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom) . "obviously"
- triangle' : (∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ (λ_ Y).hom) = (ρ_ X).hom ⊗ 𝟙 Y) . "obviously"
In a monoidal category, we can take the tensor product of objects, X ⊗ Y
and of morphisms f ⊗ g
.
Tensor product does not need to be strictly associative on objects, but there is a
specified associator, α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z)
. There is a tensor unit 𝟙_ C
,
with specified left and right unitor isomorphisms λ_ X : 𝟙_ C ⊗ X ≅ X
and ρ_ X : X ⊗ 𝟙_ C ≅ X
.
These associators and unitors satisfy the pentagon and triangle equations.
The tensor product of two isomorphisms is an isomorphism.
Equations
- category_theory.monoidal_category.tensor_is_iso f g = {inv := (category_theory.as_iso f ⊗ category_theory.as_iso g).inv, hom_inv_id' := _, inv_hom_id' := _}
The tensor product expressed as a functor.
The left-associated triple tensor product as a functor.
The right-associated triple tensor product as a functor.
The functor λ X, 𝟙_ C ⊗ X
.
The functor λ X, X ⊗ 𝟙_ C
.
The associator as a natural isomorphism.
The left unitor as a natural isomorphism.
Equations
The right unitor as a natural isomorphism.
Equations
Tensoring on the left with as fixed object, as a functor.
Tensoring on the left with X ⊗ Y
is naturally isomorphic to
tensoring on the left with Y
, and then again with X
.
Equations
Tensoring on the right with as fixed object, as a functor.
Tensoring on the right, as a functor from C
into endofunctors of C
.
We later show this is a monoidal functor.
Equations
- category_theory.monoidal_category.tensoring_right C = {obj := category_theory.monoidal_category.tensor_right _inst_2, map := λ (X Y : C) (f : X ⟶ Y), {app := λ (Z : C), 𝟙 Z ⊗ f, naturality' := _}, map_id' := _, map_comp' := _}
Equations
- _ = _
Tensoring on the right with X ⊗ Y
is naturally isomorphic to
tensoring on the right with X
, and then again with Y
.
Equations
- category_theory.monoidal_category.tensor_right_tensor X Y = category_theory.nat_iso.of_components (λ (Z : C), (α_ Z X Y).symm) _