mathlib3 documentation

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 #

Tensor categories, Etingof, Gelaki, Nikshych, Ostrik, http://www-math.mit.edu/~etingof/egnobookfinal.pdf
https://stacks.math.columbia.edu/tag/0FFK.

@[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 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 {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X Y : C} (f : X ⟶ Y) :

(𝟙 (𝟙_ C) ⊗ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ 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 {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X Y : C} (f : X ⟶ Y) :

(f ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ 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.triangle {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (X Y : C) :

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

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

@[protected, 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)

@[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.inv (f ⊗ g) = category_theory.inv f ⊗ category_theory.inv g

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

theorem category_theory.monoidal_category.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 : 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} [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)

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

@[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) :

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

@[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) :

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

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.left_unitor_inv_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {X X' : C} (f : X ⟶ X') :

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

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

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

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

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

@[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_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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.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

theorem category_theory.monoidal_category.associator_inv_naturality_assoc {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') {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} [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.associator_conjugation_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V ⟶ W) [category_theory.is_iso f] (g : X ⟶ Y) (h : Y ⟶ Z) {X' : C} (f' : V ⊗ Z ⟶ X') :

(f ⊗ g) ≫ (category_theory.inv f ⊗ h) ≫ f' = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h) ≫ f'

@[simp]

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

(f ⊗ g) ≫ (category_theory.inv f ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

@[simp]

theorem category_theory.monoidal_category.inv_hom_id_tensor'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V ⟶ W) [category_theory.is_iso f] (g : X ⟶ Y) (h : Y ⟶ Z) {X' : C} (f' : W ⊗ Z ⟶ X') :

(category_theory.inv f ⊗ g) ≫ (f ⊗ h) ≫ f' = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h) ≫ f'

@[simp]

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

(category_theory.inv f ⊗ g) ≫ (f ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

@[simp]

theorem category_theory.monoidal_category.tensor_hom_inv_id'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V ⟶ W) [category_theory.is_iso f] (g : X ⟶ Y) (h : Y ⟶ Z) {X' : C} (f' : Z ⊗ V ⟶ X') :

(g ⊗ f) ≫ (h ⊗ category_theory.inv f) ≫ f' = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V) ≫ f'

@[simp]

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

(g ⊗ f) ≫ (h ⊗ category_theory.inv f) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

@[simp]

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

(g ⊗ category_theory.inv f) ≫ (h ⊗ f) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

@[simp]

theorem category_theory.monoidal_category.tensor_inv_hom_id'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V ⟶ W) [category_theory.is_iso f] (g : X ⟶ Y) (h : Y ⟶ Z) {X' : C} (f' : Z ⊗ W ⟶ X') :

(g ⊗ category_theory.inv f) ≫ (h ⊗ f) ≫ f' = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W) ≫ f'

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

@[simp]

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

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

@[simp]

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

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

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 = (α_ X.fst X.snd.fst X.snd.snd).inv

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.fst X.snd.fst X.snd.snd).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 = (λ_ X).inv

@[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).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 = (ρ_ X).inv

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

Instances for category_theory.monoidal_category.tensor_left

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

Instances for category_theory.monoidal_category.tensor_right

@[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

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

C ⥤ C ⥤ C

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

TODO: show this is a op-monoidal functor.

Equations

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

Instances for category_theory.monoidal_category.tensoring_left

category_theory.monoidal_category.tensoring_left.category_theory.faithful

@[simp]

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

(category_theory.monoidal_category.tensoring_left C).obj X = category_theory.monoidal_category.tensor_left X

@[simp]

theorem category_theory.monoidal_category.tensoring_left_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_left C).map f).app Z = f ⊗ 𝟙 Z

@[protected, instance]

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

category_theory.faithful (category_theory.monoidal_category.tensoring_left C)

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

Instances for category_theory.monoidal_category.tensoring_right

category_theory.monoidal_category.tensoring_right.category_theory.faithful

@[protected, instance]

def category_theory.monoidal_category.tensoring_right.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

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_tensor_hom (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (_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₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] :

category_theory.monoidal_category (C₁ × C₂)

Equations

category_theory.monoidal_category.prod_monoidal C₁ C₂ = {tensor_obj := λ (X Y : C₁ × C₂), (X.fst ⊗ Y.fst, X.snd ⊗ Y.snd), tensor_hom := λ (_x _x_1 _x_2 _x_3 : C₁ × C₂) (f : _x ⟶ _x_1) (g : _x_2 ⟶ _x_3), (f.fst ⊗ g.fst, f.snd ⊗ g.snd), tensor_id' := _, tensor_comp' := _, tensor_unit := (𝟙_ C₁ _inst_2, 𝟙_ C₂ _inst_4), associator := λ (X Y Z : C₁ × C₂), (α_ X.fst Y.fst Z.fst).prod (α_ X.snd Y.snd Z.snd), associator_naturality' := _, left_unitor := λ (_x : C₁ × C₂), category_theory.monoidal_category.prod_monoidal._match_1 C₁ C₂ _x, left_unitor_naturality' := _, right_unitor := λ (_x : C₁ × C₂), category_theory.monoidal_category.prod_monoidal._match_2 C₁ C₂ _x, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
category_theory.monoidal_category.prod_monoidal._match_1 C₁ C₂ (X₁, X₂) = (λ_ X₁).prod (λ_ X₂)
category_theory.monoidal_category.prod_monoidal._match_2 C₁ C₂ (X₁, X₂) = (ρ_ X₁).prod (ρ_ X₂)

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_associator (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (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₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] :

𝟙_ (C₁ × C₂) = (𝟙_ C₁ _inst_2, 𝟙_ C₂ _inst_4)

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_tensor_obj (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (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₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(λ_ X).hom.fst = (λ_ X.fst).hom

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_left_unitor_hom_snd (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(λ_ X).hom.snd = (λ_ X.snd).hom

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_left_unitor_inv_fst (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(λ_ X).inv.fst = (λ_ X.fst).inv

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_left_unitor_inv_snd (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(λ_ X).inv.snd = (λ_ X.snd).inv

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_right_unitor_hom_fst (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(ρ_ X).hom.fst = (ρ_ X.fst).hom

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_right_unitor_hom_snd (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(ρ_ X).hom.snd = (ρ_ X.snd).hom

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_right_unitor_inv_fst (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(ρ_ X).inv.fst = (ρ_ X.fst).inv

@[simp]

theorem category_theory.monoidal_category.prod_monoidal_right_unitor_inv_snd (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (X : C₁ × C₂) :

(ρ_ X).inv.snd = (ρ_ X.snd).inv