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

• ε' : 𝟙_ D ⟶ F.obj (𝟙_ C)

  unit morphism

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

  tensorator

• μ'_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ' Y X') = CategoryStruct.comp (μ' 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)) (μ' X' Y) = CategoryStruct.comp (μ' X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
• associativity' (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ' X Y) (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.whiskerLeft (F.obj X) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z)))

  associativity of the tensorator

• left_unitality' (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ε' (F.obj X)) (CategoryStruct.comp (μ' (𝟙_ 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) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))

def 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) [F.LaxMonoidal] : 𝟙_ D ⟶ F.obj (𝟙_ C)

the unit morphism of a lax monoidal functor

Equations

• CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε'

def 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) [F.LaxMonoidal] (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y)

the tensorator of a lax monoidal functor

Equations

• CategoryTheory.Functor.LaxMonoidal.μ F X Y = CategoryTheory.Functor.LaxMonoidal.μ' X Y

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_left {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 : 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'))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_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) [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.μ_natural_right {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 : 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))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.μ_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) [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.associativity {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)) (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)))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.associativity_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.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))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality {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) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))

theorem CategoryTheory.Functor.LaxMonoidal.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) [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 (𝟙_ C) X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality {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) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))

theorem CategoryTheory.Functor.LaxMonoidal.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) [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 (𝟙_ 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 (𝟙_ 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 (𝟙_ C) X) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (𝟙_ 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 (𝟙_ 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 (𝟙_ C)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (𝟙_ 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))

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} (ε' : 𝟙_ D ⟶ F.obj (𝟙_ 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 aesop_cat) (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 aesop_cat) (left_unitality' : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by aesop_cat) (right_unitality' : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by aesop_cat) : F.LaxMonoidal

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

Equations

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

theorem 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} (ε' : 𝟙_ D ⟶ F.obj (𝟙_ 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 aesop_cat) (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 aesop_cat) (left_unitality' : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by aesop_cat) (right_unitality' : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by aesop_cat) : ε F = ε'

theorem 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} (ε' : 𝟙_ D ⟶ F.obj (𝟙_ 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 aesop_cat) (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 aesop_cat) (left_unitality' : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by aesop_cat) (right_unitality' : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by aesop_cat) : μ F = μ'

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

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 (𝟙_ C) ⟶ 𝟙_ D

  counit morphism

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

  cotensorator

• δ'_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (δ' X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ' Y X')
• δ'_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (δ' X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ' X' Y)
• oplax_associativity' (X Y Z : C) : CategoryStruct.comp (δ' (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ' 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 (δ' X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ' 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 (δ' (𝟙_ C) X) (MonoidalCategoryStruct.whiskerRight η' (F.obj X)))
• oplax_right_unitality' (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ' X (𝟙_ C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) η'))

def 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) [F.OplaxMonoidal] : F.obj (𝟙_ C) ⟶ 𝟙_ D

the counit morphism of a lax monoidal functor

Equations

• CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η'

def 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) [F.OplaxMonoidal] (X Y : C) : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)

the cotensorator of an oplax monoidal functor

Equations

• CategoryTheory.Functor.OplaxMonoidal.δ F X Y = CategoryTheory.Functor.OplaxMonoidal.δ' X Y

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_left {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 : 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')

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_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) [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.δ_natural_right {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 : 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)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_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) [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.associativity {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) (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)))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_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 (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₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (𝟙_ C) X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))

theorem CategoryTheory.Functor.OplaxMonoidal.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) [F.OplaxMonoidal] (X : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (𝟙_ 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 (𝟙_ C) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) h))

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality {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) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (𝟙_ C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))

theorem CategoryTheory.Functor.OplaxMonoidal.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) [F.OplaxMonoidal] (X : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (𝟙_ D) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv h = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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))

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

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.

• ε' : 𝟙_ D ⟶ F.obj (𝟙_ 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')) (μ' Y X') = CategoryStruct.comp (μ' 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)) (μ' X' Y) = CategoryStruct.comp (μ' X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
• associativity' (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ' X Y) (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.whiskerLeft (F.obj X) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z)))
• left_unitality' (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ε' (F.obj X)) (CategoryStruct.comp (μ' (𝟙_ 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) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))
• η' : F.obj (𝟙_ C) ⟶ 𝟙_ 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 (δ' X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ' Y X')
• δ'_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (δ' X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ' X' Y)
• oplax_associativity' (X Y Z : C) : CategoryStruct.comp (δ' (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ' 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 (δ' X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ' Y Z)))
• oplax_left_unitality' (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ' (𝟙_ C) X) (MonoidalCategoryStruct.whiskerRight η' (F.obj X)))
• oplax_right_unitality' (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ' X (𝟙_ C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) η'))
• ε_η : CategoryStruct.comp (LaxMonoidal.ε F) (OplaxMonoidal.η F) = CategoryStruct.id (𝟙_ D)
• η_ε : CategoryStruct.comp (OplaxMonoidal.η F) (LaxMonoidal.ε F) = CategoryStruct.id (F.obj (𝟙_ 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))

@[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 : 𝟙_ 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 : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ Z) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (OplaxMonoidal.δ 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] {Z : D} (h : F.obj (𝟙_ 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] (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

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] : 𝟙_ D ≅ F.obj (𝟙_ C)

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

Equations

• CategoryTheory.Functor.Monoidal.εIso F = { hom := CategoryTheory.Functor.LaxMonoidal.ε F, inv := CategoryTheory.Functor.OplaxMonoidal.η F, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

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.

Equations

• CategoryTheory.Functor.Monoidal.μIso F X Y = { hom := CategoryTheory.Functor.LaxMonoidal.μ F X Y, inv := CategoryTheory.Functor.OplaxMonoidal.δ F X Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ C)) h))

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.

Equations

• CategoryTheory.Functor.Monoidal.μNatIso F = CategoryTheory.NatIso.ofComponents (fun (x : C × C) => CategoryTheory.Functor.Monoidal.μIso 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

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

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

Equations

• CategoryTheory.Functor.Monoidal.commTensorLeft F X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => CategoryTheory.Functor.Monoidal.μIso F X Y) ⋯

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

Equations

• CategoryTheory.Functor.Monoidal.commTensorRight F X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => CategoryTheory.Functor.Monoidal.μIso F Y X) ⋯

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

Equations

• CategoryTheory.Functor.Monoidal.instId = CategoryTheory.Functor.Monoidal.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• CategoryTheory.Functor.Monoidal.instComp F G = CategoryTheory.Functor.Monoidal.mk ⋯ ⋯ ⋯ ⋯

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 : 𝟙_ D ≅ F.obj (𝟙_ 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 (𝟙_ 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 (𝟙_ C)).hom (F.map (MonoidalCategoryStruct.rightUnitor X).hom))

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

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

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 (𝟙_ 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 (𝟙_ 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.

Equations

• h.toLaxMonoidal = { ε' := h.εIso.hom, μ' := fun (X Y : C) => (h.μIso X Y).hom, μ'_natural_left := ⋯, μ'_natural_right := ⋯, associativity' := ⋯, left_unitality' := ⋯, right_unitality' := ⋯ }

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

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

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.

Equations

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

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

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

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.

Equations

• h.toMonoidal = CategoryTheory.Functor.Monoidal.mk ⋯ ⋯ ⋯ ⋯

@[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) : Monoidal.toLaxMonoidal = h.toLaxMonoidal

@[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) : Monoidal.toOplaxMonoidal = h.toOplaxMonoidal

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.Functor.Monoidal.ofLaxMonoidal F = (CategoryTheory.Functor.CoreMonoidal.ofLaxMonoidal F).toMonoidal

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.

Equations

• CategoryTheory.Functor.Monoidal.ofOplaxMonoidal F = (CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal F).toMonoidal

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

Equations

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

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

Equations

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

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

Equations

• F.instMonoidalProdProd G = CategoryTheory.Functor.Monoidal.mk ⋯ ⋯ ⋯ ⋯

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.diag_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : OplaxMonoidal.η (diag C) = CategoryStruct.id ((diag C).obj (𝟙_ 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.

Equations

• CategoryTheory.Functor.LaxMonoidal.prod' F G = inferInstanceAs ((CategoryTheory.Functor.diag C).comp (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] (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.

Equations

• CategoryTheory.Functor.OplaxMonoidal.prod' F G = inferInstanceAs ((CategoryTheory.Functor.diag C).comp (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] (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

@[simp]

theorem CategoryTheory.Functor.prod_comp_fst {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {X Y Z : C × D} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).1 = CategoryStruct.comp f.1 g.1

theorem CategoryTheory.Functor.prod_comp_fst_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {X Y Z : C × D} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.1 ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).1 h = CategoryStruct.comp f.1 (CategoryStruct.comp g.1 h)

@[simp]

theorem CategoryTheory.Functor.prod_comp_snd {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {X Y Z : C × D} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).2 = CategoryStruct.comp f.2 g.2

theorem CategoryTheory.Functor.prod_comp_snd_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {X Y Z : C × D} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : D} (h : Z.2 ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).2 h = CategoryStruct.comp f.2 (CategoryStruct.comp g.2 h)

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.

Equations

• CategoryTheory.Functor.Monoidal.prod' F G = CategoryTheory.Functor.Monoidal.mk ⋯ ⋯ ⋯ ⋯

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.

Equations

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

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 (𝟙_ C) (𝟙_ D)) (Functor.OplaxMonoidal.η F)

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 ((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)))

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 monoidal, this typeclass expresses compatibilities between the adjunction and the (op)lax monoidal structures.

• leftAdjoint_ε : Functor.LaxMonoidal.ε G = (adj.homEquiv (𝟙_ C) (𝟙_ 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 (𝟙_ 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 (𝟙_ D) ⟶ Z) : CategoryStruct.comp (adj.unit.app (𝟙_ 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 (𝟙_ 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 : 𝟙_ D ⟶ Z) : CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G)) (CategoryStruct.comp (adj.counit.app (𝟙_ 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

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

Equations

• e.instMonoidalFunctorSymmOfInverse = inferInstanceAs e.inverse.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

Equations

• e.instMonoidalInverseSymmOfFunctor = inferInstanceAs e.functor.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.

Equations

• e.inverseMonoidal = CategoryTheory.Functor.Monoidal.ofLaxMonoidal e.inverse

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

Equations

• e.IsMonoidal = e.toAdjunction.IsMonoidal

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 (𝟙_ 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 (𝟙_ D) ⟶ Z) : CategoryStruct.comp (e.unitIso.hom.app (𝟙_ 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 (𝟙_ 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 : 𝟙_ D ⟶ Z) : CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (CategoryStruct.comp (e.counitIso.hom.app (𝟙_ 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 (𝟙_ 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 (𝟙_ C) ⟶ Z) : CategoryStruct.comp (e.counitIso.inv.app (𝟙_ 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)

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

Equations

• CategoryTheory.Equivalence.instMonoidalFunctorRefl = inferInstanceAs (CategoryTheory.Functor.id C).Monoidal

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

Equations

• CategoryTheory.Equivalence.instMonoidalInverseRefl = inferInstanceAs (CategoryTheory.Functor.id C).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

Equations

• e.instMonoidalFunctorTrans e' = inferInstanceAs (e.functor.comp 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

Equations

• e.instMonoidalInverseTrans e' = inferInstanceAs (e'.inverse.comp 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.

Equations

• CategoryTheory.LaxMonoidalFunctor.of F = { toFunctor := F, laxMonoidal := inferInstance }

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