# mathlib3documentation

category_theory.monoidal.category

# Monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A monoidal category is a category equipped with a tensor product, unitors, and an associator. In the definition, we provide the tensor product as a pair of functions

• `tensor_obj : C → C → C`
• `tensor_hom : (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → ((X₁ ⊗ X₂) ⟶ (Y₁ ⊗ Y₂))` and allow use of the overloaded notation `⊗` for both. The unitors and associator are provided componentwise.

The tensor product can be expressed as a functor via `tensor : C × C ⥤ C`. The unitors and associator are gathered together as natural isomorphisms in `left_unitor_nat_iso`, `right_unitor_nat_iso` and `associator_nat_iso`.

Some consequences of the definition are proved in other files, e.g. `(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom` in `category_theory.monoidal.unitors_equal`.

## Implementation #

Dealing with unitors and associators is painful, and at this stage we do not have a useful implementation of coherence for monoidal categories.

In an effort to lessen the pain, we put some effort into choosing the right `simp` lemmas. Generally, the rule is that the component index of a natural transformation "weighs more" in considering the complexity of an expression than does a structural isomorphism (associator, etc).

As an example when we prove Proposition 2.2.4 of http://www-math.mit.edu/~etingof/egnobookfinal.pdf we state it as a `@[simp]` lemma as

``````(λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ⊗ (𝟙 Y)
``````

This is far from completely effective, but seems to prove a useful principle.

## References #

@[class]
structure category_theory.monoidal_category (C : Type u) [𝒞 : category_theory.category C] :
Type (max u v)

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.monoidal_category`
• category_theory.monoidal_category.has_sizeof_inst
@[simp]
theorem category_theory.monoidal_category.tensor_id {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (X₁ X₂ : C) :
𝟙 X₁ 𝟙 X₂ = 𝟙 (X₁ X₂)
@[simp]
theorem category_theory.monoidal_category.tensor_comp {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {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₂)
theorem category_theory.monoidal_category.tensor_comp_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) {X' : C} (f' : Z₁ Z₂ X') :
(f₁ g₁ f₂ g₂) f' = (f₁ f₂) (g₁ g₂) f'
theorem category_theory.monoidal_category.associator_naturality {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {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₃)
theorem category_theory.monoidal_category.associator_naturality_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {X' : C} (f' : Y₁ Y₂ Y₃ X') :
((f₁ f₂) f₃) (α_ Y₁ Y₂ Y₃).hom f' = (α_ X₁ X₂ X₃).hom (f₁ f₂ f₃) f'
theorem category_theory.monoidal_category.left_unitor_naturality_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
(𝟙 (𝟙_ C) f) (λ_ Y).hom f' = (λ_ X).hom f f'
theorem category_theory.monoidal_category.right_unitor_naturality_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
(f 𝟙 (𝟙_ C)) (ρ_ Y).hom f' = (ρ_ X).hom f f'
theorem category_theory.monoidal_category.pentagon {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (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
@[simp]
theorem category_theory.monoidal_category.pentagon_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (W X Y Z : C) {X' : C} (f' : W X Y Z X') :
((α_ W X Y).hom 𝟙 Z) (α_ W (X Y) Z).hom (𝟙 W (α_ X Y Z).hom) f' = (α_ (W X) Y Z).hom (α_ W X (Y Z)).hom f'
@[simp]
theorem category_theory.monoidal_category.triangle_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (X Y : C) {X' : C} (f' : X Y X') :
(α_ X (𝟙_ C) Y).hom (𝟙 X (λ_ Y).hom) f' = ((ρ_ X).hom 𝟙 Y) f'
@[simp]
theorem category_theory.tensor_iso_hom {C : Type u} {X Y X' Y' : C} (f : X Y) (g : X' Y') :
(f g).hom = f.hom g.hom
@[simp]
theorem category_theory.tensor_iso_inv {C : Type u} {X Y X' Y' : C} (f : X Y) (g : X' Y') :
(f g).inv = f.inv g.inv
def category_theory.tensor_iso {C : Type u} {X Y X' Y' : C} (f : X Y) (g : X' Y') :
X X' Y Y'

The tensor product of two isomorphisms is an isomorphism.

Equations
@[protected, instance]
def category_theory.monoidal_category.tensor_is_iso {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z)  :
@[simp]
theorem category_theory.monoidal_category.inv_tensor {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z)  :
theorem category_theory.monoidal_category.tensor_dite {C : Type u} {P : Prop} [decidable P] {W X Y Z : C} (f : W X) (g : P (Y Z)) (g' : ¬P (Y Z)) :
f dite P (λ (h : P), g h) (λ (h : ¬P), g' h) = dite P (λ (h : P), f g h) (λ (h : ¬P), f g' h)
theorem category_theory.monoidal_category.dite_tensor {C : Type u} {P : Prop} [decidable P] {W X Y Z : C} (f : W X) (g : P (Y Z)) (g' : ¬P (Y Z)) :
dite P (λ (h : P), g h) (λ (h : ¬P), g' h) f = dite P (λ (h : P), g h f) (λ (h : ¬P), g' h f)
@[simp]
theorem category_theory.monoidal_category.comp_tensor_id {C : Type u} {W X Y Z : C} (f : W X) (g : X Y) :
f g 𝟙 Z = (f 𝟙 Z) (g 𝟙 Z)
theorem category_theory.monoidal_category.comp_tensor_id_assoc {C : Type u} {W X Y Z : C} (f : W X) (g : X Y) {X' : C} (f' : Y Z X') :
(f g 𝟙 Z) f' = (f 𝟙 Z) (g 𝟙 Z) f'
@[simp]
theorem category_theory.monoidal_category.id_tensor_comp {C : Type u} {W X Y Z : C} (f : W X) (g : X Y) :
𝟙 Z f g = (𝟙 Z f) (𝟙 Z g)
theorem category_theory.monoidal_category.id_tensor_comp_assoc {C : Type u} {W X Y Z : C} (f : W X) (g : X Y) {X' : C} (f' : Z Y X') :
(𝟙 Z f g) f' = (𝟙 Z f) (𝟙 Z g) f'
@[simp]
theorem category_theory.monoidal_category.id_tensor_comp_tensor_id {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z) :
(𝟙 Y f) (g 𝟙 X) = g f
@[simp]
theorem category_theory.monoidal_category.id_tensor_comp_tensor_id_assoc {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z) {X' : C} (f' : Z X X') :
(𝟙 Y f) (g 𝟙 X) f' = (g f) f'
@[simp]
theorem category_theory.monoidal_category.tensor_id_comp_id_tensor {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z) :
(g 𝟙 W) (𝟙 Z f) = g f
@[simp]
theorem category_theory.monoidal_category.tensor_id_comp_id_tensor_assoc {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z) {X' : C} (f' : Z X X') :
(g 𝟙 W) (𝟙 Z f) f' = (g f) f'
@[simp]
theorem category_theory.monoidal_category.right_unitor_conjugation {C : Type u} {X Y : C} (f : X Y) :
f 𝟙 (𝟙_ C) = (ρ_ X).hom f (ρ_ Y).inv
@[simp]
theorem category_theory.monoidal_category.left_unitor_conjugation {C : Type u} {X Y : C} (f : X Y) :
𝟙 (𝟙_ C) f = (λ_ X).hom f (λ_ Y).inv
theorem category_theory.monoidal_category.left_unitor_inv_naturality {C : Type u} {X X' : C} (f : X X') :
f (λ_ X').inv = (λ_ X).inv (𝟙 (𝟙_ C) f)
theorem category_theory.monoidal_category.left_unitor_inv_naturality_assoc {C : Type u} {X X' : C} (f : X X') {X'_1 : C} (f' : 𝟙_ C X' X'_1) :
f (λ_ X').inv f' = (λ_ X).inv (𝟙 (𝟙_ C) f) f'
theorem category_theory.monoidal_category.right_unitor_inv_naturality_assoc {C : Type u} {X X' : C} (f : X X') {X'_1 : C} (f' : X' 𝟙_ C X'_1) :
f (ρ_ X').inv f' = (ρ_ X).inv (f 𝟙 (𝟙_ C)) f'
theorem category_theory.monoidal_category.right_unitor_inv_naturality {C : Type u} {X X' : C} (f : X X') :
f (ρ_ X').inv = (ρ_ X).inv (f 𝟙 (𝟙_ C))
theorem category_theory.monoidal_category.tensor_left_iff {C : Type u} {X Y : C} (f g : X Y) :
𝟙 (𝟙_ C) f = 𝟙 (𝟙_ C) g f = g
theorem category_theory.monoidal_category.tensor_right_iff {C : Type u} {X Y : C} (f g : X Y) :
f 𝟙 (𝟙_ C) = g 𝟙 (𝟙_ C) f = g

The lemmas in the next section are true by coherence, but we prove them directly as they are used in proving the coherence theorem.

theorem category_theory.monoidal_category.pentagon_inv {C : Type u} (W X Y Z : C) :
(𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) = (α_ W X (Y Z)).inv (α_ (W X) Y Z).inv
theorem category_theory.monoidal_category.pentagon_inv_assoc {C : Type u} (W X Y Z : C) {X' : C} (f' : ((W X) Y) Z X') :
(𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) f' = (α_ W X (Y Z)).inv (α_ (W X) Y Z).inv f'
@[simp]
theorem category_theory.monoidal_category.right_unitor_tensor {C : Type u} (X Y : C) :
(ρ_ (X Y)).hom = (α_ X Y (𝟙_ C)).hom (𝟙 X (ρ_ Y).hom)
theorem category_theory.monoidal_category.right_unitor_tensor_assoc {C : Type u} (X Y : C) {X' : C} (f' : X Y X') :
(ρ_ (X Y)).hom f' = (α_ X Y (𝟙_ C)).hom (𝟙 X (ρ_ Y).hom) f'
theorem category_theory.monoidal_category.right_unitor_tensor_inv_assoc {C : Type u} (X Y : C) {X' : C} (f' : (X Y) 𝟙_ C X') :
(ρ_ (X Y)).inv f' = (𝟙 X (ρ_ Y).inv) (α_ X Y (𝟙_ C)).inv f'
@[simp]
theorem category_theory.monoidal_category.right_unitor_tensor_inv {C : Type u} (X Y : C) :
(ρ_ (X Y)).inv = (𝟙 X (ρ_ Y).inv) (α_ X Y (𝟙_ C)).inv
@[simp]
@[simp]
theorem category_theory.monoidal_category.triangle_assoc_comp_right_assoc {C : Type u} (X Y : C) {X' : C} (f' : X Y X') :
(α_ X (𝟙_ C) Y).inv ((ρ_ X).hom 𝟙 Y) f' = (𝟙 X (λ_ Y).hom) f'
@[simp]
theorem category_theory.monoidal_category.triangle_assoc_comp_left_inv_assoc {C : Type u} (X Y : C) {X' : C} (f' : (X 𝟙_ C) Y X') :
(𝟙 X (λ_ Y).inv) (α_ X (𝟙_ C) Y).inv f' = ((ρ_ X).inv 𝟙 Y) f'
@[simp]
theorem category_theory.monoidal_category.associator_inv_naturality_assoc {C : Type u} {X Y Z X' Y' Z' : C} (f : X X') (g : Y Y') (h : Z Z') {X'_1 : C} (f' : (X' Y') Z' X'_1) :
(f g h) (α_ X' Y' Z').inv f' = (α_ X Y Z).inv ((f g) h) f'
theorem category_theory.monoidal_category.associator_inv_naturality {C : Type u} {X Y Z X' Y' Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
(f g h) (α_ X' Y' Z').inv = (α_ X Y Z).inv ((f g) h)
theorem category_theory.monoidal_category.associator_conjugation_assoc {C : Type u} {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') {X'_1 : C} (f' : (X' Y') Z' X'_1) :
((f g) h) f' = (α_ X Y Z).hom (f g h) (α_ X' Y' Z').inv f'
@[simp]
theorem category_theory.monoidal_category.associator_conjugation {C : Type u} {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
(f g) h = (α_ X Y Z).hom (f g h) (α_ X' Y' Z').inv
theorem category_theory.monoidal_category.associator_inv_conjugation_assoc {C : Type u} {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') {X'_1 : C} (f' : X' Y' Z' X'_1) :
(f g h) f' = (α_ X Y Z).inv ((f g) h) (α_ X' Y' Z').hom f'
theorem category_theory.monoidal_category.associator_inv_conjugation {C : Type u} {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
f g h = (α_ X Y Z).inv ((f g) h) (α_ X' Y' Z').hom
theorem category_theory.monoidal_category.id_tensor_associator_naturality {C : Type u} {X Y Z Z' : C} (h : Z Z') :
(𝟙 (X Y) h) (α_ X Y Z').hom = (α_ X Y Z).hom (𝟙 X 𝟙 Y h)
theorem category_theory.monoidal_category.id_tensor_associator_naturality_assoc {C : Type u} {X Y Z Z' : C} (h : Z Z') {X' : C} (f' : X Y Z' X') :
(𝟙 (X Y) h) (α_ X Y Z').hom f' = (α_ X Y Z).hom (𝟙 X 𝟙 Y h) f'
theorem category_theory.monoidal_category.id_tensor_associator_inv_naturality_assoc {C : Type u} {X Y Z X' : C} (f : X X') {X'_1 : C} (f' : (X' Y) Z X'_1) :
(f 𝟙 (Y Z)) (α_ X' Y Z).inv f' = (α_ X Y Z).inv ((f 𝟙 Y) 𝟙 Z) f'
theorem category_theory.monoidal_category.id_tensor_associator_inv_naturality {C : Type u} {X Y Z X' : C} (f : X X') :
(f 𝟙 (Y Z)) (α_ X' Y Z).inv = (α_ X Y Z).inv ((f 𝟙 Y) 𝟙 Z)
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : V Z X') :
(f.hom g) (f.inv h) f' = (𝟙 V g) (𝟙 V h) f'
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(f.hom g) (f.inv h) = (𝟙 V g) (𝟙 V h)
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(f.inv g) (f.hom h) = (𝟙 W g) (𝟙 W h)
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : W Z X') :
(f.inv g) (f.hom h) f' = (𝟙 W g) (𝟙 W h) f'
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : Z V X') :
(g f.hom) (h f.inv) f' = (g 𝟙 V) (h 𝟙 V) f'
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(g f.hom) (h f.inv) = (g 𝟙 V) (h 𝟙 V)
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : Z W X') :
(g f.inv) (h f.hom) f' = (g 𝟙 W) (h 𝟙 W) f'
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(g f.inv) (h f.hom) = (g 𝟙 W) (h 𝟙 W)
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor'_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : V Z X') :
(f g) h) f' = (𝟙 V g) (𝟙 V h) f'
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor' {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(f g) h) = (𝟙 V g) (𝟙 V h)
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor'_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : W Z X') :
g) (f h) f' = (𝟙 W g) (𝟙 W h) f'
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor' {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
g) (f h) = (𝟙 W g) (𝟙 W h)
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id'_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : Z V X') :
(g f) (h f' = (g 𝟙 V) (h 𝟙 V) f'
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id' {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(g f) (h = (g 𝟙 V) (h 𝟙 V)
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id' {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(g (h f) = (g 𝟙 W) (h 𝟙 W)
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id'_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : Z W X') :
(g (h f) f' = (g 𝟙 W) (h 𝟙 W) f'

The tensor product expressed as a functor.

Equations
@[simp]
theorem category_theory.monoidal_category.tensor_map (C : Type u) {X Y : C × C} (f : X Y) :
= f.fst f.snd
@[simp]

The left-associated triple tensor product as a functor.

Equations
@[simp]
@[simp]
theorem category_theory.monoidal_category.left_assoc_tensor_map (C : Type u) {X Y : C × C × C} (f : X Y) :
= (f.fst f.snd.fst) f.snd.snd

The right-associated triple tensor product as a functor.

Equations
@[simp]
theorem category_theory.monoidal_category.right_assoc_tensor_map (C : Type u) {X Y : C × C × C} (f : X Y) :

The functor `λ X, 𝟙_ C ⊗ X`.

Equations

The functor `λ X, X ⊗ 𝟙_ C`.

Equations

The associator as a natural isomorphism.

Equations
@[simp]
@[simp]

The left unitor as a natural isomorphism.

Equations
@[simp]

The right unitor as a natural isomorphism.

Equations
@[simp]
@[simp]
theorem category_theory.monoidal_category.tensor_left_map {C : Type u} (X Y Y' : C) (f : Y Y') :
@[simp]

Tensoring on the left with a fixed object, as a functor.

Equations
Instances for `category_theory.monoidal_category.tensor_left`

Tensoring on the left with `X ⊗ Y` is naturally isomorphic to tensoring on the left with `Y`, and then again with `X`.

Equations
@[simp]
@[simp]
@[simp]

Tensoring on the right with a fixed object, as a functor.

Equations
Instances for `category_theory.monoidal_category.tensor_right`
@[simp]
theorem category_theory.monoidal_category.tensor_right_map {C : Type u} (X Y Y' : C) (f : Y Y') :

Tensoring on the left, as a functor from `C` into endofunctors of `C`.

TODO: show this is a op-monoidal functor.

Equations
Instances for `category_theory.monoidal_category.tensoring_left`
@[simp]
@[simp]
theorem category_theory.monoidal_category.tensoring_left_map_app (C : Type u) (X Y : C) (f : X Y) (Z : C) :
= f 𝟙 Z
@[protected, instance]
@[simp]
@[simp]
theorem category_theory.monoidal_category.tensoring_right_map_app (C : Type u) (X Y : C) (f : X Y) (Z : C) :
= 𝟙 Z f

Tensoring on the right, as a functor from `C` into endofunctors of `C`.

We later show this is a monoidal functor.

Equations
Instances for `category_theory.monoidal_category.tensoring_right`
@[protected, instance]

Tensoring on the right with `X ⊗ Y` is naturally isomorphic to tensoring on the right with `X`, and then again with `Y`.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_tensor_hom (C₁ : Type u₁) (C₂ : Type u₂) (_x _x_1 _x_2 _x_3 : C₁ × C₂) (f : _x _x_1) (g : _x_2 _x_3) :
f g = (f.fst g.fst, f.snd g.snd)
@[protected, instance]
def category_theory.monoidal_category.prod_monoidal (C₁ : Type u₁) (C₂ : Type u₂)  :
Equations
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_associator (C₁ : Type u₁) (C₂ : Type u₂) (X Y Z : C₁ × C₂) :
α_ X Y Z = (α_ X.fst Y.fst Z.fst).prod (α_ X.snd Y.snd Z.snd)
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_tensor_unit (C₁ : Type u₁) (C₂ : Type u₂)  :
𝟙_ (C₁ × C₂) = (𝟙_ C₁ _inst_2, 𝟙_ C₂ _inst_4)
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_tensor_obj (C₁ : Type u₁) (C₂ : Type u₂) (X Y : C₁ × C₂) :
X Y = (X.fst Y.fst, X.snd Y.snd)
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_left_unitor_hom_fst (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(λ_ X).hom.fst = (λ_ X.fst).hom
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_left_unitor_hom_snd (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(λ_ X).hom.snd = (λ_ X.snd).hom
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_left_unitor_inv_fst (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(λ_ X).inv.fst = (λ_ X.fst).inv
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_left_unitor_inv_snd (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(λ_ X).inv.snd = (λ_ X.snd).inv
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_right_unitor_hom_fst (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(ρ_ X).hom.fst = (ρ_ X.fst).hom
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_right_unitor_hom_snd (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(ρ_ X).hom.snd = (ρ_ X.snd).hom
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_right_unitor_inv_fst (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(ρ_ X).inv.fst = (ρ_ X.fst).inv
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_right_unitor_inv_snd (C₁ : Type u₁) (C₂ : Type u₂) (X : C₁ × C₂) :
(ρ_ X).inv.snd = (ρ_ X.snd).inv