Constructing monoidal functors from natural transformations between multifunctors

This file provides alternative constructors for (op/lax) monoidal functors, given tensorators μ : F - ⊗ F - ⟶ F (- ⊗ -) / δ : F (- ⊗ -) ⟶ F - ⊗ F - as natural transformations between bifunctors. The associativity conditions are phrased as equalities of natural transformations between trifunctors (F - ⊗ F -) ⊗ F - ⟶ F (- ⊗ (- ⊗ -)) / F ((- ⊗ -) ⊗ -) ⟶ F - ⊗ (F - ⊗ F -), and the unitality conditions are phrased as equalities of natural transformation between functors.

Once we have more API for quadrifunctors, we can add constructors for monoidal category structures by phrasing the pentagon axiom as an equality of natural transformations between quadrifunctors.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor C (Functor D D)

The bifunctor (F -) ⊗ -.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₂ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor D (Functor C D)

The bifunctor - ⊗ (F -).

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPre {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor C (Functor C D)

The bifunctor F - ⊗ F -.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPost {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Functor C (Functor C D)

The bifunctor F (- ⊗ -).

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPrePre {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor C (Functor C (Functor C D))

The trifunctor (F - ⊗ F -) ⊗ F -.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPrePre' {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor C (Functor C (Functor C D))

The trifunctor F - ⊗ (F - ⊗ F -).

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPostPre {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor C (Functor C (Functor C D))

The trifunctor F (- ⊗ -) ⊗ F -.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPrePost {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : Functor C (Functor C (Functor C D))

The trifunctor F - ⊗ F (- ⊗ -).

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPostPost {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Functor C (Functor C (Functor C D))

The trifunctor F ((- ⊗ -) ⊗ -)

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPostPost' {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Functor C (Functor C (Functor C D))

The trifunctor F (- ⊗ (- ⊗ -))

def CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : curriedTensorPre F ≅ curriedTensorPost F

The natural isomorphism of bifunctors F - ⊗ F - ≅ F (- ⊗ -), given a monoidal functor F.

@[simp]

theorem CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_hom_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : ((curriedTensorPreIsoPost F).hom.app X).app X✝ = Functor.LaxMonoidal.μ F X X✝

@[simp]

theorem CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_inv_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : ((curriedTensorPreIsoPost F).inv.app X).app X✝ = Functor.OplaxMonoidal.δ F X X✝

def CategoryTheory.MonoidalCategory.curriedTensorPreFunctor {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] : Functor (Functor C D) (Functor C (Functor C D))

The functor which associates to a functor F the bifunctor F - ⊗ F -.

@[simp]

theorem CategoryTheory.MonoidalCategory.curriedTensorPreFunctor_obj {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : curriedTensorPreFunctor.obj F = curriedTensorPre F

@[simp]

theorem CategoryTheory.MonoidalCategory.curriedTensorPreFunctor_map_app_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F₁ F₂ : Functor C D} (f : F₁ ⟶ F₂) (X₁ X₂ : C) : ((curriedTensorPreFunctor.map f).app X₁).app X₂ = tensorHom (f.app X₁) (f.app X₂)

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.curriedTensorPostFunctor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] : Functor (Functor C D) (Functor C (Functor C D))

The functor which associates to a functor F the bifunctor F (- ⊗ -).

Lax monoidal functors

Given a unit morphism ε : 𝟙_ D ⟶ F.obj (𝟙_ C)) and a tensorator μ : F - ⊗ F - ⟶ F (- ⊗ -) such that the diagrams below commute, we define CategoryTheory.Functor.LaxMonoidal.ofBifunctor : F.LaxMonoidal.

Associativity hexagon

      (F - ⊗ F -) ⊗ F -
        /           \
       v             v
F (- ⊗ -) ⊗ F -    F - ⊗ (F - ⊗ F -)
       |             |
       v             v
F ((- ⊗ -) ⊗ -)    F - ⊗ F (- ⊗ -)
        \            /
         v          v
       F (- ⊗ (- ⊗ -))

Left unitality square

𝟙 ⊗ F - ⟶ F 𝟙 ⊗ F -
  |           |
  v           v
  F    ←   F (𝟙 ⊗ -)

Right unitality square

F - ⊗ 𝟙 ⟶ F - ⊗ F 𝟙
  |           |
  v           v
  F   ←   F (- ⊗ 𝟙)

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) : MonoidalCategory.curriedTensorPrePre F ⟶ MonoidalCategory.curriedTensorPostPre F

The top left map in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (X₁ X₂ X₃ : C) : (((firstMap₁ μ).app X₁).app X₂).app X₃ = MonoidalCategoryStruct.whiskerRight ((μ.app X₁).app X₂) (F.obj X₃)

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) : MonoidalCategory.curriedTensorPostPre F ⟶ MonoidalCategory.curriedTensorPostPost F

The middle left map in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (X₁ X₂ X₃ : C) : (((firstMap₂ μ).app X₁).app X₂).app X₃ = (μ.app (MonoidalCategoryStruct.tensorObj X₁ X₂)).app X₃

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : MonoidalCategory.curriedTensorPostPost F ⟶ MonoidalCategory.curriedTensorPostPost' F

The bottom left map in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (X X✝ X✝¹ : C) : (((firstMap₃ F).app X).app X✝).app X✝¹ = F.map (MonoidalCategoryStruct.associator X X✝ X✝¹).hom

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) : MonoidalCategory.curriedTensorPrePre F ⟶ MonoidalCategory.curriedTensorPostPost' F

The composition of the left maps in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (X X✝ X✝¹ : C) : (((firstMap μ).app X).app X✝).app X✝¹ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((μ.app X).app X✝) (F.obj X✝¹)) (CategoryStruct.comp ((μ.app (MonoidalCategoryStruct.tensorObj X X✝)).app X✝¹) (F.map (MonoidalCategoryStruct.associator X X✝ X✝¹).hom))

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : MonoidalCategory.curriedTensorPrePre F ⟶ MonoidalCategory.curriedTensorPrePre' F

The top right map in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) (X X✝ X✝¹ : C) : (((secondMap₁ F).app X).app X✝).app X✝¹ = (MonoidalCategoryStruct.associator (F.obj X) (F.obj X✝) (F.obj X✝¹)).hom

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) : MonoidalCategory.curriedTensorPrePre' F ⟶ MonoidalCategory.curriedTensorPrePost F

The middle right map in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (X₁ X₂ X₃ : C) : (((secondMap₂ μ).app X₁).app X₂).app X₃ = MonoidalCategoryStruct.whiskerLeft (F.obj X₁) ((μ.app X₂).app X₃)

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) : MonoidalCategory.curriedTensorPrePost F ⟶ MonoidalCategory.curriedTensorPostPost' F

The bottom right map in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (X₁ X₂ X₃ : C) : (((secondMap₃ μ).app X₁).app X₂).app X₃ = (μ.app X₁).app (MonoidalCategoryStruct.tensorObj X₂ X₃)

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) : MonoidalCategory.curriedTensorPrePre F ⟶ MonoidalCategory.curriedTensorPostPost' F

The composition of the right maps in the associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (X X✝ X✝¹ : C) : (((secondMap μ).app X).app X✝).app X✝¹ = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj X✝) (F.obj X✝¹)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) ((μ.app X✝).app X✝¹)) ((μ.app X).app (MonoidalCategoryStruct.tensorObj X✝ X✝¹)))

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : F.comp (MonoidalCategory.tensorUnitLeft D) ⟶ F

The left map in the left unitality square.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) (X : C) : (leftMapₗ F).app X = (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) : F.comp (MonoidalCategory.tensorUnitLeft D) ⟶ (MonoidalCategory.curriedTensorPre F).obj (MonoidalCategoryStruct.tensorUnit C)

The top map in the left unitality square.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) (X : C) : (topMapₗ ε).app X = MonoidalCategoryStruct.whiskerRight ε (F.obj X)

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : ((MonoidalCategory.curriedTensor C).obj (MonoidalCategoryStruct.tensorUnit C)).comp F ⟶ F

The bottom map in the left unitality square.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (X : C) : (bottomMapₗ F).app X = F.map (MonoidalCategoryStruct.leftUnitor X).hom

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : F.comp (MonoidalCategory.tensorUnitRight D) ⟶ F

The left map in the right unitality square.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) (X : C) : (leftMapᵣ F).app X = (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) : F.comp (MonoidalCategory.tensorUnitRight D) ⟶ (MonoidalCategory.curriedTensorPre F).flip.obj (MonoidalCategoryStruct.tensorUnit C)

The top map in the right unitality square.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) (X : C) : (topMapᵣ ε).app X = MonoidalCategoryStruct.whiskerLeft (F.obj X) ε

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : ((MonoidalCategory.curriedTensor C).flip.obj (MonoidalCategoryStruct.tensorUnit C)).comp F ⟶ F

The bottom map in the right unitality square.

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (X : C) : (bottomMapᵣ F).app X = F.map (MonoidalCategoryStruct.rightUnitor X).hom

def CategoryTheory.Functor.LaxMonoidal.ofBifunctor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (associativity : ofBifunctor.firstMap μ = ofBifunctor.secondMap μ) (left_unitality : ofBifunctor.leftMapₗ F = CategoryStruct.comp (ofBifunctor.topMapₗ ε) (CategoryStruct.comp (μ.app (MonoidalCategoryStruct.tensorUnit C)) (ofBifunctor.bottomMapₗ F))) (right_unitality : ofBifunctor.leftMapᵣ F = CategoryStruct.comp (ofBifunctor.topMapᵣ ε) (CategoryStruct.comp (((flipFunctor C C D).map μ).app (MonoidalCategoryStruct.tensorUnit C)) (ofBifunctor.bottomMapᵣ F))) : F.LaxMonoidal

F is lax monoidal given a unit morphism ε : 𝟙_ D ⟶ F.obj (𝟙_ C)) and a tensorator μ : F - ⊗ F - ⟶ F (- ⊗ -) as a natural transformation between bifunctors, satisfying the relevant compatibilities.

Oplax monoidal functors

Given a counit morphism η : F.obj (𝟙_ C)) ⟶ 𝟙_ D and a tensorator δ : F (- ⊗ -) ⟶ F - ⊗ F - such that the diagrams below commute, we define CategoryTheory.Functor.OplaxMonoidal.ofBifunctor : F.OplaxMonoidal.

Oplax associativity hexagon

      F ((- ⊗ -) ⊗ -)
        /           \
       v             v
F (- ⊗ -) ⊗ F -      F (- ⊗ (- ⊗ -))
       |                |
       v                v
(F - ⊗ F -) ⊗ F -    F - ⊗ F (- ⊗ -)
        \            /
         v          v
       F - ⊗ (F - ⊗ F -)

Oplax left unitality square

  F   ⟶  F (𝟙 ⊗ -)
  |           |
  v           v
𝟙 ⊗ F - ← F 𝟙 ⊗ F -

Oplax right unitality square

  F  ⟶   F (- ⊗ 𝟙)
  |           |
  v           v
F - ⊗ 𝟙 ← F - ⊗ F 𝟙

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) : MonoidalCategory.curriedTensorPostPost F ⟶ MonoidalCategory.curriedTensorPostPre F

The top left map in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (X₁ X₂ X₃ : C) : (((firstMap₁ δ).app X₁).app X₂).app X₃ = (δ.app (MonoidalCategoryStruct.tensorObj X₁ X₂)).app X₃

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) : MonoidalCategory.curriedTensorPostPre F ⟶ MonoidalCategory.curriedTensorPrePre F

The middle left map in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (X₁ X₂ X₃ : C) : (((firstMap₂ δ).app X₁).app X₂).app X₃ = MonoidalCategoryStruct.whiskerRight ((δ.app X₁).app X₂) (F.obj X₃)

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : MonoidalCategory.curriedTensorPrePre F ⟶ MonoidalCategory.curriedTensorPrePre' F

The bottom left map in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) (X X✝ X✝¹ : C) : (((firstMap₃ F).app X).app X✝).app X✝¹ = (MonoidalCategoryStruct.associator (F.obj X) (F.obj X✝) (F.obj X✝¹)).hom

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) : MonoidalCategory.curriedTensorPostPost F ⟶ MonoidalCategory.curriedTensorPrePre' F

The composition of the three left maps in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (X X✝ X✝¹ : C) : (((firstMap δ).app X).app X✝).app X✝¹ = CategoryStruct.comp ((δ.app (MonoidalCategoryStruct.tensorObj X X✝)).app X✝¹) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((δ.app X).app X✝) (F.obj X✝¹)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj X✝) (F.obj X✝¹)).hom)

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : MonoidalCategory.curriedTensorPostPost F ⟶ MonoidalCategory.curriedTensorPostPost' F

The top right map in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (X X✝ X✝¹ : C) : (((secondMap₁ F).app X).app X✝).app X✝¹ = F.map (MonoidalCategoryStruct.associator X X✝ X✝¹).hom

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) : MonoidalCategory.curriedTensorPostPost' F ⟶ MonoidalCategory.curriedTensorPrePost F

The middle right map in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (X₁ X₂ X₃ : C) : (((secondMap₂ δ).app X₁).app X₂).app X₃ = (δ.app X₁).app (MonoidalCategoryStruct.tensorObj X₂ X₃)

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) : MonoidalCategory.curriedTensorPrePost F ⟶ MonoidalCategory.curriedTensorPrePre' F

The bottom right map in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (X₁ X₂ X₃ : C) : (((secondMap₃ δ).app X₁).app X₂).app X₃ = MonoidalCategoryStruct.whiskerLeft (F.obj X₁) ((δ.app X₂).app X₃)

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) : MonoidalCategory.curriedTensorPostPost F ⟶ MonoidalCategory.curriedTensorPrePre' F

The composition of the three right maps in the oplax associativity hexagon.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (X X✝ X✝¹ : C) : (((secondMap δ).app X).app X✝).app X✝¹ = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X X✝ X✝¹).hom) (CategoryStruct.comp ((δ.app X).app (MonoidalCategoryStruct.tensorObj X✝ X✝¹)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) ((δ.app X✝).app X✝¹)))

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : F ⟶ F.comp (MonoidalCategory.tensorUnitLeft D)

The left map in the oplax left unitality square.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) (X : C) : (leftMapₗ F).app X = (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : F ⟶ ((MonoidalCategory.curriedTensor C).obj (MonoidalCategoryStruct.tensorUnit C)).comp F

The top map in the oplax left unitality square.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (X : C) : (topMapₗ F).app X = F.map (MonoidalCategoryStruct.leftUnitor X).inv

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D) : (MonoidalCategory.curriedTensorPre F).obj (MonoidalCategoryStruct.tensorUnit C) ⟶ F.comp (MonoidalCategory.tensorUnitLeft D)

The bottom map in the oplax left unitality square.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D) (X : C) : (bottomMapₗ η).app X = MonoidalCategoryStruct.whiskerRight η (F.obj X)

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) : F ⟶ F.comp (MonoidalCategory.tensorUnitRight D)

The left map in the oplax right unitality square.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] (F : Functor C D) (X : C) : (leftMapᵣ F).app X = (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : F ⟶ ((MonoidalCategory.curriedTensor C).flip.obj (MonoidalCategoryStruct.tensorUnit C)).comp F

The top map in the oplax right unitality square.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (X : C) : (topMapᵣ F).app X = F.map (MonoidalCategoryStruct.rightUnitor X).inv

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D) : (MonoidalCategory.curriedTensorPre F).flip.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ F.comp (MonoidalCategory.tensorUnitRight D)

The bottom map in the oplax right unitality square.

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D) (X : C) : (bottomMapᵣ η).app X = MonoidalCategoryStruct.whiskerLeft (F.obj X) η

def CategoryTheory.Functor.OplaxMonoidal.ofBifunctor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D) (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (oplax_associativity : ofBifunctor.firstMap δ = ofBifunctor.secondMap δ) (oplax_left_unitality : ofBifunctor.leftMapₗ F = CategoryStruct.comp (ofBifunctor.topMapₗ F) (CategoryStruct.comp (δ.app (MonoidalCategoryStruct.tensorUnit C)) (ofBifunctor.bottomMapₗ η))) (oplax_right_unitality : ofBifunctor.leftMapᵣ F = CategoryStruct.comp (ofBifunctor.topMapᵣ F) (CategoryStruct.comp (((flipFunctor C C D).map δ).app (MonoidalCategoryStruct.tensorUnit C)) (ofBifunctor.bottomMapᵣ η))) : F.OplaxMonoidal

F is oplax monoidal given a counit morphism η : F.obj (𝟙_ C) ⟶ 𝟙_ D and a tensorator δ : F (- ⊗ -) ⟶ F - ⊗ F - as a natural transformation between bifunctors, satisfying the relevant compatibilities.

def CategoryTheory.Functor.Monoidal.ofBifunctor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C)) (μ : MonoidalCategory.curriedTensorPre F ⟶ MonoidalCategory.curriedTensorPost F) (associativity : LaxMonoidal.ofBifunctor.firstMap μ = LaxMonoidal.ofBifunctor.secondMap μ) (left_unitality : LaxMonoidal.ofBifunctor.leftMapₗ F = CategoryStruct.comp (LaxMonoidal.ofBifunctor.topMapₗ ε) (CategoryStruct.comp (μ.app (MonoidalCategoryStruct.tensorUnit C)) (LaxMonoidal.ofBifunctor.bottomMapₗ F))) (right_unitality : LaxMonoidal.ofBifunctor.leftMapᵣ F = CategoryStruct.comp (LaxMonoidal.ofBifunctor.topMapᵣ ε) (CategoryStruct.comp (((flipFunctor C C D).map μ).app (MonoidalCategoryStruct.tensorUnit C)) (LaxMonoidal.ofBifunctor.bottomMapᵣ F))) (η : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D) (δ : MonoidalCategory.curriedTensorPost F ⟶ MonoidalCategory.curriedTensorPre F) (oplax_associativity : OplaxMonoidal.ofBifunctor.firstMap δ = OplaxMonoidal.ofBifunctor.secondMap δ) (oplax_left_unitality : OplaxMonoidal.ofBifunctor.leftMapₗ F = CategoryStruct.comp (OplaxMonoidal.ofBifunctor.topMapₗ F) (CategoryStruct.comp (δ.app (MonoidalCategoryStruct.tensorUnit C)) (OplaxMonoidal.ofBifunctor.bottomMapₗ η))) (oplax_right_unitality : OplaxMonoidal.ofBifunctor.leftMapᵣ F = CategoryStruct.comp (OplaxMonoidal.ofBifunctor.topMapᵣ F) (CategoryStruct.comp (((flipFunctor C C D).map δ).app (MonoidalCategoryStruct.tensorUnit C)) (OplaxMonoidal.ofBifunctor.bottomMapᵣ η))) (ε_η : CategoryStruct.comp ε η = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit D)) (η_ε : CategoryStruct.comp η ε = CategoryStruct.id (F.obj (MonoidalCategoryStruct.tensorUnit C))) (μ_δ : CategoryStruct.comp μ δ = CategoryStruct.id (MonoidalCategory.curriedTensorPre F)) (δ_μ : CategoryStruct.comp δ μ = CategoryStruct.id (MonoidalCategory.curriedTensorPost F)) : F.Monoidal

F is monoidal given a co/unit morphisms ε/η : 𝟙_ D ↔ F.obj (𝟙_ C) and tensorators μ / δ : F - ⊗ F - ↔ F (- ⊗ -) as natural transformations between bifunctors, satisfying the relevant compatibilities.

def CategoryTheory.Functor.CoreMonoidal.ofBifunctor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory D] {F : Functor C D} (ε : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C)) (μ : MonoidalCategory.curriedTensorPre F ≅ MonoidalCategory.curriedTensorPost F) (associativity : LaxMonoidal.ofBifunctor.firstMap μ.hom = LaxMonoidal.ofBifunctor.secondMap μ.hom) (left_unitality : LaxMonoidal.ofBifunctor.leftMapₗ F = CategoryStruct.comp (LaxMonoidal.ofBifunctor.topMapₗ ε.hom) (CategoryStruct.comp (μ.hom.app (MonoidalCategoryStruct.tensorUnit C)) (LaxMonoidal.ofBifunctor.bottomMapₗ F))) (right_unitality : LaxMonoidal.ofBifunctor.leftMapᵣ F = CategoryStruct.comp (LaxMonoidal.ofBifunctor.topMapᵣ ε.hom) (CategoryStruct.comp (((flipFunctor C C D).map μ.hom).app (MonoidalCategoryStruct.tensorUnit C)) (LaxMonoidal.ofBifunctor.bottomMapᵣ F))) : F.CoreMonoidal

F is monoidal given a unit isomorphism ε : 𝟙_ D ≅ F.obj (𝟙_ C) and a tensorator isomorphism μ : F - ⊗ F - ≅ F (- ⊗ -) as a natural isomorphism between bifunctors, satisfying the relevant compatibilities.