(Lax) monoidal functors

A lax monoidal functor F between monoidal categories C and D is a functor between the underlying categories equipped with morphisms

• ε : 𝟙_ D ⟶ F.obj (𝟙_ C) (called the unit morphism)
• μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y) (called the tensorator, or strength). satisfying various axioms. This is implemented as a typeclass F.LaxMonoidal.

Similarly, we define the typeclass F.OplaxMonoidal. For these oplax monoidal functors, we have similar data η and δ, but with morphisms in the opposite direction.

A monoidal functor (F.Monoidal) is defined here as the combination of F.LaxMonoidal and F.OplaxMonoidal, with the additional conditions that ε/η and μ/δ are inverse isomorphisms.

We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.

See Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean for monoidal natural transformations.

We show in Mathlib.CategoryTheory.Monoidal.Mon_ that lax monoidal functors take monoid objects to monoid objects.

References

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

class CategoryTheory.Functor.LaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) : Type (max u₁ v₂)

A functor F : C ⥤ D between monoidal categories is lax monoidal if it is equipped with morphisms ε : 𝟙_ D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the appropriate coherences.

• ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)

  the unit morphism of a lax monoidal functor

• μ (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y)

  the tensorator of a lax monoidal functor

• μ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ F Y X') = CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.whiskerRight f X'))
• μ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ F X' Y) = CategoryStruct.comp (μ F X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
• associativity (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (μ F X (MonoidalCategoryStruct.tensorObj Y Z)))

  associativity of the tensorator

• left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))
• right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))

theorem CategoryTheory.Functor.LaxMonoidal.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} {x y : F.LaxMonoidal} : x = y ↔ ε F = ε F ∧ μ F = μ F

theorem CategoryTheory.Functor.LaxMonoidal.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} {x y : F.LaxMonoidal} (ε : ε F = ε F) (μ : μ F = μ F) : x = y

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.LaxMonoidal] {X Y : C} (X' : C) (f : X ⟶ Y) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryStruct.comp (μ F X' Y) h) = CategoryStruct.comp (μ F X' X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h)

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.LaxMonoidal] {X Y : C} (f : X ⟶ Y) (X' : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y X') ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryStruct.comp (μ F Y X') h) = CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h)

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.associativity_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.LaxMonoidal] (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h))

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.LaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.LaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ F Y Y') = CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.tensorHom f g))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y Y') ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (μ F Y Y') h) = CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h)

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (μ F (MonoidalCategoryStruct.tensorUnit C) X)) = F.map (MonoidalCategoryStruct.leftUnitor X).inv

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (μ F X (MonoidalCategoryStruct.tensorUnit C))) = F.map (MonoidalCategoryStruct.rightUnitor X).inv

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.associativity_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) (F.map (MonoidalCategoryStruct.associator X Y Z).inv)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (μ F (MonoidalCategoryStruct.tensorObj X Y) Z))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h))

theorem CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f) (μ F (MonoidalCategoryStruct.tensorUnit C) X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (F.map (MonoidalCategoryStruct.leftUnitor X).inv))

theorem CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h))

theorem CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F)) (μ F X (MonoidalCategoryStruct.tensorUnit C)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (F.map (MonoidalCategoryStruct.rightUnitor X).inv))

theorem CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h))

theorem CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f) (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))

theorem CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))

theorem CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)) (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))

theorem CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))

theorem CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) (F.map (MonoidalCategoryStruct.associator X Y Z).inv)))

theorem CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h)))

theorem CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)))

theorem CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)))

def CategoryTheory.Functor.LaxMonoidal.ofTensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) (μ : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y)) (μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryStruct.comp (μ X X') (F.map (MonoidalCategoryStruct.tensorHom f g)) := by cat_disch) (associativity : ∀ (X Y Z : C), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ Y Z)) (μ X (MonoidalCategoryStruct.tensorObj Y Z))) := by cat_disch) (left_unitality : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ (MonoidalCategoryStruct.tensorUnit C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by cat_disch) (right_unitality : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε) (CategoryStruct.comp (μ X (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by cat_disch) : F.LaxMonoidal

A constructor for lax monoidal functors whose axioms are described by tensorHom instead of whiskerLeft and whiskerRight.

instance CategoryTheory.Functor.LaxMonoidal.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (Functor.id C).LaxMonoidal

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.id_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (x✝ x✝¹ : C) : μ (Functor.id C) x✝ x✝¹ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((Functor.id C).obj x✝) ((Functor.id C).obj x✝¹))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.id_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : ε (Functor.id C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

instance CategoryTheory.Functor.LaxMonoidal.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] : (F.comp G).LaxMonoidal

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.comp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) : μ (F.comp G) X Y = CategoryStruct.comp (μ G (F.obj X) (F.obj Y)) (G.map (μ F X Y))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.comp_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] : ε (F.comp G) = CategoryStruct.comp (ε G) (G.map (ε F))

class CategoryTheory.Functor.OplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) : Type (max u₁ v₂)

A functor F : C ⥤ D between monoidal categories is oplax monoidal if it is equipped with morphisms η : F.obj (𝟙_ C) ⟶ 𝟙 _D and δ X Y : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y, satisfying the appropriate coherences.

• η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D

  the counit morphism of a lax monoidal functor

• δ (X Y : C) : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)

  the cotensorator of an oplax monoidal functor

• δ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ F Y X')
• δ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (δ F X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ F X' Y)
• oplax_associativity (X Y Z : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)))

  associativity of the tensorator

• oplax_left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))
• oplax_right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))

theorem CategoryTheory.Functor.OplaxMonoidal.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} {x y : F.OplaxMonoidal} (η : η F = η F) (δ : δ F = δ F) : x = y

theorem CategoryTheory.Functor.OplaxMonoidal.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} {x y : F.OplaxMonoidal} : x = y ↔ η F = η F ∧ δ F = δ F

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] {X Y : C} (X' : C) (f : X ⟶ Y) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X') (F.obj Y) ⟶ Z) : CategoryStruct.comp (δ F X' X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (CategoryStruct.comp (δ F X' Y) h)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] {X Y : C} (f : X ⟶ Y) (X' : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj X') ⟶ Z) : CategoryStruct.comp (δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (CategoryStruct.comp (δ F Y X') h)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.associativity {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] (X Y Z : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)))

Alias of CategoryTheory.Functor.OplaxMonoidal.oplax_associativity.

---

associativity of the tensorator

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] (X Y Z : C) {Z✝ : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶ Z✝) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) h))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))

Alias of CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality.

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] (X : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) (F.obj X) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv h = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) h))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))

Alias of CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality.

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.OplaxMonoidal] (X : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv h = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) h))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (δ F Y Y')

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Y') ⟶ Z) : CategoryStruct.comp (δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (δ F Y Y') h)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom) = F.map (MonoidalCategoryStruct.leftUnitor X).hom

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom) = F.map (MonoidalCategoryStruct.rightUnitor X).hom

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) {Z✝ : D} (h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶ Z✝) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) h))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.tensorHom (η F) f) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y) {Z : D} (h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) Y ⟶ Z) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (η F) f) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f) h))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.tensorHom f (η F)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y) {Z : D} (h : MonoidalCategoryStruct.tensorObj Y (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (η F)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)) h))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) {Z✝ : D} (h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶ Z✝) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h)))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) {Z✝ : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶ Z✝) : CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h)))

instance CategoryTheory.Functor.OplaxMonoidal.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (Functor.id C).OplaxMonoidal

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.id_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : η (Functor.id C) = CategoryStruct.id ((Functor.id C).obj (MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.id_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (x✝ x✝¹ : C) : δ (Functor.id C) x✝ x✝¹ = CategoryStruct.id ((Functor.id C).obj (MonoidalCategoryStruct.tensorObj x✝ x✝¹))

instance CategoryTheory.Functor.OplaxMonoidal.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] : (F.comp G).OplaxMonoidal

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.comp_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) : δ (F.comp G) X Y = CategoryStruct.comp (G.map (δ F X Y)) (δ G (F.obj X) (F.obj Y))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.comp_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] : η (F.comp G) = CategoryStruct.comp (G.map (η F)) (η G)

class CategoryTheory.Functor.Monoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) extends F.LaxMonoidal, F.OplaxMonoidal : Type (max u₁ v₂)

A functor between monoidal categories is monoidal if it is lax and oplax monoidals, and both data give inverse isomorphisms.

• ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)
• μ (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y)
• μ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ F Y X') = CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.whiskerRight f X'))
• μ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ F X' Y) = CategoryStruct.comp (μ F X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
• associativity (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (μ F X (MonoidalCategoryStruct.tensorObj Y Z)))
• left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))
• right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))
• η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D
• δ (X Y : C) : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)
• δ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ F Y X')
• δ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (δ F X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ F X' Y)
• oplax_associativity (X Y Z : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)))
• oplax_left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))
• oplax_right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))
• ε_η : CategoryStruct.comp (LaxMonoidal.ε F) (OplaxMonoidal.η F) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit D)
• η_ε : CategoryStruct.comp (OplaxMonoidal.η F) (LaxMonoidal.ε F) = CategoryStruct.id (F.obj (MonoidalCategoryStruct.tensorUnit C))
• μ_δ (X Y : C) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (OplaxMonoidal.δ F X Y) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))
• δ_μ (X Y : C) : CategoryStruct.comp (OplaxMonoidal.δ F X Y) (LaxMonoidal.μ F X Y) = CategoryStruct.id (F.obj (MonoidalCategoryStruct.tensorObj X Y))

theorem CategoryTheory.Functor.Monoidal.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} {x y : F.Monoidal} : x = y ↔ LaxMonoidal.ε F = LaxMonoidal.ε F ∧ LaxMonoidal.μ F = LaxMonoidal.μ F ∧ OplaxMonoidal.η F = OplaxMonoidal.η F ∧ OplaxMonoidal.δ F = OplaxMonoidal.δ F

theorem CategoryTheory.Functor.Monoidal.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} {x y : F.Monoidal} (ε : LaxMonoidal.ε F = LaxMonoidal.ε F) (μ : LaxMonoidal.μ F = LaxMonoidal.μ F) (η : OplaxMonoidal.η F = OplaxMonoidal.η F) (δ : OplaxMonoidal.δ F = OplaxMonoidal.δ F) : x = y

@[simp]

theorem CategoryTheory.Functor.Monoidal.η_ε_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.Monoidal] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z) : CategoryStruct.comp (OplaxMonoidal.η F) (CategoryStruct.comp (LaxMonoidal.ε F) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.ε_η_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.Monoidal] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (OplaxMonoidal.η F) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.δ_μ_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.Monoidal] (X Y : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ Z) : CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (LaxMonoidal.μ F X Y) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_δ_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} (F : Functor C D) [self : F.Monoidal] (X Y : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ Z) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (OplaxMonoidal.δ F X Y) h) = h

def CategoryTheory.Functor.Monoidal.εIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C)

The isomorphism 𝟙_ D ≅ F.obj (𝟙_ C) when F is a monoidal functor.

@[simp]

theorem CategoryTheory.Functor.Monoidal.εIso_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : (εIso F).inv = OplaxMonoidal.η F

@[simp]

theorem CategoryTheory.Functor.Monoidal.εIso_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : (εIso F).hom = LaxMonoidal.ε F

def CategoryTheory.Functor.Monoidal.μIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y)

The isomorphism F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y) when F is a monoidal functor.

@[simp]

theorem CategoryTheory.Functor.Monoidal.μIso_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : (μIso F X Y).hom = LaxMonoidal.μ F X Y

@[simp]

theorem CategoryTheory.Functor.Monoidal.μIso_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : (μIso F X Y).inv = OplaxMonoidal.δ F X Y

instance CategoryTheory.Functor.Monoidal.instIsIsoε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : IsIso (LaxMonoidal.ε F)

instance CategoryTheory.Functor.Monoidal.instIsIsoη {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : IsIso (OplaxMonoidal.η F)

instance CategoryTheory.Functor.Monoidal.instIsIsoμ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : IsIso (LaxMonoidal.μ F X Y)

instance CategoryTheory.Functor.Monoidal.instIsIsoδ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : IsIso (OplaxMonoidal.δ F X Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_ε_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') : CategoryStruct.comp (G.map (LaxMonoidal.ε F)) (G.map (OplaxMonoidal.η F)) = CategoryStruct.id (G.obj (MonoidalCategoryStruct.tensorUnit D))

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_ε_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') {Z : C'} (h : G.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (G.map (LaxMonoidal.ε F)) (CategoryStruct.comp (G.map (OplaxMonoidal.η F)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_η_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') : CategoryStruct.comp (G.map (OplaxMonoidal.η F)) (G.map (LaxMonoidal.ε F)) = CategoryStruct.id (G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_η_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') {Z : C'} (h : G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (G.map (OplaxMonoidal.η F)) (CategoryStruct.comp (G.map (LaxMonoidal.ε F)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_μ_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) : CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) (G.map (OplaxMonoidal.δ F X Y)) = CategoryStruct.id (G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_μ_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) {Z : C'} (h : G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z) : CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) (CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_δ_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) : CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) (G.map (LaxMonoidal.μ F X Y)) = CategoryStruct.id (G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.map_δ_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) {Z : C'} (h : G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z) : CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_ε_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) T)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_ε_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) T ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_η_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorUnit C)) T)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_η_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorUnit C)) T ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) T)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) T ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorUnit D))

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorUnit C)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) h) = h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorObj X Y)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) h) = h

theorem CategoryTheory.Functor.Monoidal.map_tensor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : F.map (MonoidalCategoryStruct.tensorHom f g) = CategoryStruct.comp (OplaxMonoidal.δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (LaxMonoidal.μ F Y Y'))

theorem CategoryTheory.Functor.Monoidal.map_tensor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y Y') ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h = CategoryStruct.comp (OplaxMonoidal.δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (LaxMonoidal.μ F Y Y') h))

theorem CategoryTheory.Functor.Monoidal.map_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Y Z : C} (f : Y ⟶ Z) : F.map (MonoidalCategoryStruct.whiskerLeft X f) = CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (LaxMonoidal.μ F X Z))

theorem CategoryTheory.Functor.Monoidal.map_whiskerLeft_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X Z) ⟶ Z✝) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X f)) h = CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (CategoryStruct.comp (LaxMonoidal.μ F X Z) h))

theorem CategoryTheory.Functor.Monoidal.map_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y : C} (f : X ⟶ Y) (Z : C) : F.map (MonoidalCategoryStruct.whiskerRight f Z) = CategoryStruct.comp (OplaxMonoidal.δ F X Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z)) (LaxMonoidal.μ F Y Z))

theorem CategoryTheory.Functor.Monoidal.map_whiskerRight_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y : C} (f : X ⟶ Y) (Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z✝) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f Z)) h = CategoryStruct.comp (OplaxMonoidal.δ F X Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z)) (CategoryStruct.comp (LaxMonoidal.μ F Y Z) h))

theorem CategoryTheory.Functor.Monoidal.map_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) : F.map (MonoidalCategoryStruct.associator X Y Z).hom = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z)) (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z)))))

theorem CategoryTheory.Functor.Monoidal.map_associator_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z)) (CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h))))

theorem CategoryTheory.Functor.Monoidal.map_associator_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) : F.map (MonoidalCategoryStruct.associator X Y Z).inv = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z)) (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z))))

theorem CategoryTheory.Functor.Monoidal.map_associator_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z) ⟶ Z✝) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z)) (CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h))))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : F.map (MonoidalCategoryStruct.leftUnitor X).hom = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) (F.obj X)) (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom)

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) (F.obj X)) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : F.map (MonoidalCategoryStruct.leftUnitor X).inv = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) (F.obj X)) (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit C) X))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) (F.obj X)) (CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit C) X) h))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : F.map (MonoidalCategoryStruct.rightUnitor X).hom = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.η F)) (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom)

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.η F)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : F.map (MonoidalCategoryStruct.rightUnitor X).inv = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.ε F)) (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorUnit C)))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.ε F)) (CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorUnit C)) h))

@[simp]

theorem CategoryTheory.Functor.Monoidal.inv_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : CategoryTheory.inv (OplaxMonoidal.η F) = LaxMonoidal.ε F

@[simp]

theorem CategoryTheory.Functor.Monoidal.inv_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : CategoryTheory.inv (LaxMonoidal.ε F) = OplaxMonoidal.η F

@[simp]

theorem CategoryTheory.Functor.Monoidal.inv_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : CategoryTheory.inv (LaxMonoidal.μ F X Y) = OplaxMonoidal.δ F X Y

@[simp]

theorem CategoryTheory.Functor.Monoidal.inv_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : CategoryTheory.inv (OplaxMonoidal.δ F X Y) = LaxMonoidal.μ F X Y

noncomputable def CategoryTheory.Functor.Monoidal.μNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : (F.prod F).comp (MonoidalCategory.tensor D) ≅ (MonoidalCategory.tensor C).comp F

The tensorator as a natural isomorphism.

@[simp]

theorem CategoryTheory.Functor.Monoidal.μNatIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C × C) : (μNatIso F).inv.app X = OplaxMonoidal.δ F X.1 X.2

@[simp]

theorem CategoryTheory.Functor.Monoidal.μNatIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C × C) : (μNatIso F).hom.app X = LaxMonoidal.μ F X.1 X.2

noncomputable def CategoryTheory.Functor.Monoidal.commTensorLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : F.comp (MonoidalCategory.tensorLeft (F.obj X)) ≅ (MonoidalCategory.tensorLeft X).comp F

Monoidal functors commute with left tensoring up to isomorphism

@[simp]

theorem CategoryTheory.Functor.Monoidal.commTensorLeft_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : (commTensorLeft F X).hom.app X✝ = LaxMonoidal.μ F X X✝

@[simp]

theorem CategoryTheory.Functor.Monoidal.commTensorLeft_inv_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : (commTensorLeft F X).inv.app X✝ = OplaxMonoidal.δ F X X✝

noncomputable def CategoryTheory.Functor.Monoidal.commTensorRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : F.comp (MonoidalCategory.tensorRight (F.obj X)) ≅ (MonoidalCategory.tensorRight X).comp F

Monoidal functors commute with right tensoring up to isomorphism

@[simp]

theorem CategoryTheory.Functor.Monoidal.commTensorRight_inv_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : (commTensorRight F X).inv.app X✝ = OplaxMonoidal.δ F X✝ X

@[simp]

theorem CategoryTheory.Functor.Monoidal.commTensorRight_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : (commTensorRight F X).hom.app X✝ = LaxMonoidal.μ F X✝ X

instance CategoryTheory.Functor.Monoidal.instId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (Functor.id C).Monoidal

instance CategoryTheory.Functor.Monoidal.instComp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] : (F.comp G).Monoidal

theorem CategoryTheory.Functor.Monoidal.toLaxMonoidal_injective {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) : Function.Injective (@toLaxMonoidal C inst✝ inst✝¹ D inst✝² inst✝³ F)

theorem CategoryTheory.Functor.Monoidal.toOplaxMonoidal_injective {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) : Function.Injective (@toOplaxMonoidal C inst✝ inst✝¹ D inst✝² inst✝³ F)

structure CategoryTheory.Functor.CoreMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) : Type (max u₁ v₂)

Structure which is a helper in order to show that a functor is monoidal. It consists of isomorphisms εIso and μIso such that the morphisms .hom induced by these isomorphisms satisfy the axioms of lax monoidal functors.

• εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C)

  unit morphism

• μIso (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y)

  tensorator

• μIso_hom_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (self.μIso Y X').hom = CategoryStruct.comp (self.μIso X X').hom (F.map (MonoidalCategoryStruct.whiskerRight f X'))
• μIso_hom_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (self.μIso X' Y).hom = CategoryStruct.comp (self.μIso X' X).hom (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
• associativity (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).hom (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom) (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z)).hom)

  associativity of the tensorator

• left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorUnit C) X).hom (F.map (MonoidalCategoryStruct.leftUnitor X).hom))
• right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom) (CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorUnit C)).hom (F.map (MonoidalCategoryStruct.rightUnitor X).hom))

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) {X Y : C} (X' : C) (f : X ⟶ Y) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryStruct.comp (self.μIso X' Y).hom h) = CategoryStruct.comp (self.μIso X' X).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h)

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.associativity_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) (X Y Z : C) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom) (CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z)).hom h))

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) {X Y : C} (f : X ⟶ Y) (X' : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y X') ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryStruct.comp (self.μIso Y X').hom h) = CategoryStruct.comp (self.μIso X X').hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h)

theorem CategoryTheory.Functor.CoreMonoidal.left_unitality_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorUnit C) X).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))

theorem CategoryTheory.Functor.CoreMonoidal.right_unitality_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom) (CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorUnit C)).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))

def CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : F.LaxMonoidal

The lax monoidal functor structure induced by a Functor.CoreMonoidal structure.

theorem CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) (X Y : C) : LaxMonoidal.μ F X Y = (h.μIso X Y).hom

theorem CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : LaxMonoidal.ε F = h.εIso.hom

def CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : F.OplaxMonoidal

The oplax monoidal functor structure induced by a Functor.CoreMonoidal structure.

theorem CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) (X Y : C) : OplaxMonoidal.δ F X Y = (h.μIso X Y).inv

theorem CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : OplaxMonoidal.η F = h.εIso.inv

def CategoryTheory.Functor.CoreMonoidal.toMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : F.Monoidal

The monoidal functor structure induced by a Functor.CoreMonoidal structure.

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : h.toMonoidal.toOplaxMonoidal = h.toOplaxMonoidal

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : h.toMonoidal.toLaxMonoidal = h.toLaxMonoidal

noncomputable def CategoryTheory.Functor.CoreMonoidal.ofLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] [IsIso (LaxMonoidal.ε F)] [∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)] : F.CoreMonoidal

The Functor.CoreMonoidal structure given by a lax monoidal functor such that ε and μ are isomorphisms.

noncomputable def CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] : F.CoreMonoidal

The Functor.CoreMonoidal structure given by an oplax monoidal functor such that η and δ are isomorphisms.

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_μIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] (X Y : C) : (ofOplaxMonoidal F).μIso X Y = (asIso (OplaxMonoidal.δ F X Y)).symm

@[simp]

theorem CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_εIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] : (ofOplaxMonoidal F).εIso = (asIso (OplaxMonoidal.η F)).symm

noncomputable def CategoryTheory.Functor.Monoidal.ofLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] [IsIso (LaxMonoidal.ε F)] [∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)] : F.Monoidal

The Functor.Monoidal structure given by a lax monoidal functor such that ε and μ are isomorphisms.

noncomputable def CategoryTheory.Functor.Monoidal.ofOplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] : F.Monoidal

The Functor.Monoidal structure given by an oplax monoidal functor such that η and δ are isomorphisms.

instance CategoryTheory.Functor.instLaxMonoidalProdProd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] : (F.prod G).LaxMonoidal

@[simp]

theorem CategoryTheory.Functor.prod_ε_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] : (LaxMonoidal.ε (F.prod G)).1 = LaxMonoidal.ε F

@[simp]

theorem CategoryTheory.Functor.prod_ε_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] : (LaxMonoidal.ε (F.prod G)).2 = LaxMonoidal.ε G

@[simp]

theorem CategoryTheory.Functor.prod_μ_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C × E) : (LaxMonoidal.μ (F.prod G) X Y).1 = LaxMonoidal.μ F X.1 Y.1

@[simp]

theorem CategoryTheory.Functor.prod_μ_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C × E) : (LaxMonoidal.μ (F.prod G) X Y).2 = LaxMonoidal.μ G X.2 Y.2

instance CategoryTheory.Functor.instOplaxMonoidalProdProd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] : (F.prod G).OplaxMonoidal

@[simp]

theorem CategoryTheory.Functor.prod_η_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] : (OplaxMonoidal.η (F.prod G)).1 = OplaxMonoidal.η F

@[simp]

theorem CategoryTheory.Functor.prod_η_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] : (OplaxMonoidal.η (F.prod G)).2 = OplaxMonoidal.η G

@[simp]

theorem CategoryTheory.Functor.prod_δ_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C × E) : (OplaxMonoidal.δ (F.prod G) X Y).1 = OplaxMonoidal.δ F X.1 Y.1

@[simp]

theorem CategoryTheory.Functor.prod_δ_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C × E) : (OplaxMonoidal.δ (F.prod G) X Y).2 = OplaxMonoidal.δ G X.2 Y.2

instance CategoryTheory.Functor.instMonoidalProdProd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {C' : Type u₁'} [Category.{v₁', u₁'} C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.Monoidal] [G.Monoidal] : (F.prod G).Monoidal

instance CategoryTheory.Functor.instMonoidalProdDiag {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (diag C).Monoidal

@[simp]

theorem CategoryTheory.Functor.diag_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : LaxMonoidal.ε (diag C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit (C × C))

@[simp]

theorem CategoryTheory.Functor.diag_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : OplaxMonoidal.η (diag C) = CategoryStruct.id ((diag C).obj (MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem CategoryTheory.Functor.diag_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) : LaxMonoidal.μ (diag C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((diag C).obj X) ((diag C).obj Y))

@[simp]

theorem CategoryTheory.Functor.diag_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) : OplaxMonoidal.δ (diag C) X Y = CategoryStruct.id ((diag C).obj (MonoidalCategoryStruct.tensorObj X Y))

instance CategoryTheory.Functor.LaxMonoidal.prod' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] : (F.prod' G).LaxMonoidal

The functor C ⥤ D × E obtained from two lax monoidal functors is lax monoidal.

@[simp]

theorem CategoryTheory.Functor.prod'_ε_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] : (LaxMonoidal.ε (F.prod' G)).1 = LaxMonoidal.ε F

@[simp]

theorem CategoryTheory.Functor.prod'_ε_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] : (LaxMonoidal.ε (F.prod' G)).2 = LaxMonoidal.ε G

@[simp]

theorem CategoryTheory.Functor.prod'_μ_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) : (LaxMonoidal.μ (F.prod' G) X Y).1 = LaxMonoidal.μ F X Y

@[simp]

theorem CategoryTheory.Functor.prod'_μ_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) : (LaxMonoidal.μ (F.prod' G) X Y).2 = LaxMonoidal.μ G X Y

instance CategoryTheory.Functor.OplaxMonoidal.prod' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] : (F.prod' G).OplaxMonoidal

The functor C ⥤ D × E obtained from two oplax monoidal functors is oplax monoidal.

@[simp]

theorem CategoryTheory.Functor.prod'_η_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] : (OplaxMonoidal.η (F.prod' G)).1 = OplaxMonoidal.η F

@[simp]

theorem CategoryTheory.Functor.prod'_η_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] : (OplaxMonoidal.η (F.prod' G)).2 = OplaxMonoidal.η G

@[simp]

theorem CategoryTheory.Functor.prod'_δ_fst {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) : (OplaxMonoidal.δ (F.prod' G) X Y).1 = OplaxMonoidal.δ F X Y

@[simp]

theorem CategoryTheory.Functor.prod'_δ_snd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) : (OplaxMonoidal.δ (F.prod' G) X Y).2 = OplaxMonoidal.δ G X Y

@[deprecated CategoryTheory.prod_comp_fst (since := "2025-06-08")]

theorem CategoryTheory.Functor.prod_comp_fst (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ Z✝ : C × D} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) : (CategoryStruct.comp f g).1 = CategoryStruct.comp f.1 g.1

Alias of CategoryTheory.prod_comp_fst.

@[deprecated CategoryTheory.prod_comp_snd (since := "2025-06-08")]

theorem CategoryTheory.Functor.prod_comp_snd (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ Z✝ : C × D} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) : (CategoryStruct.comp f g).2 = CategoryStruct.comp f.2 g.2

Alias of CategoryTheory.prod_comp_snd.

instance CategoryTheory.Functor.Monoidal.prod' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.Monoidal] [G.Monoidal] : (F.prod' G).Monoidal

The functor C ⥤ D × E obtained from two monoidal functors is monoidal.

def CategoryTheory.Adjunction.rightAdjointLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] : G.LaxMonoidal

The right adjoint of an oplax monoidal functor is lax monoidal.

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] : Functor.LaxMonoidal.ε G = (adj.homEquiv (MonoidalCategoryStruct.tensorUnit C) (MonoidalCategoryStruct.tensorUnit D)) (Functor.OplaxMonoidal.η F)

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] (X Y : D) : Functor.LaxMonoidal.μ G X Y = (adj.homEquiv (MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)))

class CategoryTheory.Adjunction.IsMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] : Prop

When adj : F ⊣ G is an adjunction, with F oplax monoidal and G lax-monoidal, this typeclass expresses compatibilities between the adjunction and the (op)lax monoidal structures.

• leftAdjoint_ε : Functor.LaxMonoidal.ε G = (adj.homEquiv (MonoidalCategoryStruct.tensorUnit C) (MonoidalCategoryStruct.tensorUnit D)) (Functor.OplaxMonoidal.η F)
• leftAdjoint_μ (X Y : D) : Functor.LaxMonoidal.μ G X Y = (adj.homEquiv (MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorObj ((Functor.id D).obj X) ((Functor.id D).obj Y))) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)))

instance CategoryTheory.Adjunction.instIsMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] : adj.IsMonoidal

theorem CategoryTheory.Adjunction.unit_app_unit_comp_map_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] : CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) (G.map (Functor.OplaxMonoidal.η F)) = Functor.LaxMonoidal.ε G

theorem CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {Z : C} (h : G.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (G.map (Functor.OplaxMonoidal.η F)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε G) h

theorem CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : C) : CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (G.map (Functor.OplaxMonoidal.δ F X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y)) (Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y))

theorem CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : C) {Z : C} (h : G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z) : CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (G.map (Functor.OplaxMonoidal.δ F X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)) h)

theorem CategoryTheory.Adjunction.map_ε_comp_counit_app_unit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] : CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G)) (adj.counit.app (MonoidalCategoryStruct.tensorUnit D)) = Functor.OplaxMonoidal.η F

theorem CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G)) (CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorUnit D)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.η F) h

theorem CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : D) : CategoryStruct.comp (F.map (Functor.LaxMonoidal.μ G X Y)) (adj.counit.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))

theorem CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryStruct.comp (F.map (Functor.LaxMonoidal.μ G X Y)) (CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)) h)

instance CategoryTheory.Adjunction.instIsMonoidalId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : id.IsMonoidal

instance CategoryTheory.Adjunction.isMonoidal_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {F' : Functor D E} {G' : Functor E D} (adj' : F' ⊣ G') [F'.OplaxMonoidal] [G'.LaxMonoidal] [adj'.IsMonoidal] : (adj.comp adj').IsMonoidal

theorem CategoryTheory.Adjunction.ε_comp_map_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.Monoidal] [adj.IsMonoidal] : CategoryStruct.comp (Functor.LaxMonoidal.ε G) (G.map (Functor.LaxMonoidal.ε F)) = adj.unit.app (MonoidalCategoryStruct.tensorUnit C)

theorem CategoryTheory.Adjunction.ε_comp_map_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.Monoidal] [adj.IsMonoidal] {Z : C} (h : G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (Functor.LaxMonoidal.ε G) (CategoryStruct.comp (G.map (Functor.LaxMonoidal.ε F)) h) = CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) h

theorem CategoryTheory.Adjunction.map_η_comp_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.Monoidal] [adj.IsMonoidal] : CategoryStruct.comp (F.map (Functor.OplaxMonoidal.η G)) (Functor.OplaxMonoidal.η F) = adj.counit.app (MonoidalCategoryStruct.tensorUnit D)

theorem CategoryTheory.Adjunction.map_η_comp_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.Monoidal] [adj.IsMonoidal] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (F.map (Functor.OplaxMonoidal.η G)) (CategoryStruct.comp (Functor.OplaxMonoidal.η F) h) = CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorUnit D)) h

instance CategoryTheory.Equivalence.instMonoidalFunctorSymmOfInverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.inverse.Monoidal] : e.symm.functor.Monoidal

instance CategoryTheory.Equivalence.instMonoidalInverseSymmOfFunctor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] : e.symm.inverse.Monoidal

noncomputable def CategoryTheory.Equivalence.inverseMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] : e.inverse.Monoidal

If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.

@[reducible, inline]

abbrev CategoryTheory.Equivalence.IsMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] : Prop

An equivalence of categories involving monoidal functors is monoidal if the underlying adjunction satisfies certain compatibilities with respect to the monoidal functor data.

theorem CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorUnit C)) (e.inverse.map (Functor.OplaxMonoidal.η e.functor)) = Functor.LaxMonoidal.ε e.inverse

theorem CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : C} (h : e.inverse.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.η e.functor)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε e.inverse) h

theorem CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) : CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)) (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y))

theorem CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : C} (h : e.inverse.obj (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)) ⟶ Z) : CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h)

theorem CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (e.counitIso.hom.app (MonoidalCategoryStruct.tensorUnit D)) = Functor.OplaxMonoidal.η e.functor

theorem CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (CategoryStruct.comp (e.counitIso.hom.app (MonoidalCategoryStruct.tensorUnit D)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.η e.functor) h

theorem CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y)) (e.counitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y)) (MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y))

theorem CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y)) (CategoryStruct.comp (e.counitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y)) h)

theorem CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorUnit D)) (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) = Functor.LaxMonoidal.ε e.functor

theorem CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : e.functor.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z) : CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorUnit D)) (CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε e.functor) h

theorem CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) : CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y) (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))

theorem CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : D} (h : e.functor.obj (MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))) ⟶ Z) : CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) (CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y) (CategoryStruct.comp (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))) h)

theorem CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorUnit C)) (e.inverse.map (Functor.OplaxMonoidal.η e.functor)) = Functor.LaxMonoidal.ε e.inverse

theorem CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : C} (h : e.inverse.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z) : CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.η e.functor)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε e.inverse) h

theorem CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) : CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unit.app X) (e.unitIso.hom.app Y)) (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y))

theorem CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : C} (h : e.inverse.obj (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)) ⟶ Z) : CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unit.app X) (e.unitIso.hom.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h)

@[simp]

theorem CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (e.counit.app (MonoidalCategoryStruct.tensorUnit D)) = Functor.OplaxMonoidal.η e.functor

@[simp]

theorem CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (CategoryStruct.comp (e.counit.app (MonoidalCategoryStruct.tensorUnit D)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.η e.functor) h

theorem CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y)) (e.counit.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y)) (MonoidalCategoryStruct.tensorHom (e.counit.app X) (e.counit.app Y))

theorem CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) {Z : D} (h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y)) (CategoryStruct.comp (e.counit.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.counit.app X) (e.counit.app Y)) h)

theorem CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.counitInv.app (MonoidalCategoryStruct.tensorUnit D)) (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) = Functor.LaxMonoidal.ε e.functor

theorem CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : e.functor.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z) : CategoryStruct.comp (e.counitInv.app (MonoidalCategoryStruct.tensorUnit D)) (CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε e.functor) h

theorem CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) : CategoryStruct.comp (e.counitInv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y) (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))

theorem CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : D} (h : e.functor.obj (MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))) ⟶ Z) : CategoryStruct.comp (e.counitInv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) (CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y) (CategoryStruct.comp (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))) h)

@[simp]

theorem CategoryTheory.Equivalence.ε_comp_map_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (Functor.LaxMonoidal.ε e.inverse) (e.inverse.map (Functor.LaxMonoidal.ε e.functor)) = e.unit.app (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Equivalence.ε_comp_map_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : C} (h : e.inverse.obj (e.functor.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (Functor.LaxMonoidal.ε e.inverse) (CategoryStruct.comp (e.inverse.map (Functor.LaxMonoidal.ε e.functor)) h) = CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorUnit C)) h

@[simp]

theorem CategoryTheory.Equivalence.map_η_comp_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) (Functor.OplaxMonoidal.η e.functor) = e.counit.app (MonoidalCategoryStruct.tensorUnit D)

@[simp]

theorem CategoryTheory.Equivalence.map_η_comp_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) (CategoryStruct.comp (Functor.OplaxMonoidal.η e.functor) h) = CategoryStruct.comp (e.counit.app (MonoidalCategoryStruct.tensorUnit D)) h

instance CategoryTheory.Equivalence.instMonoidalFunctorRefl {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : refl.functor.Monoidal

instance CategoryTheory.Equivalence.instMonoidalInverseRefl {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : refl.inverse.Monoidal

instance CategoryTheory.Equivalence.isMonoidal_refl {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : refl.IsMonoidal

The obvious auto-equivalence of a monoidal category is monoidal.

instance CategoryTheory.Equivalence.isMonoidal_symm {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.symm.IsMonoidal

The inverse of a monoidal category equivalence is also a monoidal category equivalence.

instance CategoryTheory.Equivalence.instMonoidalFunctorTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (e : C ≌ D) [e.functor.Monoidal] (e' : D ≌ E) [e'.functor.Monoidal] : (e.trans e').functor.Monoidal

instance CategoryTheory.Equivalence.instMonoidalInverseTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (e : C ≌ D) [e.inverse.Monoidal] (e' : D ≌ E) [e'.inverse.Monoidal] : (e.trans e').inverse.Monoidal

instance CategoryTheory.Equivalence.isMonoidal_trans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (e' : D ≌ E) [e'.functor.Monoidal] [e'.inverse.Monoidal] [e'.IsMonoidal] : (e.trans e').IsMonoidal

The composition of two monoidal category equivalences is monoidal.

structure CategoryTheory.LaxMonoidalFunctor (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] extends CategoryTheory.Functor C D : Type (max (max (max u₁ u₂) v₁) v₂)

Bundled version of lax monoidal functors. This type is equipped with a category structure in CategoryTheory.Monoidal.NaturalTransformation.

• obj : C → D
• map {X Y : C} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id (X : C) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
• laxMonoidal : self.LaxMonoidal

def CategoryTheory.LaxMonoidalFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : LaxMonoidalFunctor C D

Constructor for LaxMonoidalFunctor C D.

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : (of F).toFunctor = F