Constructing monoidal categories and monoidal functors from multifunctors

This file first constructs monoidal category structures from a tensor bifunctor, associator and unitor natural isomorphisms, and pentagon and triangle identities expressed as equalities of natural transformations between quadrifunctors and bifunctors.

It then 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 equalities of natural transformations between trifunctors (F - ⊗ F -) ⊗ F - ⟶ F (- ⊗ (- ⊗ -)) / F ((- ⊗ -) ⊗ -) ⟶ F - ⊗ (F - ⊗ F -), and the unitality conditions are equalities of natural transformations between functors.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.source {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) : Functor C (Functor C (Functor C (Functor C C)))

The source quadrifunctor of the two paths around the monoidal pentagon.

Equations

• CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.source tensor = (CategoryTheory.Functor.postcompose₃.obj tensor).obj (CategoryTheory.bifunctorComp₁₂ tensor tensor)

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.target {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) : Functor C (Functor C (Functor C (Functor C C)))

The target quadrifunctor of the two paths around the monoidal pentagon.

Equations

• CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.target tensor = CategoryTheory.trifunctorComp₂₃₄ tensor (CategoryTheory.bifunctorComp₂₃ tensor tensor)

def CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.firstMap {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) : source tensor ⟶ target tensor

The three-associator path along the top and right of the monoidal pentagon.

((X₁ ⊗ X₂) ⊗ X₃) ⊗ X₄  ---->  (X₁ ⊗ (X₂ ⊗ X₃)) ⊗ X₄
              |                              |
              v                              v
   (X₁ ⊗ X₂) ⊗ (X₃ ⊗ X₄)       X₁ ⊗ ((X₂ ⊗ X₃) ⊗ X₄)
              \                              |
               \                             v
                -----------------> X₁ ⊗ (X₂ ⊗ (X₃ ⊗ X₄))

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.firstMap_app_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) (X X✝ X✝¹ X✝² : C) : ((((firstMap tensor associator).app X).app X✝).app X✝¹).app X✝² = CategoryStruct.comp ((tensor.map (((associator.hom.app X).app X✝).app X✝¹)).app X✝²) (CategoryStruct.comp (((associator.hom.app X).app ((tensor.obj X✝).obj X✝¹)).app X✝²) ((tensor.obj X).map (((associator.hom.app X✝).app X✝¹).app X✝²)))

def CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.secondMap {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) : source tensor ⟶ target tensor

The two-associator path along the left and bottom of the monoidal pentagon displayed in Pentagon.firstMap.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.secondMap_app_app_app_app {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) (X X✝ X✝¹ X✝² : C) : ((((secondMap tensor associator).app X).app X✝).app X✝¹).app X✝² = CategoryStruct.comp (((associator.hom.app ((tensor.obj X).obj X✝)).app X✝¹).app X✝²) (((associator.hom.app X).app X✝).app ((tensor.obj X✝¹).obj X✝²))

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.source {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) : Functor C (Functor C C)

The source bifunctor of the two paths around the monoidal triangle.

Equations

• CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.source tensor unit = (tensor.flip.obj unit).comp tensor

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.middle {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) : Functor C (Functor C C)

The intermediate bifunctor X Y ↦ X ⊗ (𝟙 ⊗ Y) in the monoidal triangle.

Equations

• CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.middle tensor unit = tensor.comp ((CategoryTheory.Functor.whiskeringRight C C C).flip.obj (tensor.obj unit))

def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.associatorMap {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) : source tensor unit ⟶ middle tensor unit

The associator edge of the monoidal triangle.

Equations

• CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.associatorMap tensor unit associator = { app := fun (X : C) => (associator.hom.app X).app unit, naturality := ⋯ }

@[simp]

theorem CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.associatorMap_app {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) (X : C) : (associatorMap tensor unit associator).app X = (associator.hom.app X).app unit

def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.leftUnitorMap {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (leftUnitor : tensor.obj unit ≅ Functor.id C) : middle tensor unit ⟶ tensor

The left-unitor edge of the monoidal triangle.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.leftUnitorMap_app_app {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (leftUnitor : tensor.obj unit ≅ Functor.id C) (X Y : C) : ((leftUnitorMap tensor unit leftUnitor).app X).app Y = (tensor.obj X).map (leftUnitor.hom.app Y)

def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.firstMap {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) (leftUnitor : tensor.obj unit ≅ Functor.id C) : source tensor unit ⟶ tensor

The path around the top and right of the monoidal triangle through the associator and left unitor.

(X₁ ⊗ 𝟙) ⊗ X₂  ---->  X₁ ⊗ (𝟙 ⊗ X₂)
        \                       |
         \                      v
          -----------------> X₁ ⊗ X₂

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.firstMap_app_app {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) (leftUnitor : tensor.obj unit ≅ Functor.id C) (X X✝ : C) : ((firstMap tensor unit associator leftUnitor).app X).app X✝ = CategoryStruct.comp (((associator.hom.app X).app unit).app X✝) ((tensor.obj X).map (leftUnitor.hom.app X✝))

def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.secondMap {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (rightUnitor : tensor.flip.obj unit ≅ Functor.id C) : source tensor unit ⟶ tensor

The diagonal path in the monoidal triangle displayed in Triangle.firstMap, given by the right unitor.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.secondMap_app_app {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (rightUnitor : tensor.flip.obj unit ≅ Functor.id C) (X Y : C) : ((secondMap tensor unit rightUnitor).app X).app Y = (tensor.map (rightUnitor.hom.app X)).app Y

@[instance_reducible]

def CategoryTheory.MonoidalCategory.ofBifunctor {C : Type u_1} [Category.{v_1, u_1} C] (tensor : Functor C (Functor C C)) (unit : C) (associator : bifunctorComp₁₂ tensor tensor ≅ bifunctorComp₂₃ tensor tensor) (leftUnitor : tensor.obj unit ≅ Functor.id C) (rightUnitor : tensor.flip.obj unit ≅ Functor.id C) (pentagon : ofBifunctor.Pentagon.firstMap tensor associator = ofBifunctor.Pentagon.secondMap tensor associator) (triangle : ofBifunctor.Triangle.firstMap tensor unit associator leftUnitor = ofBifunctor.Triangle.secondMap tensor unit rightUnitor) : MonoidalCategory C

Construct a monoidal category from a tensor bifunctor, associator and unitor natural isomorphisms, and pentagon and triangle identities between multifunctor transformations.

Equations

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

@[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 -) ⊗ -.

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPre F = (((CategoryTheory.Functor.whiskeringLeft₂ D).obj F).obj F).obj (CategoryTheory.MonoidalCategory.curriedTensor D)

@[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 (- ⊗ -).

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPost F = (CategoryTheory.Functor.postcompose₂.obj F).obj (CategoryTheory.MonoidalCategory.curriedTensor C)

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

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPostPre F = CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensorPre 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 (- ⊗ -).

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPrePost F = CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.curriedTensorPre F) (CategoryTheory.MonoidalCategory.curriedTensor C)

@[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 ((- ⊗ -) ⊗ -)

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPostPost F = CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C) (CategoryTheory.MonoidalCategory.curriedTensorPost 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 (- ⊗ (- ⊗ -))

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPostPost' F = CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.curriedTensorPost F) (CategoryTheory.MonoidalCategory.curriedTensor C)

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.

Equations

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

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

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

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 -.

Equations

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

@[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 (- ⊗ -).

Equations

• CategoryTheory.MonoidalCategory.curriedTensorPostFunctor = CategoryTheory.Functor.postcompose₂.flip.obj (CategoryTheory.MonoidalCategory.curriedTensor C)

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.

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁ μ = (CategoryTheory.bifunctorComp₁₂Functor.map μ).app (CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₂ F)

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂ μ = (CategoryTheory.bifunctorComp₁₂Functor.obj (CategoryTheory.MonoidalCategory.curriedTensor C)).map μ

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃ F = (CategoryTheory.Functor.postcompose₃.obj F).map (CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).hom

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

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂ μ = (CategoryTheory.bifunctorComp₂₃Functor.obj (CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁ F)).map μ

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃ μ = (CategoryTheory.bifunctorComp₂₃Functor.map μ).app (CategoryTheory.MonoidalCategory.curriedTensor C)

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

Equations

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

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ F = F.whiskerLeft (CategoryTheory.MonoidalCategory.leftUnitorNatIso D).hom

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ ε = F.whiskerLeft ((CategoryTheory.MonoidalCategory.curriedTensor D).map ε)

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ F = CategoryTheory.Functor.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).hom F

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ F = F.whiskerLeft (CategoryTheory.MonoidalCategory.rightUnitorNatIso D).hom

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ ε = F.whiskerLeft ((CategoryTheory.MonoidalCategory.curriedTensor D).flip.map ε)

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

Equations

• CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ F = CategoryTheory.Functor.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).hom F

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

@[instance_reducible]

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.

Equations

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

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.

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁ δ = (CategoryTheory.bifunctorComp₁₂Functor.obj (CategoryTheory.MonoidalCategory.curriedTensor C)).map δ

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂ δ = (CategoryTheory.bifunctorComp₁₂Functor.map δ).app (CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₂ F)

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

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁ F = (CategoryTheory.Functor.postcompose₃.obj F).map (CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).hom

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂ δ = (CategoryTheory.bifunctorComp₂₃Functor.map δ).app (CategoryTheory.MonoidalCategory.curriedTensor C)

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₃ δ = (CategoryTheory.bifunctorComp₂₃Functor.obj (CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁ F)).map δ

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

Equations

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

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ F = F.whiskerLeft (CategoryTheory.MonoidalCategory.leftUnitorNatIso D).inv

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ F = CategoryTheory.Functor.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).inv F

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ η = F.whiskerLeft ((CategoryTheory.MonoidalCategory.curriedTensor D).map η)

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ F = F.whiskerLeft (CategoryTheory.MonoidalCategory.rightUnitorNatIso D).inv

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ F = CategoryTheory.Functor.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).inv F

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

Equations

• CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ η = F.whiskerLeft ((CategoryTheory.MonoidalCategory.curriedTensor D).flip.map η)

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

@[instance_reducible]

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.

Equations

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

@[instance_reducible]

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.

Equations

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

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.

Equations

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