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

A monoidal functor is a lax monoidal functor for which ε and μ are isomorphisms.

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

See also CategoryTheory.Monoidal.Functorial for a typeclass decorating an object-level function with the additional data of a monoidal functor. This is useful when stating that a pre-existing functor is monoidal.

See CategoryTheory.Monoidal.NaturalTransformation for monoidal natural transformations.

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

Future work

• Oplax monoidal functors.

References

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

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

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
• ε : CategoryTheory.MonoidalCategory.tensorUnit D ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorUnit C)

  unit morphism

• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (s.obj X) (s.obj Y) ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)

  tensorator

• μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.map f) (s.map g)) (CategoryTheory.LaxMonoidalFunctor.μ s Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s X X') (s.map (CategoryTheory.MonoidalCategory.tensorHom f g))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ s X Y) (CategoryTheory.CategoryStruct.id (s.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (s.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (s.obj X) (s.obj Y) (s.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ s Y Z)) (CategoryTheory.LaxMonoidalFunctor.μ s X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))

  associativity of the tensorator

• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.ε (CategoryTheory.CategoryStruct.id (s.obj X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s (CategoryTheory.MonoidalCategory.tensorUnit C) X) (s.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) s.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s X (CategoryTheory.MonoidalCategory.tensorUnit C)) (s.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

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

@[simp]

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

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.associativity_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (self : CategoryTheory.LaxMonoidalFunctor C D) (X : C) (Y : C) (Z : C) {Z : D} (h : self.obj (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ self X Y) (CategoryTheory.CategoryStruct.id (self.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ self (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (self.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ self Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ self X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) h))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
• ε : CategoryTheory.MonoidalCategory.tensorUnit D ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorUnit C)
• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (s.obj X) (s.obj Y) ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
• μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.map f) (s.map g)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X X') (s.map (CategoryTheory.MonoidalCategory.tensorHom f g))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y) (CategoryTheory.CategoryStruct.id (s.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (s.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (s.obj X) (s.obj Y) (s.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Z)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.ε (CategoryTheory.CategoryStruct.id (s.obj X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit C) X) (s.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) s.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorUnit C)) (s.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
• ε_isIso : CategoryTheory.IsIso s.ε
• μ_isIso : ∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y)

A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.

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

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

The unit morphism of a (strong) monoidal functor as an isomorphism.

Equations

• CategoryTheory.MonoidalFunctor.εIso F = CategoryTheory.asIso F.ε

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

The tensorator of a (strong) monoidal functor as an isomorphism.

Equations

• CategoryTheory.MonoidalFunctor.μIso F X Y = CategoryTheory.asIso (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)

@[simp]

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

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.id_toFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.LaxMonoidalFunctor.id C).toFunctor = CategoryTheory.Functor.id C

@[simp]

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

def CategoryTheory.LaxMonoidalFunctor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidalFunctor C C

The identity lax monoidal functor.

Equations

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

instance CategoryTheory.LaxMonoidalFunctor.instInhabitedLaxMonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Inhabited (CategoryTheory.LaxMonoidalFunctor C C)

Equations

• CategoryTheory.LaxMonoidalFunctor.instInhabitedLaxMonoidalFunctor C = { default := CategoryTheory.LaxMonoidalFunctor.id C }

theorem CategoryTheory.MonoidalFunctor.map_tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {X : C} {Y : C} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : F.map (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X X')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y Y'))

theorem CategoryTheory.MonoidalFunctor.map_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) : F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit C) X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv F.ε) (CategoryTheory.CategoryStruct.id (F.obj X))) (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom)

theorem CategoryTheory.MonoidalFunctor.map_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) : F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorUnit C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) (CategoryTheory.inv F.ε)) (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom)

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

The tensorator as a natural isomorphism.

Equations

• CategoryTheory.MonoidalFunctor.μNatIso F = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.MonoidalFunctor.μIso F X.fst X.snd

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.μ_inv_hom_id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.μIso F X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y) h) = h

@[simp]

theorem CategoryTheory.MonoidalFunctor.μ_inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.μIso F X Y).inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y) = CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))

@[simp]

theorem CategoryTheory.MonoidalFunctor.μ_hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y) (CategoryTheory.MonoidalFunctor.μIso F X Y).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y))

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.ε_inv_hom_id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorUnit C) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.εIso F).inv (CategoryTheory.CategoryStruct.comp F.ε h) = h

@[simp]

theorem CategoryTheory.MonoidalFunctor.ε_inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.εIso F).inv F.ε = CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategory.tensorUnit C))

@[simp]

theorem CategoryTheory.MonoidalFunctor.ε_hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) : CategoryTheory.CategoryStruct.comp F.ε (CategoryTheory.MonoidalFunctor.εIso F).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit D)

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.commTensorLeft_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (X : C) : (CategoryTheory.MonoidalFunctor.commTensorLeft F X).inv.app X = (CategoryTheory.MonoidalFunctor.μIso F X X).inv

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

Monoidal functors commute with left tensoring up to isomorphism

Equations

• CategoryTheory.MonoidalFunctor.commTensorLeft F X = CategoryTheory.NatIso.ofComponents fun Y => CategoryTheory.MonoidalFunctor.μIso F X Y

@[simp]

theorem CategoryTheory.MonoidalFunctor.commTensorRight_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (X : C) : (CategoryTheory.MonoidalFunctor.commTensorRight F X).inv.app X = (CategoryTheory.MonoidalFunctor.μIso F X X).inv

@[simp]

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

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

Monoidal functors commute with right tensoring up to isomorphism

Equations

• CategoryTheory.MonoidalFunctor.commTensorRight F X = CategoryTheory.NatIso.ofComponents fun Y => CategoryTheory.MonoidalFunctor.μIso F Y X

@[simp]

theorem CategoryTheory.MonoidalFunctor.id_toLaxMonoidalFunctor_toFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalFunctor.id C).toLaxMonoidalFunctor.toFunctor = CategoryTheory.Functor.id C

@[simp]

theorem CategoryTheory.MonoidalFunctor.id_toLaxMonoidalFunctor_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalFunctor.id C).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)

@[simp]

theorem CategoryTheory.MonoidalFunctor.id_toLaxMonoidalFunctor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalFunctor.id C).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk (CategoryTheory.Functor.id C).toPrefunctor).obj X) ((CategoryTheory.Functor.mk (CategoryTheory.Functor.id C).toPrefunctor).obj Y))

def CategoryTheory.MonoidalFunctor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalFunctor C C

The identity monoidal functor.

Equations

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

instance CategoryTheory.MonoidalFunctor.instInhabitedMonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Inhabited (CategoryTheory.MonoidalFunctor C C)

Equations

• CategoryTheory.MonoidalFunctor.instInhabitedMonoidalFunctor C = { default := CategoryTheory.MonoidalFunctor.id C }

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.comp_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor D E) : (F ⊗⋙ G).toFunctor = CategoryTheory.Functor.comp F.toFunctor G.toFunctor

@[simp]

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

@[simp]

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

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

The composition of two lax monoidal functors is again lax monoidal.

Equations

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

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

The composition of two lax monoidal functors is again lax monoidal.

Equations

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

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) : (CategoryTheory.LaxMonoidalFunctor.prod F G).ε = (F.ε, G.ε)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) (X : B × D) (Y : B × D) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.LaxMonoidalFunctor.prod F G) X Y = (CategoryTheory.LaxMonoidalFunctor.μ F X.fst Y.fst, CategoryTheory.LaxMonoidalFunctor.μ G X.snd Y.snd)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) : (CategoryTheory.LaxMonoidalFunctor.prod F G).toFunctor = CategoryTheory.Functor.prod F.toFunctor G.toFunctor

def CategoryTheory.LaxMonoidalFunctor.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) : CategoryTheory.LaxMonoidalFunctor (B × D) (C × E)

The cartesian product of two lax monoidal functors is lax monoidal.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.diag_toLaxMonoidalFunctor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalFunctor.diag C).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk (CategoryTheory.Functor.diag C).toPrefunctor).obj X) ((CategoryTheory.Functor.mk (CategoryTheory.Functor.diag C).toPrefunctor).obj Y))

@[simp]

theorem CategoryTheory.MonoidalFunctor.diag_toLaxMonoidalFunctor_toFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalFunctor.diag C).toLaxMonoidalFunctor.toFunctor = CategoryTheory.Functor.diag C

@[simp]

theorem CategoryTheory.MonoidalFunctor.diag_toLaxMonoidalFunctor_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalFunctor.diag C).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit (C × C))

def CategoryTheory.MonoidalFunctor.diag (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalFunctor C (C × C)

The diagonal functor as a monoidal functor.

Equations

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

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

The cartesian product of two lax monoidal functors starting from the same monoidal category C is lax monoidal.

Equations

• CategoryTheory.LaxMonoidalFunctor.prod' F G = (CategoryTheory.MonoidalFunctor.diag C).toLaxMonoidalFunctor ⊗⋙ CategoryTheory.LaxMonoidalFunctor.prod F G

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod'_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor C E) : (CategoryTheory.LaxMonoidalFunctor.prod' F G).toFunctor = CategoryTheory.Functor.prod' F.toFunctor G.toFunctor

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.comp_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.MonoidalFunctor C D) (G : CategoryTheory.MonoidalFunctor D E) : (F ⊗⋙ G).toLaxMonoidalFunctor = F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor

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

The composition of two monoidal functors is again monoidal.

Equations

• F ⊗⋙ G = let src := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor; CategoryTheory.MonoidalFunctor.mk (CategoryTheory.LaxMonoidalFunctor.mk src.toFunctor src.ε src.μ)

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

The composition of two monoidal functors is again monoidal.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.prod_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.MonoidalFunctor B C) (G : CategoryTheory.MonoidalFunctor D E) : (CategoryTheory.MonoidalFunctor.prod F G).toLaxMonoidalFunctor = CategoryTheory.LaxMonoidalFunctor.prod F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor

def CategoryTheory.MonoidalFunctor.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.MonoidalFunctor B C) (G : CategoryTheory.MonoidalFunctor D E) : CategoryTheory.MonoidalFunctor (B × D) (C × E)

The cartesian product of two monoidal functors is monoidal.

Equations

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

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

The cartesian product of two monoidal functors starting from the same monoidal category C is monoidal.

Equations

• CategoryTheory.MonoidalFunctor.prod' F G = CategoryTheory.MonoidalFunctor.diag C ⊗⋙ CategoryTheory.MonoidalFunctor.prod F G

@[simp]

theorem CategoryTheory.MonoidalFunctor.prod'_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.MonoidalFunctor C D) (G : CategoryTheory.MonoidalFunctor C E) : (CategoryTheory.MonoidalFunctor.prod' F G).toLaxMonoidalFunctor = CategoryTheory.LaxMonoidalFunctor.prod' F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor

@[simp]

theorem CategoryTheory.monoidalAdjoint_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) (X : D) (Y : D) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.monoidalAdjoint F h) X Y = ↑(CategoryTheory.Adjunction.homEquiv h (CategoryTheory.MonoidalCategory.tensorObj (G.obj X) (G.obj Y)) (CategoryTheory.MonoidalCategory.tensorObj X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y))) (CategoryTheory.MonoidalCategory.tensorHom (h.counit.app X) (h.counit.app Y)))

@[simp]

theorem CategoryTheory.monoidalAdjoint_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) : (CategoryTheory.monoidalAdjoint F h).ε = ↑(CategoryTheory.Adjunction.homEquiv h (CategoryTheory.MonoidalCategory.tensorUnit C) (CategoryTheory.MonoidalCategory.tensorUnit D)) (CategoryTheory.inv F.ε)

@[simp]

theorem CategoryTheory.monoidalAdjoint_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) : (CategoryTheory.monoidalAdjoint F h).toFunctor = G

noncomputable def CategoryTheory.monoidalAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) : CategoryTheory.LaxMonoidalFunctor D C

If we have a right adjoint functor G to a monoidal functor F, then G has a lax monoidal structure as well.

Equations

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

@[simp]

theorem CategoryTheory.monoidalInverse_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] : (CategoryTheory.monoidalInverse F).toLaxMonoidalFunctor = CategoryTheory.monoidalAdjoint F (CategoryTheory.Functor.asEquivalence F.toLaxMonoidalFunctor.1).toAdjunction

noncomputable def CategoryTheory.monoidalInverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] : CategoryTheory.MonoidalFunctor D C

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

Equations

• CategoryTheory.monoidalInverse F = CategoryTheory.MonoidalFunctor.mk (CategoryTheory.monoidalAdjoint F (CategoryTheory.Functor.asEquivalence F.toLaxMonoidalFunctor.1).toAdjunction)