# Monoidal categories #

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

• tensorObj : C → C → C
• tensorHom : (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 leftUnitor_nat_iso, rightUnitor_nat_iso and associator_nat_iso.

Some consequences of the definition are proved in other files after proving the coherence theorem, e.g. (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom in CategoryTheory.Monoidal.CoherenceLemmas.

## Implementation notes #

In the definition of monoidal categories, we also provide the whiskering operators:

• whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : X ⊗ Y₁ ⟶ X ⊗ Y₂, denoted by X ◁ f,
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : X₁ ⊗ Y ⟶ X₂ ⊗ Y, denoted by f ▷ Y. These are products of an object and a morphism (the terminology "whiskering" is borrowed from 2-category theory). The tensor product of morphisms tensorHom can be defined in terms of the whiskerings. There are two possible such definitions, which are related by the exchange property of the whiskerings. These two definitions are accessed by tensorHom_def and tensorHom_def'. By default, tensorHom is defined so that tensorHom_def holds definitionally.

If you want to provide tensorHom and define whiskerLeft and whiskerRight in terms of it, you can use the alternative constructor CategoryTheory.MonoidalCategory.ofTensorHom.

The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories.

### Simp-normal form for morphisms #

Rewriting involving associators and unitors could be very complicated. We try to ease this complexity by putting carefully chosen simp lemmas that rewrite any morphisms into the simp-normal form defined below. Rewriting into simp-normal form is especially useful in preprocessing performed by the coherence tactic.

The simp-normal form of morphisms is defined to be an expression that has the minimal number of parentheses. More precisely,

1. it is a composition of morphisms like f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅ such that each fᵢ is either a structural morphisms (morphisms made up only of identities, associators, unitors) or non-structural morphisms, and
2. each non-structural morphism in the composition is of the form X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅, where each Xᵢ is a object that is not the identity or a tensor and f is a non-structural morphisms that is not the identity or a composite.

Note that X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅ is actually X₁ ◁ (X₂ ◁ (X₃ ◁ ((f ▷ X₄) ▷ X₅))).

Currently, the simp lemmas don't rewrite 𝟙 X ⊗ f and f ⊗ 𝟙 Y into X ◁ f and f ▷ Y, respectively, since it requires a huge refactoring. We hope to add these simp lemmas soon.

## References #

class CategoryTheory.MonoidalCategoryStruct (C : Type u) [𝒞 : ] :
Type (max u v)

Auxiliary structure to carry only the data fields of (and provide notation for) MonoidalCategory.

• tensorObj : CCC

curried tensor product of objects

• whiskerLeft : (X : C) → {Y₁ Y₂ : C} → (Y₁ Y₂)

left whiskering for morphisms

• whiskerRight : {X₁ X₂ : C} → (X₁ X₂)

right whiskering for morphisms

• tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ Y₁)(X₂ Y₂)

Tensor product of identity maps is the identity: (𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)

• tensorUnit : C

The tensor unity in the monoidal structure 𝟙_ C

• associator :

The associator isomorphism (X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)

• leftUnitor : (X : C) →

The left unitor: 𝟙_ C ⊗ X ≃ X

• rightUnitor : (X : C) →

The right unitor: X ⊗ 𝟙_ C ≃ X

Instances

Notation for tensorObj, the tensor product of objects in a monoidal category

Equations
• One or more equations did not get rendered due to their size.
Instances For

Notation for the whiskerLeft operator of monoidal categories

Equations
• One or more equations did not get rendered due to their size.
Instances For

Notation for the whiskerRight operator of monoidal categories

Equations
• One or more equations did not get rendered due to their size.
Instances For

Notation for tensorHom, the tensor product of morphisms in a monoidal category

Equations
• One or more equations did not get rendered due to their size.
Instances For

Notation for tensorUnit, the two-sided identity of ⊗

Equations
• One or more equations did not get rendered due to their size.
Instances For

Used to ensure that 𝟙_ notation is used, as the ascription makes this not automatic.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Notation for the monoidal associator: (X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)

Equations
Instances For

Notation for the leftUnitor: 𝟙_C ⊗ X ≃ X

Equations
Instances For

Notation for the rightUnitor: X ⊗ 𝟙_C ≃ X

Equations
Instances For
class CategoryTheory.MonoidalCategory (C : Type u) [𝒞 : ] extends :
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.

• tensorObj : CCC
• whiskerLeft : (X : C) → {Y₁ Y₂ : C} → (Y₁ Y₂)
• whiskerRight : {X₁ X₂ : C} → (X₁ X₂)
• tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ Y₁)(X₂ Y₂)
• tensorUnit : C
• associator :
• leftUnitor : (X : C) →
• rightUnitor : (X : C) →
• tensorHom_def : ∀ {X₁ Y₁ X₂ Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂),
• tensor_id :

Tensor product of identity maps is the identity: (𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)

• tensor_comp : ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂),

Composition of tensor products is tensor product of compositions: (f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)

• whiskerLeft_id :
• id_whiskerRight :
• associator_naturality : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃), =

Naturality of the associator isomorphism: (f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)

• leftUnitor_naturality : ∀ {X Y : C} (f : X Y),

Naturality of the left unitor, commutativity of 𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y and 𝟙_ C ⊗ X ⟶ X ⟶ Y

• rightUnitor_naturality : ∀ {X Y : C} (f : X Y),

Naturality of the right unitor: commutativity of X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y and X ⊗ 𝟙_ C ⟶ X ⟶ Y

• pentagon : ∀ (W X Y Z : C), =

The pentagon identity relating the isomorphism between X ⊗ (Y ⊗ (Z ⊗ W)) and ((X ⊗ Y) ⊗ Z) ⊗ W

• triangle : ∀ (X Y : C),

The identity relating the isomorphisms between X ⊗ (𝟙_ C ⊗ Y), (X ⊗ 𝟙_ C) ⊗ Y and X ⊗ Y

Instances
theorem CategoryTheory.MonoidalCategory.tensorHom_def {C : Type u} [𝒞 : ] [self : ] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) :
theorem CategoryTheory.MonoidalCategory.tensor_id {C : Type u} [𝒞 : ] [self : ] (X₁ : C) (X₂ : C) :

Tensor product of identity maps is the identity: (𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)

@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_comp {C : Type u} [𝒞 : ] [self : ] {X₁ : C} {Y₁ : C} {Z₁ : C} {X₂ : C} {Y₂ : C} {Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :

Composition of tensor products is tensor product of compositions: (f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)

@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_id {C : Type u} [𝒞 : ] [self : ] (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.id_whiskerRight {C : Type u} [𝒞 : ] [self : ] (X : C) (Y : C) :
theorem CategoryTheory.MonoidalCategory.associator_naturality {C : Type u} [𝒞 : ] [self : ] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :

Naturality of the associator isomorphism: (f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)

theorem CategoryTheory.MonoidalCategory.leftUnitor_naturality {C : Type u} [𝒞 : ] [self : ] {X : C} {Y : C} (f : X Y) :

Naturality of the left unitor, commutativity of 𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y and 𝟙_ C ⊗ X ⟶ X ⟶ Y

theorem CategoryTheory.MonoidalCategory.rightUnitor_naturality {C : Type u} [𝒞 : ] [self : ] {X : C} {Y : C} (f : X Y) :

Naturality of the right unitor: commutativity of X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y and X ⊗ 𝟙_ C ⟶ X ⟶ Y

@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon {C : Type u} [𝒞 : ] [self : ] (W : C) (X : C) (Y : C) (Z : C) :

The pentagon identity relating the isomorphism between X ⊗ (Y ⊗ (Z ⊗ W)) and ((X ⊗ Y) ⊗ Z) ⊗ W

@[simp]
theorem CategoryTheory.MonoidalCategory.triangle {C : Type u} [𝒞 : ] [self : ] (X : C) (Y : C) :

The identity relating the isomorphisms between X ⊗ (𝟙_ C ⊗ Y), (X ⊗ 𝟙_ C) ⊗ Y and X ⊗ Y

theorem CategoryTheory.MonoidalCategory.tensorHom_def_assoc {C : Type u} [𝒞 : ] [self : ] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.whiskerLeft_id_assoc {C : Type u} [𝒞 : ] [self : ] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.id_whiskerRight_assoc {C : Type u} [𝒞 : ] [self : ] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.tensor_comp_assoc {C : Type u} [𝒞 : ] [self : ] {X₁ : C} {Y₁ : C} {Z₁ : C} {X₂ : C} {Y₂ : C} {Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.associator_naturality_assoc {C : Type u} [𝒞 : ] [self : ] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {Z : C} :
theorem CategoryTheory.MonoidalCategory.leftUnitor_naturality_assoc {C : Type u} [𝒞 : ] [self : ] {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.MonoidalCategory.rightUnitor_naturality_assoc {C : Type u} [𝒞 : ] [self : ] {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_assoc {C : Type u} [𝒞 : ] [self : ] (W : C) (X : C) (Y : C) (Z : C) {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc {C : Type u} [𝒞 : ] [self : ] (X : C) (Y : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.id_tensorHom {C : Type u} [𝒞 : ] (X : C) {Y₁ : C} {Y₂ : C} (f : Y₁ Y₂) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorHom_id {C : Type u} [𝒞 : ] {X₁ : C} {X₂ : C} (f : X₁ X₂) (Y : C) :
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc {C : Type u} [𝒞 : ] (W : C) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp {C : Type u} [𝒞 : ] (W : C) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft_assoc {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft_assoc {C : Type u} [𝒞 : ] (X : C) (Y : C) {Z : C} {Z' : C} (f : Z✝ Z') {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft {C : Type u} [𝒞 : ] (X : C) (Y : C) {Z : C} {Z' : C} (f : Z Z') :
theorem CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc {C : Type u} [𝒞 : ] {W : C} {X : C} {Y : C} (f : W X) (g : X Y) (Z : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.comp_whiskerRight {C : Type u} [𝒞 : ] {W : C} {X : C} {Y : C} (f : W X) (g : X Y) (Z : C) :
theorem CategoryTheory.MonoidalCategory.whiskerRight_id_assoc {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRight_id {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor_assoc {C : Type u} [𝒞 : ] {X : C} {X' : C} (f : X X') (Y : C) (Z : C) {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor {C : Type u} [𝒞 : ] {X : C} {X' : C} (f : X X') (Y : C) (Z : C) :
theorem CategoryTheory.MonoidalCategory.whisker_assoc_assoc {C : Type u} [𝒞 : ] (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.whisker_assoc {C : Type u} [𝒞 : ] (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) :
theorem CategoryTheory.MonoidalCategory.whisker_exchange_assoc {C : Type u} [𝒞 : ] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z✝) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.whisker_exchange {C : Type u} [𝒞 : ] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
theorem CategoryTheory.MonoidalCategory.tensorHom_def'_assoc {C : Type u} [𝒞 : ] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.tensorHom_def' {C : Type u} [𝒞 : ] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight_assoc {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv'_assoc {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv' {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight'_assoc {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight' {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom'_assoc {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom' {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight'_assoc {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight' {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_hom {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_inv {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
def CategoryTheory.MonoidalCategory.whiskerLeftIso {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :

The left whiskering of an isomorphism is an isomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.MonoidalCategory.whiskerLeft_isIso {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
Equations
• =
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_whiskerLeft {C : Type u} [𝒞 : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_refl {C : Type u} [𝒞 : ] (W : C) (X : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_trans {C : Type u} [𝒞 : ] (W : C) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_symm {C : Type u} [𝒞 : ] (W : C) {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_inv {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_hom {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
def CategoryTheory.MonoidalCategory.whiskerRightIso {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :

The right whiskering of an isomorphism is an isomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.MonoidalCategory.whiskerRight_isIso {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
Equations
• =
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_whiskerRight {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_refl {C : Type u} [𝒞 : ] (X : C) (W : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_trans {C : Type u} [𝒞 : ] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (W : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_symm {C : Type u} [𝒞 : ] {X : C} {Y : C} (f : X Y) (W : C) :
@[simp]
theorem CategoryTheory.tensorIso_inv {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} (f : X Y) (g : X' Y') :
(f g).inv =
@[simp]
theorem CategoryTheory.tensorIso_hom {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} (f : X Y) (g : X' Y') :
(f g).hom =
def CategoryTheory.tensorIso {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} (f : X Y) (g : X' Y') :

The tensor product of two isomorphisms is an isomorphism.

Equations
• f g = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For

Notation for tensorIso, the tensor product of isomorphisms

Equations
Instances For
instance CategoryTheory.MonoidalCategory.tensor_isIso {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
Equations
• =
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_tensor {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
theorem CategoryTheory.MonoidalCategory.whiskerLeft_dite {C : Type u} {P : Prop} [] (X : C) {Y : C} {Z : C} (f : P(Y Z)) (f' : ¬P(Y Z)) :
CategoryTheory.MonoidalCategory.whiskerLeft X (if h : P then f h else f' h) = if h : P then else
theorem CategoryTheory.MonoidalCategory.dite_whiskerRight {C : Type u} {P : Prop} [] {X : C} {Y : C} (f : P(X Y)) (f' : ¬P(X Y)) (Z : C) :
CategoryTheory.MonoidalCategory.whiskerRight (if h : P then f h else f' h) Z = if h : P then else
theorem CategoryTheory.MonoidalCategory.tensor_dite {C : Type u} {P : Prop} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : P(Y Z)) (g' : ¬P(Y Z)) :
CategoryTheory.MonoidalCategory.tensorHom f (if h : P then g h else g' h) = if h : P then else
theorem CategoryTheory.MonoidalCategory.dite_tensor {C : Type u} {P : Prop} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : P(Y Z)) (g' : ¬P(Y Z)) :
CategoryTheory.MonoidalCategory.tensorHom (if h : P then g h else g' h) f = if h : P then else
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_eqToHom {C : Type u} (X : C) {Y : C} {Z : C} (f : Y = Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.eqToHom_whiskerRight {C : Type u} {X : C} {Y : C} (f : X = Y) (Z : C) :
theorem CategoryTheory.MonoidalCategory.associator_naturality_left_assoc {C : Type u} {X : C} {X' : C} (f : X X') (Y : C) (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_naturality_left {C : Type u} {X : C} {X' : C} (f : X X') (Y : C) (Z : C) :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_left_assoc {C : Type u} {X : C} {X' : C} (f : X X') (Y : C) (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_left {C : Type u} {X : C} {X' : C} (f : X X') (Y : C) (Z : C) :
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm_assoc {C : Type u} {X : C} {X' : C} (f : X X') (Y : C) (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm {C : Type u} {X : C} {X' : C} (f : X X') (Y : C) (Z : C) :
theorem CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc {C : Type u} (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_naturality_middle {C : Type u} (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc {C : Type u} (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_middle {C : Type u} (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) :
theorem CategoryTheory.MonoidalCategory.whisker_assoc_symm_assoc {C : Type u} (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.whisker_assoc_symm {C : Type u} (X : C) {Y : C} {Y' : C} (f : Y Y') (Z : C) :
theorem CategoryTheory.MonoidalCategory.associator_naturality_right_assoc {C : Type u} (X : C) (Y : C) {Z : C} {Z' : C} (f : Z✝ Z') {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_naturality_right {C : Type u} (X : C) (Y : C) {Z : C} {Z' : C} (f : Z Z') :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc {C : Type u} (X : C) (Y : C) {Z : C} {Z' : C} (f : Z✝ Z') {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_right {C : Type u} (X : C) (Y : C) {Z : C} {Z' : C} (f : Z Z') :
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm_assoc {C : Type u} (X : C) (Y : C) {Z : C} {Z' : C} (f : Z✝ Z') {Z : C} :
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm {C : Type u} (X : C) (Y : C) {Z : C} {Z' : C} (f : Z Z') :
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft_symm_assoc {C : Type u} {X : C} {X' : C} (f : X X') {Z : C} (h : X' Z) :
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft_symm {C : Type u} {X : C} {X' : C} (f : X X') :
theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc {C : Type u} {X : C} {X' : C} (f : X X') {Z : C} (h : Z) :
theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality {C : Type u} {X : C} {X' : C} (f : X X') :
theorem CategoryTheory.MonoidalCategory.whiskerRight_id_symm_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.MonoidalCategory.whiskerRight_id_symm {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.MonoidalCategory.whiskerLeft_iff {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
f = g
theorem CategoryTheory.MonoidalCategory.whiskerRight_iff {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
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.

@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_hom_hom_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_hom_hom {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_hom_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_hom {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_inv_hom_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_inv_hom {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_hom_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_hom {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
@[simp]
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
@[simp]

We state it as a simp lemma, which is regarded as an involved version of id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y).

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv_assoc {C : Type u} (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_assoc {C : Type u} {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X X') (g : Y Y') (h : Z✝ Z') {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality {C : Type u} {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
theorem CategoryTheory.MonoidalCategory.associator_conjugation_assoc {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X X') (g : Y Y') (h : Z✝ Z') {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.associator_conjugation {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation_assoc {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X X') (g : Y Y') (h : Z✝ Z') {Z : C} :
theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality_assoc {C : Type u} {X : C} {Y : C} {Z : C} {Z' : C} (h : Z✝ Z') {Z : C} :
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality {C : Type u} {X : C} {Y : C} {Z : C} {Z' : C} (h : Z Z') :
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality_assoc {C : Type u} {X : C} {Y : C} {Z : C} {X' : C} (f : X X') {Z : C} :
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality {C : Type u} {X : C} {Y : C} {Z : C} {X' : C} (f : X X') :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor'_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor' {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor'_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor' {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id'_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id' {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id'_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id' {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : X Y) (h : Y Z) :
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.ofTensorHom {C : Type u} (tensor_id : autoParam (∀ (X₁ X₂ : C), ) _auto✝) (id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ Y₂), ) _auto✝) (tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ X₂) (Y : C), ) _auto✝) (tensor_comp : autoParam (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂), ) _auto✝) (associator_naturality : autoParam (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃), = ) _auto✝) (leftUnitor_naturality : autoParam (∀ {X Y : C} (f : X Y), ) _auto✝) (rightUnitor_naturality : autoParam (∀ {X Y : C} (f : X Y), ) _auto✝) (pentagon : autoParam (∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp () () = ) _auto✝) (triangle : autoParam (∀ (X Y : C), ) _auto✝) :

A constructor for monoidal categories that requires tensorHom instead of whiskerLeft and whiskerRight.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.MonoidalCategory.comp_tensor_id_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : X Y) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.comp_tensor_id {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : X Y) :
theorem CategoryTheory.MonoidalCategory.id_tensor_comp_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : X Y) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.id_tensor_comp {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : X Y) :
theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z✝) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z✝) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
theorem CategoryTheory.MonoidalCategory.tensor_left_iff {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
theorem CategoryTheory.MonoidalCategory.tensor_right_iff {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_obj (C : Type u) [𝒞 : ] (X : C × C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_map (C : Type u) [𝒞 : ] {X : C × C} {Y : C × C} (f : X Y) :

The tensor product expressed as a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The left-associated triple tensor product as a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.leftAssocTensor_obj (C : Type u) [𝒞 : ] (X : C × C × C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.leftAssocTensor_map (C : Type u) [𝒞 : ] {X : C × C × C} {Y : C × C × C} (f : X Y) :

The right-associated triple tensor product as a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.rightAssocTensor_obj (C : Type u) [𝒞 : ] (X : C × C × C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.rightAssocTensor_map (C : Type u) [𝒞 : ] {X : C × C × C} {Y : C × C × C} (f : X Y) :
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedTensor_obj_map (C : Type u) [𝒞 : ] (X : C) :
∀ {X_1 Y : C} (g : X_1 Y),
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedTensor_obj_obj (C : Type u) [𝒞 : ] (X : C) (Y : C) :
().obj Y =
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedTensor_map_app (C : Type u) [𝒞 : ] :
∀ {X Y : C} (f : X Y) (Y_1 : C), ().app Y_1 =

The tensor product bifunctor C ⥤ C ⥤ C of a monoidal category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorLeft_map {C : Type u} [𝒞 : ] (X : C) :
∀ {X_1 Y : C} (g : X_1 Y),
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorLeft_obj {C : Type u} [𝒞 : ] (X : C) (Y : C) :
def CategoryTheory.MonoidalCategory.tensorLeft {C : Type u} [𝒞 : ] (X : C) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorRight_obj {C : Type u} [𝒞 : ] (X : C) (j : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorRight_map {C : Type u} [𝒞 : ] (X : C) :
∀ {X_1 Y : C} (f : X_1 Y),
def CategoryTheory.MonoidalCategory.tensorRight {C : Type u} [𝒞 : ] (X : C) :

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

Equations
Instances For
@[reducible, inline]

The functor fun X ↦ 𝟙_ C ⊗ X.

Equations
Instances For
@[reducible, inline]

The functor fun X ↦ X ⊗ 𝟙_ C.

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.associatorNatIso_inv_app (C : Type u) [𝒞 : ] (X : C × C × C) :
.app X = (CategoryTheory.MonoidalCategory.associator X.1 X.2.1 X.2.2).inv
@[simp]
theorem CategoryTheory.MonoidalCategory.associatorNatIso_hom_app (C : Type u) [𝒞 : ] (X : C × C × C) :
.app X = (CategoryTheory.MonoidalCategory.associator X.1 X.2.1 X.2.2).hom

The associator as a natural isomorphism.

Equations
Instances For
@[simp]
@[simp]

The left unitor as a natural isomorphism.

Equations
Instances For
@[simp]
@[simp]

The right unitor as a natural isomorphism.

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedAssociatorNatIso_inv_app_app_app (C : Type u) [𝒞 : ] (X : C) (X : C) (X : C) :
(( X✝¹).app X✝).app X = ().inv
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedAssociatorNatIso_hom_app_app_app (C : Type u) [𝒞 : ] (X : C) (X : C) (X : C) :
(( X✝¹).app X✝).app X = ().hom

The associator as a natural isomorphism between trifunctors C ⥤ C ⥤ C ⥤ C.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_hom_app {C : Type u} [𝒞 : ] (X : C) (Y : C) (Z : C) :
.app Z = .hom
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_inv_app {C : Type u} [𝒞 : ] (X : C) (Y : C) (Z : C) :
.app Z = .inv
@[reducible, inline]

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

TODO: show this is an op-monoidal functor.

Equations
Instances For
Equations
• =