mathlib documentation

category_theory.monoidal.category

@[class]

structure category_theory.monoidal_category (C : Type u) [𝒞 : category_theory.category C] :

Type (max u v)

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.

See https://stacks.math.columbia.edu/tag/0FFK.

Instances

@[simp]

theorem category_theory.tensor_iso_hom {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category 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} [category_theory.category C] [category_theory.monoidal_category 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} [category_theory.category C] [category_theory.monoidal_category C] (f : X ≅ Y) (g : X' ≅ Y') :

X ⊗ X' ≅ Y ⊗ Y'

The tensor product of two isomorphisms is an isomorphism.

Equations

f ⊗ g = {hom := f.hom ⊗ g.hom, inv := f.inv ⊗ g.inv, hom_inv_id' := _, inv_hom_id' := _}

@[instance]

def category_theory.monoidal_category.tensor_is_iso {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W ⟶ X) [category_theory.is_iso f] (g : Y ⟶ Z) [category_theory.is_iso g] :

category_theory.is_iso (f ⊗ g)

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' := _}

@[simp]

theorem category_theory.monoidal_category.inv_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W ⟶ X) [category_theory.is_iso f] (g : Y ⟶ Z) [category_theory.is_iso g] :

category_theory.is_iso.inv (f ⊗ g) = (category_theory.is_iso.inv f ⊗ category_theory.is_iso.inv g)

@[simp]

theorem category_theory.monoidal_category.comp_tensor_id {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) :

f ≫ g ⊗ 𝟙 Z = (f ⊗ 𝟙 Z) ≫ (g ⊗ 𝟙 Z)

@[simp]

theorem category_theory.monoidal_category.id_tensor_comp {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) :

𝟙 Z ⊗ f ≫ g = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g)

@[simp]

theorem category_theory.monoidal_category.id_tensor_comp_tensor_id {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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'

theorem category_theory.monoidal_category.left_unitor_inv_naturality {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' : C} (f : X ⟶ X') :

f ≫ (λ_ X').inv = (λ_ X).inv ≫ (𝟙 (𝟙_ C) ⊗ f)

theorem category_theory.monoidal_category.right_unitor_inv_naturality {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' : C} (f : X ⟶ X') :

f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ⊗ 𝟙 (𝟙_ C))

@[simp]

theorem category_theory.monoidal_category.right_unitor_conjugation {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y : C} (f : X ⟶ Y) :

(ρ_ X).inv ≫ (f ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = f

@[simp]

theorem category_theory.monoidal_category.left_unitor_conjugation {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y : C} (f : X ⟶ Y) :

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

@[simp]

theorem category_theory.monoidal_category.tensor_left_iff {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y : C} (f g : X ⟶ Y) :

𝟙 (𝟙_ C) ⊗ f = (𝟙 (𝟙_ C) ⊗ g) ↔ f = g

@[simp]

theorem category_theory.monoidal_category.tensor_right_iff {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y : C} (f g : X ⟶ Y) :

f ⊗ 𝟙 (𝟙_ C) = (g ⊗ 𝟙 (𝟙_ C)) ↔ f = g

theorem category_theory.monoidal_category.left_unitor_product_aux_perimeter {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.left_unitor_product_aux_triangle {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.left_unitor_product_aux_square {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.left_unitor_product_aux {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.right_unitor_product_aux_perimeter {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.right_unitor_product_aux_triangle {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.right_unitor_product_aux_square {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(α_ X (Y ⊗ 𝟙_ C) (𝟙_ C)).hom ≫ (𝟙 X ⊗ ((ρ_ Y).hom ⊗ 𝟙 (𝟙_ C))) = (𝟙 X ⊗ (ρ_ Y).hom ⊗ 𝟙 (𝟙_ C)) ≫ (α_ X Y (𝟙_ C)).hom

theorem category_theory.monoidal_category.right_unitor_product_aux {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

((α_ X Y (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫ (𝟙 X ⊗ (ρ_ Y).hom ⊗ 𝟙 (𝟙_ C)) = ((ρ_ (X ⊗ Y)).hom ⊗ 𝟙 (𝟙_ C))

theorem category_theory.monoidal_category.left_unitor_tensor' {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

@[simp]

theorem category_theory.monoidal_category.left_unitor_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.left_unitor_tensor_inv' {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

@[simp]

theorem category_theory.monoidal_category.left_unitor_tensor_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

@[simp]

theorem category_theory.monoidal_category.right_unitor_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ (𝟙 X ⊗ (ρ_ Y).hom)

@[simp]

theorem category_theory.monoidal_category.right_unitor_tensor_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(ρ_ (X ⊗ Y)).inv = (𝟙 X ⊗ (ρ_ Y).inv) ≫ (α_ X Y (𝟙_ C)).inv

theorem category_theory.monoidal_category.associator_inv_naturality {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {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.pentagon_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (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.triangle_assoc_comp_left {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

@[simp]

theorem category_theory.monoidal_category.triangle_assoc_comp_right {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

@[simp]

theorem category_theory.monoidal_category.triangle_assoc_comp_right_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

@[simp]

theorem category_theory.monoidal_category.triangle_assoc_comp_left_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

def category_theory.monoidal_category.tensor (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

C × C ⥤ C

The tensor product expressed as a functor.

Equations

category_theory.monoidal_category.tensor C = {obj := λ (X : C × C), X.fst ⊗ X.snd, map := λ {X Y : C × C} (f : X ⟶ Y), f.fst ⊗ f.snd, map_id' := _, map_comp' := _}

def category_theory.monoidal_category.left_assoc_tensor (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

C × C × C ⥤ C

The left-associated triple tensor product as a functor.

Equations

category_theory.monoidal_category.left_assoc_tensor C = {obj := λ (X : C × C × C), X.fst ⊗ X.snd.fst ⊗ X.snd.snd, map := λ {X Y : C × C × C} (f : X ⟶ Y), f.fst ⊗ f.snd.fst ⊗ f.snd.snd, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.monoidal_category.left_assoc_tensor_obj (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C × C × C) :

(category_theory.monoidal_category.left_assoc_tensor C).obj X = (X.fst ⊗ X.snd.fst ⊗ X.snd.snd)

@[simp]

theorem category_theory.monoidal_category.left_assoc_tensor_map (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] {X Y : C × C × C} (f : X ⟶ Y) :

(category_theory.monoidal_category.left_assoc_tensor C).map f = (f.fst ⊗ f.snd.fst ⊗ f.snd.snd)

def category_theory.monoidal_category.right_assoc_tensor (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

C × C × C ⥤ C

The right-associated triple tensor product as a functor.

Equations

category_theory.monoidal_category.right_assoc_tensor C = {obj := λ (X : C × C × C), X.fst ⊗ (X.snd.fst ⊗ X.snd.snd), map := λ {X Y : C × C × C} (f : X ⟶ Y), f.fst ⊗ (f.snd.fst ⊗ f.snd.snd), map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.monoidal_category.right_assoc_tensor_obj (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C × C × C) :

(category_theory.monoidal_category.right_assoc_tensor C).obj X = (X.fst ⊗ (X.snd.fst ⊗ X.snd.snd))

@[simp]

theorem category_theory.monoidal_category.right_assoc_tensor_map (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] {X Y : C × C × C} (f : X ⟶ Y) :

(category_theory.monoidal_category.right_assoc_tensor C).map f = (f.fst ⊗ (f.snd.fst ⊗ f.snd.snd))

def category_theory.monoidal_category.tensor_unit_left (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

C ⥤ C

The functor λ X, 𝟙_ C ⊗ X.

Equations

category_theory.monoidal_category.tensor_unit_left C = {obj := λ (X : C), 𝟙_ C ⊗ X, map := λ {X Y : C} (f : X ⟶ Y), 𝟙 (𝟙_ C) ⊗ f, map_id' := _, map_comp' := _}

def category_theory.monoidal_category.tensor_unit_right (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

C ⥤ C

The functor λ X, X ⊗ 𝟙_ C.

Equations

category_theory.monoidal_category.tensor_unit_right C = {obj := λ (X : C), X ⊗ 𝟙_ C, map := λ {X Y : C} (f : X ⟶ Y), f ⊗ 𝟙 (𝟙_ C), map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.monoidal_category.associator_nat_iso_inv_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C × C × C) :

(category_theory.monoidal_category.associator_nat_iso C).inv.app X = category_theory.is_iso.inv ({app := λ (X : C × C × C), ((λ (X : C × C × C), α_ X.fst X.snd.fst X.snd.snd) X).hom, naturality' := _}.app X)

def category_theory.monoidal_category.associator_nat_iso (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_category.left_assoc_tensor C ≅ category_theory.monoidal_category.right_assoc_tensor C

The associator as a natural isomorphism.

Equations

category_theory.monoidal_category.associator_nat_iso C = category_theory.nat_iso.of_components (λ (X : C × C × C), α_ X.fst X.snd.fst X.snd.snd) _

@[simp]

theorem category_theory.monoidal_category.associator_nat_iso_hom_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C × C × C) :

(category_theory.monoidal_category.associator_nat_iso C).hom.app X = ((λ (X : C × C × C), α_ X.fst X.snd.fst X.snd.snd) X).hom

@[simp]

theorem category_theory.monoidal_category.left_unitor_nat_iso_inv_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

(category_theory.monoidal_category.left_unitor_nat_iso C).inv.app X = category_theory.is_iso.inv ({app := λ (X : C), ((λ (X : C), λ_ X) X).hom, naturality' := _}.app X)

@[simp]

theorem category_theory.monoidal_category.left_unitor_nat_iso_hom_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

(category_theory.monoidal_category.left_unitor_nat_iso C).hom.app X = ((λ (X : C), λ_ X) X).hom

def category_theory.monoidal_category.left_unitor_nat_iso (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_category.tensor_unit_left C ≅ 𝟭 C

The left unitor as a natural isomorphism.

Equations

category_theory.monoidal_category.left_unitor_nat_iso C = category_theory.nat_iso.of_components (λ (X : C), λ_ X) _

@[simp]

theorem category_theory.monoidal_category.right_unitor_nat_iso_inv_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

(category_theory.monoidal_category.right_unitor_nat_iso C).inv.app X = category_theory.is_iso.inv ({app := λ (X : C), ((λ (X : C), ρ_ X) X).hom, naturality' := _}.app X)

def category_theory.monoidal_category.right_unitor_nat_iso (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_category.tensor_unit_right C ≅ 𝟭 C

The right unitor as a natural isomorphism.

Equations

category_theory.monoidal_category.right_unitor_nat_iso C = category_theory.nat_iso.of_components (λ (X : C), ρ_ X) _

@[simp]

theorem category_theory.monoidal_category.right_unitor_nat_iso_hom_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

(category_theory.monoidal_category.right_unitor_nat_iso C).hom.app X = ((λ (X : C), ρ_ X) X).hom

@[simp]

theorem category_theory.monoidal_category.tensor_left_map {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y Y' : C) (f : Y ⟶ Y') :

(category_theory.monoidal_category.tensor_left X).map f = (𝟙 X ⊗ f)

@[simp]

theorem category_theory.monoidal_category.tensor_left_obj {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.monoidal_category.tensor_left X).obj Y = (X ⊗ Y)

def category_theory.monoidal_category.tensor_left {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

C ⥤ C

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

Equations

category_theory.monoidal_category.tensor_left X = {obj := λ (Y : C), X ⊗ Y, map := λ (Y Y' : C) (f : Y ⟶ Y'), 𝟙 X ⊗ f, map_id' := _, map_comp' := _}

def category_theory.monoidal_category.tensor_left_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

category_theory.monoidal_category.tensor_left (X ⊗ Y) ≅ category_theory.monoidal_category.tensor_left Y ⋙ category_theory.monoidal_category.tensor_left X

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

Equations

category_theory.monoidal_category.tensor_left_tensor X Y = category_theory.nat_iso.of_components (α_ X Y) _

@[simp]

theorem category_theory.monoidal_category.tensor_left_tensor_hom_app {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : C) :

(category_theory.monoidal_category.tensor_left_tensor X Y).hom.app Z = (α_ X Y Z).hom

@[simp]

theorem category_theory.monoidal_category.tensor_left_tensor_inv_app {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : C) :

(category_theory.monoidal_category.tensor_left_tensor X Y).inv.app Z = (α_ X Y Z).inv

@[simp]

theorem category_theory.monoidal_category.tensor_right_obj {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.monoidal_category.tensor_right X).obj Y = (Y ⊗ X)

def category_theory.monoidal_category.tensor_right {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

C ⥤ C

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

Equations

category_theory.monoidal_category.tensor_right X = {obj := λ (Y : C), Y ⊗ X, map := λ (Y Y' : C) (f : Y ⟶ Y'), f ⊗ 𝟙 X, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.monoidal_category.tensor_right_map {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y Y' : C) (f : Y ⟶ Y') :

(category_theory.monoidal_category.tensor_right X).map f = (f ⊗ 𝟙 X)

@[simp]

theorem category_theory.monoidal_category.tensoring_right_obj (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

(category_theory.monoidal_category.tensoring_right C).obj X = category_theory.monoidal_category.tensor_right X

@[simp]

theorem category_theory.monoidal_category.tensoring_right_map_app (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) (f : X ⟶ Y) (Z : C) :

((category_theory.monoidal_category.tensoring_right C).map f).app Z = (𝟙 Z ⊗ f)

def category_theory.monoidal_category.tensoring_right (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

C ⥤ C ⥤ C

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' := _}

@[instance]

def category_theory.monoidal_category.category_theory.faithful (C : Type u) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.faithful (category_theory.monoidal_category.tensoring_right C)

def category_theory.monoidal_category.tensor_right_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

category_theory.monoidal_category.tensor_right (X ⊗ Y) ≅ category_theory.monoidal_category.tensor_right X ⋙ category_theory.monoidal_category.tensor_right Y

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) _

@[simp]

theorem category_theory.monoidal_category.tensor_right_tensor_hom_app {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : C) :

(category_theory.monoidal_category.tensor_right_tensor X Y).hom.app Z = (α_ Z X Y).inv

@[simp]

theorem category_theory.monoidal_category.tensor_right_tensor_inv_app {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : C) :

(category_theory.monoidal_category.tensor_right_tensor X Y).inv.app Z = (α_ Z X Y).hom