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.

References

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

class CategoryTheory.MonoidalCategory (C : Type u) [𝒞 : CategoryTheory.Category.{v, u} C] : Type (max u v)

• tensorObj : C → C → C

  curried tensor product of objects

• whiskerLeft : (X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (CategoryTheory.MonoidalCategory.tensorObj X Y₁ ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y₂)

  left whiskering for morphisms

• whiskerRight : {X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → CategoryTheory.MonoidalCategory.tensorObj X₁ Y ⟶ CategoryTheory.MonoidalCategory.tensorObj X₂ Y

  right whiskering for morphisms

• tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂)

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

• tensorHom_def : ∀ {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X₂) (CategoryTheory.MonoidalCategory.whiskerLeft Y₁ g)
• tensor_id : ∀ (X₁ X₂ : C), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)

  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₂), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)

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

• tensorUnit' : C

  The tensor unity in the monoidal structure 𝟙_ C

• associator : (X Y Z : C) → CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≅ CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)

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

• whiskerLeft_id : ∀ (X Y : C), CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
• id_whiskerRight : ∀ (X Y : C), CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.id X) Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
• associator_naturality : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) f₃) (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategory.tensorHom f₁ (CategoryTheory.MonoidalCategory.tensorHom f₂ f₃))

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

• leftUnitor : (X : C) → CategoryTheory.MonoidalCategory.tensorObj CategoryTheory.MonoidalCategory.tensorUnit' X ≅ X

  The left unitor: 𝟙_ C ⊗ X ≃ X

• leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit') f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f

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

• rightUnitor : (X : C) → CategoryTheory.MonoidalCategory.tensorObj X CategoryTheory.MonoidalCategory.tensorUnit' ≅ X

  The right unitor: X ⊗ 𝟙_ C ≃ X

• rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit')) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f

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

• pentagon : ∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom

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

• triangle : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X CategoryTheory.MonoidalCategory.tensorUnit' Y).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)

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

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.

theorem CategoryTheory.MonoidalCategory.tensorHom_def_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Y₁ g) h)

theorem CategoryTheory.MonoidalCategory.whiskerLeft_id_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.CategoryStruct.id Y)) h = h

theorem CategoryTheory.MonoidalCategory.id_whiskerRight_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.id X) Y) h = h

theorem CategoryTheory.MonoidalCategory.tensor_comp_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {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 : CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂) h)

theorem CategoryTheory.MonoidalCategory.associator_naturality_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Y₁ (CategoryTheory.MonoidalCategory.tensorObj Y₂ Y₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) f₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ (CategoryTheory.MonoidalCategory.tensorHom f₂ f₃)) h)

theorem CategoryTheory.MonoidalCategory.leftUnitor_naturality_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit') f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)

theorem CategoryTheory.MonoidalCategory.rightUnitor_naturality_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)

theorem CategoryTheory.MonoidalCategory.pentagon_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj W (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.MonoidalCategory.associator X Y Z).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom h)

@[simp]

theorem CategoryTheory.MonoidalCategory.triangle_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X CategoryTheory.MonoidalCategory.tensorUnit' Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)) h

@[inline, reducible]

abbrev CategoryTheory.MonoidalCategory.tensorUnit (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : C

The tensor unity in the monoidal structure 𝟙_ C

def CategoryTheory.MonoidalCategory.«term_⊗_» : Lean.TrailingParserDescr

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

def CategoryTheory.MonoidalCategory.«term_◁_» : Lean.TrailingParserDescr

Notation for the whiskerLeft operator of monoidal categories

def CategoryTheory.MonoidalCategory.«term_▷_» : Lean.TrailingParserDescr

Notation for the whiskerRight operator of monoidal categories

def CategoryTheory.MonoidalCategory.«term_⊗__1» : Lean.TrailingParserDescr

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

def CategoryTheory.MonoidalCategory.«term𝟙_» : Lean.ParserDescr

Notation for tensorUnit, the two-sided identity of ⊗

def CategoryTheory.MonoidalCategory.termα_ : Lean.ParserDescr

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

def CategoryTheory.MonoidalCategory.«termλ_» : Lean.ParserDescr

Notation for the leftUnitor: 𝟙_C ⊗ X ≃ X

def CategoryTheory.MonoidalCategory.termρ_ : Lean.ParserDescr

Notation for the rightUnitor: X ⊗ 𝟙_C ≃ X

theorem CategoryTheory.MonoidalCategory.id_tensorHom {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y₁ : C} {Y₂ : C} (f : Y₁ ⟶ Y₂) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f = CategoryTheory.MonoidalCategory.whiskerLeft X f

theorem CategoryTheory.MonoidalCategory.tensorHom_id {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.MonoidalCategory.whiskerRight f Y

theorem CategoryTheory.MonoidalCategory.whisker_exchange {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W g) (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Y) (CategoryTheory.MonoidalCategory.whiskerLeft X g)

theorem CategoryTheory.MonoidalCategory.tensorHom_def'_assoc {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X₁ g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Y₂) h)

theorem CategoryTheory.MonoidalCategory.tensorHom_def' {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X₁ g) (CategoryTheory.MonoidalCategory.whiskerRight f Y₂)

@[simp]

theorem CategoryTheory.tensorIso_hom {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f : X ≅ Y) (g : X' ≅ Y') : (f ⊗ g).hom = CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom

@[simp]

theorem CategoryTheory.tensorIso_inv {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f : X ≅ Y) (g : X' ≅ Y') : (f ⊗ g).inv = CategoryTheory.MonoidalCategory.tensorHom f.inv g.inv

def CategoryTheory.tensorIso {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f : X ≅ Y) (g : X' ≅ Y') : CategoryTheory.MonoidalCategory.tensorObj X X' ≅ CategoryTheory.MonoidalCategory.tensorObj Y Y'

The tensor product of two isomorphisms is an isomorphism.

def CategoryTheory.«term_⊗_» : Lean.TrailingParserDescr

Notation for tensorIso, the tensor product of isomorphisms

instance CategoryTheory.MonoidalCategory.tensor_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) [CategoryTheory.IsIso f] (g : Y ⟶ Z) [CategoryTheory.IsIso g] : CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.tensorHom f g)

@[simp]

theorem CategoryTheory.MonoidalCategory.inv_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) [CategoryTheory.IsIso f] (g : Y ⟶ Z) [CategoryTheory.IsIso g] : CategoryTheory.inv (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) (CategoryTheory.inv g)

theorem CategoryTheory.MonoidalCategory.tensor_dite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : Prop} [Decidable P] {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 CategoryTheory.MonoidalCategory.tensorHom f (g h) else CategoryTheory.MonoidalCategory.tensorHom f (g' h)

theorem CategoryTheory.MonoidalCategory.dite_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : Prop} [Decidable P] {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 CategoryTheory.MonoidalCategory.tensorHom (g h) f else CategoryTheory.MonoidalCategory.tensorHom (g' h) f

theorem CategoryTheory.MonoidalCategory.comp_tensor_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Y Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id Z)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.comp_tensor_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z))

theorem CategoryTheory.MonoidalCategory.id_tensor_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.id_tensor_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g)

@[simp]

theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id X)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) h

@[simp]

theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) f) (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.MonoidalCategory.tensorHom g f

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) h

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) = CategoryTheory.MonoidalCategory.tensorHom g f

@[simp]

theorem CategoryTheory.MonoidalCategory.rightUnitor_conjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor Y).inv)

@[simp]

theorem CategoryTheory.MonoidalCategory.leftUnitor_conjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor Y).inv)

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} (f : X ⟶ X') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj CategoryTheory.MonoidalCategory.tensorUnit' X' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit') f) h)

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} (f : X ⟶ X') : CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor X').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit') f)

theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} (f : X ⟶ X') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X' CategoryTheory.MonoidalCategory.tensorUnit' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit')) h)

theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} (f : X ⟶ X') : CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor X').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit'))

theorem CategoryTheory.MonoidalCategory.tensor_left_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) f = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) g ↔ f = g

theorem CategoryTheory.MonoidalCategory.tensor_right_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) = CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit 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 CategoryTheory.MonoidalCategory.pentagon_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj W X) Y) Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.MonoidalCategory.associator X Y Z).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).inv (CategoryTheory.CategoryStruct.id Z)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv h)

theorem CategoryTheory.MonoidalCategory.pentagon_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.MonoidalCategory.associator X Y Z).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).inv (CategoryTheory.CategoryStruct.id Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv

theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom)

theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) CategoryTheory.MonoidalCategory.tensorUnit' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.rightUnitor Y).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y (CategoryTheory.MonoidalCategory.tensorUnit C)).inv h)

@[simp]

theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.rightUnitor Y).inv) (CategoryTheory.MonoidalCategory.associator X Y (CategoryTheory.MonoidalCategory.tensorUnit C)).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (CategoryTheory.MonoidalCategory.tensorUnit C) Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) h

@[simp]

theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (CategoryTheory.MonoidalCategory.tensorUnit C) Y).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorUnit C)) Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (CategoryTheory.MonoidalCategory.tensorUnit C) Y).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.id Y)) h

@[simp]

theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).inv) (CategoryTheory.MonoidalCategory.associator X (CategoryTheory.MonoidalCategory.tensorUnit C) Y).inv = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.id Y)

theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X' Y') Z' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X' Y' Z').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h) h)

theorem CategoryTheory.MonoidalCategory.associator_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) (CategoryTheory.MonoidalCategory.associator X' Y' Z').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h)

theorem CategoryTheory.MonoidalCategory.associator_conjugation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X' Y') Z' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X' Y' Z').inv h))

@[simp]

theorem CategoryTheory.MonoidalCategory.associator_conjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) (CategoryTheory.MonoidalCategory.associator X' Y' Z').inv)

theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X' (CategoryTheory.MonoidalCategory.tensorObj Y' Z') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X' Y' Z').hom h))

theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') : CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h) (CategoryTheory.MonoidalCategory.associator X' Y' Z').hom)

theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} {Z' : C} (h : Z ⟶ Z') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) h)) h)

theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} {Z' : C} (h : Z ⟶ Z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) (CategoryTheory.MonoidalCategory.associator X Y Z').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) h))

theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} {X' : C} (f : X ⟶ X') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X' Y) Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X' Y Z).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.CategoryStruct.id Z)) h)

theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} {X' : C} (f : X ⟶ X') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z))) (CategoryTheory.MonoidalCategory.associator X' Y Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.CategoryStruct.id Z))

@[simp]

theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj V Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.inv h) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) h) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom g) (CategoryTheory.MonoidalCategory.tensorHom f.inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj W Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.inv g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom h) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) h) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.inv g) (CategoryTheory.MonoidalCategory.tensorHom f.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorHom_inv_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z V ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h f.inv) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id V)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorHom_inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f.hom) (CategoryTheory.MonoidalCategory.tensorHom h f.inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id V)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id V))

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h f.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id W)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f.inv) (CategoryTheory.MonoidalCategory.tensorHom h f.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id W))

@[simp]

theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj V Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) h) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) h) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj W Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f h) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) h) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) g) (CategoryTheory.MonoidalCategory.tensorHom f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorHom_inv_id'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z V ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.inv f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id V)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorHom_inv_id' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id V)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id V))

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.inv f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id W)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V ⟶ W) [CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.inv f)) (CategoryTheory.MonoidalCategory.tensorHom h f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id W))

def CategoryTheory.MonoidalCategory.ofTensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] (tensorObj : C → C → C) (tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)) (whiskerLeft : optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) fun X x x_1 f => tensorHom X X x x_1 (CategoryTheory.CategoryStruct.id X) f) (whiskerRight : optParam ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom X₁ X₂ Y Y f (CategoryTheory.CategoryStruct.id Y)) (tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom X₁ X₁ X₂ X₂ (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (tensorObj X₁ X₂)) _auto✝) (id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom X X Y₁ Y₂ (CategoryTheory.CategoryStruct.id X) f = whiskerLeft X Y₁ Y₂ f) _auto✝) (tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom X₁ X₂ Y Y f (CategoryTheory.CategoryStruct.id Y) = whiskerRight X₁ X₂ f Y) _auto✝) (tensor_comp : autoParam (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂), tensorHom X₁ Z₁ X₂ Z₂ (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (tensorHom X₁ Y₁ X₂ Y₂ f₁ f₂) (tensorHom Y₁ Z₁ Y₂ Z₂ g₁ g₂)) _auto✝) (tensorUnit' : C) (associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)) (associator_naturality : autoParam (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), CategoryTheory.CategoryStruct.comp (tensorHom (tensorObj X₁ X₂) (tensorObj Y₁ Y₂) X₃ Y₃ (tensorHom X₁ Y₁ X₂ Y₂ f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom X₁ Y₁ (tensorObj X₂ X₃) (tensorObj Y₂ Y₃) f₁ (tensorHom X₂ Y₂ X₃ Y₃ f₂ f₃))) _auto✝) (leftUnitor : (X : C) → tensorObj tensorUnit' X ≅ X) (leftUnitor_naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (tensorHom tensorUnit' tensorUnit' X Y (CategoryTheory.CategoryStruct.id tensorUnit') f) (leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (leftUnitor X).hom f) _auto✝) (rightUnitor : (X : C) → tensorObj X tensorUnit' ≅ X) (rightUnitor_naturality : autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (tensorHom X Y tensorUnit' tensorUnit' f (CategoryTheory.CategoryStruct.id tensorUnit')) (rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (rightUnitor X).hom f) _auto✝) (pentagon : autoParam (∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (tensorHom (tensorObj (tensorObj W X) Y) (tensorObj W (tensorObj X Y)) Z Z (associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (tensorHom W W (tensorObj (tensorObj X Y) Z) (tensorObj X (tensorObj Y Z)) (CategoryTheory.CategoryStruct.id W) (associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom) _auto✝) (triangle : autoParam (∀ (X Y : C), CategoryTheory.CategoryStruct.comp (associator X tensorUnit' Y).hom (tensorHom X X (tensorObj tensorUnit' Y) Y (CategoryTheory.CategoryStruct.id X) (leftUnitor Y).hom) = tensorHom (tensorObj X tensorUnit') X Y Y (rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)) _auto✝) : CategoryTheory.MonoidalCategory C

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

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C × C) : (CategoryTheory.MonoidalCategory.tensor C).obj X = CategoryTheory.MonoidalCategory.tensorObj X.fst X.snd

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C × C} {Y : C × C} (f : X ⟶ Y) : (CategoryTheory.MonoidalCategory.tensor C).map f = CategoryTheory.MonoidalCategory.tensorHom f.fst f.snd

def CategoryTheory.MonoidalCategory.tensor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (C × C) C

The tensor product expressed as a functor.

def CategoryTheory.MonoidalCategory.leftAssocTensor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (C × C × C) C

The left-associated triple tensor product as a functor.

@[simp]

theorem CategoryTheory.MonoidalCategory.leftAssocTensor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C × C × C) : (CategoryTheory.MonoidalCategory.leftAssocTensor C).obj X = CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X.fst X.snd.fst) X.snd.snd

@[simp]

theorem CategoryTheory.MonoidalCategory.leftAssocTensor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C × C × C} {Y : C × C × C} (f : X ⟶ Y) : (CategoryTheory.MonoidalCategory.leftAssocTensor C).map f = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f.fst f.snd.fst) f.snd.snd

def CategoryTheory.MonoidalCategory.rightAssocTensor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (C × C × C) C

The right-associated triple tensor product as a functor.

@[simp]

theorem CategoryTheory.MonoidalCategory.rightAssocTensor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C × C × C) : (CategoryTheory.MonoidalCategory.rightAssocTensor C).obj X = CategoryTheory.MonoidalCategory.tensorObj X.fst (CategoryTheory.MonoidalCategory.tensorObj X.snd.fst X.snd.snd)

@[simp]

theorem CategoryTheory.MonoidalCategory.rightAssocTensor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C × C × C} {Y : C × C × C} (f : X ⟶ Y) : (CategoryTheory.MonoidalCategory.rightAssocTensor C).map f = CategoryTheory.MonoidalCategory.tensorHom f.fst (CategoryTheory.MonoidalCategory.tensorHom f.snd.fst f.snd.snd)

def CategoryTheory.MonoidalCategory.tensorUnitLeft (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor C C

The functor fun X ↦ 𝟙_ C ⊗ X.

def CategoryTheory.MonoidalCategory.tensorUnitRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor C C

The functor fun X ↦ X ⊗ 𝟙_ C.

@[simp]

theorem CategoryTheory.MonoidalCategory.associatorNatIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C × C × C) : (CategoryTheory.MonoidalCategory.associatorNatIso C).inv.app X = (CategoryTheory.MonoidalCategory.associator X.fst X.snd.fst X.snd.snd).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.associatorNatIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C × C × C) : (CategoryTheory.MonoidalCategory.associatorNatIso C).hom.app X = (CategoryTheory.MonoidalCategory.associator X.fst X.snd.fst X.snd.snd).hom

def CategoryTheory.MonoidalCategory.associatorNatIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory.leftAssocTensor C ≅ CategoryTheory.MonoidalCategory.rightAssocTensor C

The associator as a natural isomorphism.

@[simp]

theorem CategoryTheory.MonoidalCategory.leftUnitorNatIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).inv.app X = (CategoryTheory.MonoidalCategory.leftUnitor X).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.leftUnitorNatIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).hom.app X = (CategoryTheory.MonoidalCategory.leftUnitor X).hom

def CategoryTheory.MonoidalCategory.leftUnitorNatIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory.tensorUnitLeft C ≅ CategoryTheory.Functor.id C

The left unitor as a natural isomorphism.

@[simp]

theorem CategoryTheory.MonoidalCategory.rightUnitorNatIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).inv.app X = (CategoryTheory.MonoidalCategory.rightUnitor X).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.rightUnitorNatIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).hom.app X = (CategoryTheory.MonoidalCategory.rightUnitor X).hom

def CategoryTheory.MonoidalCategory.rightUnitorNatIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory.tensorUnitRight C ≅ CategoryTheory.Functor.id C

The right unitor as a natural isomorphism.

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorLeft_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y : C} {Y' : C} (f : Y ⟶ Y') : (CategoryTheory.MonoidalCategory.tensorLeft X).map f = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorLeft_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : (CategoryTheory.MonoidalCategory.tensorLeft X).obj Y = CategoryTheory.MonoidalCategory.tensorObj X Y

def CategoryTheory.MonoidalCategory.tensorLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Functor C C

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

def CategoryTheory.MonoidalCategory.tensorLeftTensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) ≅ CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorLeft Y) (CategoryTheory.MonoidalCategory.tensorLeft X)

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

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).hom.app Z = (CategoryTheory.MonoidalCategory.associator X Y Z).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).inv.app Z = (CategoryTheory.MonoidalCategory.associator X Y Z).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorRight_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y : C} {Y' : C} (f : Y ⟶ Y') : (CategoryTheory.MonoidalCategory.tensorRight X).map f = CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorRight_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : (CategoryTheory.MonoidalCategory.tensorRight X).obj Y = CategoryTheory.MonoidalCategory.tensorObj Y X

def CategoryTheory.MonoidalCategory.tensorRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.Functor C C

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

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringLeft_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.tensoringLeft C).obj X = CategoryTheory.MonoidalCategory.tensorLeft X

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringLeft_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) : ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f).app Z = CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)

def CategoryTheory.MonoidalCategory.tensoringLeft (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor C (CategoryTheory.Functor C C)

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

TODO: show this is an op-monoidal functor.

instance CategoryTheory.MonoidalCategory.instFaithfulFunctorCategoryTensoringLeft (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.tensoringLeft C)

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategory.tensoringRight C).obj X = CategoryTheory.MonoidalCategory.tensorRight X

@[simp]

theorem CategoryTheory.MonoidalCategory.tensoringRight_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) : ((CategoryTheory.MonoidalCategory.tensoringRight C).map f).app Z = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f

def CategoryTheory.MonoidalCategory.tensoringRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor C (CategoryTheory.Functor C C)

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

We later show this is a monoidal functor.

instance CategoryTheory.MonoidalCategory.instFaithfulFunctorCategoryTensoringRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.tensoringRight C)

def CategoryTheory.MonoidalCategory.tensorRightTensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.MonoidalCategory.tensorObj X Y) ≅ CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorRight X) (CategoryTheory.MonoidalCategory.tensorRight Y)

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

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorRightTensor_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.tensorRightTensor X Y).hom.app Z = (CategoryTheory.MonoidalCategory.associator Z X Y).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorRightTensor_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.tensorRightTensor X Y).inv.app Z = (CategoryTheory.MonoidalCategory.associator Z X Y).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_tensorObj (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) (Y : C₁ × C₂) : CategoryTheory.MonoidalCategory.tensorObj X Y = (CategoryTheory.MonoidalCategory.tensorObj X.fst Y.fst, CategoryTheory.MonoidalCategory.tensorObj X.snd Y.snd)

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_associator (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) (Y : C₁ × C₂) (Z : C₁ × C₂) : CategoryTheory.MonoidalCategory.associator X Y Z = CategoryTheory.Iso.prod (CategoryTheory.MonoidalCategory.associator X.fst Y.fst Z.fst) (CategoryTheory.MonoidalCategory.associator X.snd Y.snd Z.snd)

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_tensorUnit' (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] : CategoryTheory.MonoidalCategory.tensorUnit' = (CategoryTheory.MonoidalCategory.tensorUnit C₁, CategoryTheory.MonoidalCategory.tensorUnit C₂)

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_tensorHom (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] : ∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = (CategoryTheory.MonoidalCategory.tensorHom f.fst g.fst, CategoryTheory.MonoidalCategory.tensorHom f.snd g.snd)

instance CategoryTheory.MonoidalCategory.prodMonoidal (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] : CategoryTheory.MonoidalCategory (C₁ × C₂)

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_hom_fst (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.fst = (CategoryTheory.MonoidalCategory.leftUnitor X.fst).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_hom_snd (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.snd = (CategoryTheory.MonoidalCategory.leftUnitor X.snd).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_inv_fst (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.fst = (CategoryTheory.MonoidalCategory.leftUnitor X.fst).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_inv_snd (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.snd = (CategoryTheory.MonoidalCategory.leftUnitor X.snd).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_hom_fst (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.fst = (CategoryTheory.MonoidalCategory.rightUnitor X.fst).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_hom_snd (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.snd = (CategoryTheory.MonoidalCategory.rightUnitor X.snd).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_inv_fst (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.fst = (CategoryTheory.MonoidalCategory.rightUnitor X.fst).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_inv_snd (C₁ : Type u₁) [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.MonoidalCategory C₁] (C₂ : Type u₂) [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.MonoidalCategory C₂] (X : C₁ × C₂) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.snd = (CategoryTheory.MonoidalCategory.rightUnitor X.snd).inv