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

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

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.

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

  unit morphism

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

  tensorator

• μ_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.toPrefunctor.map f) (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X'))) (self.μ Y X') = CategoryTheory.CategoryStruct.comp (self.μ X X') (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X')))
• μ_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X')) (self.toPrefunctor.map f)) (self.μ X' Y) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X') f))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.μ X Y) (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj Z))) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.toPrefunctor.obj X) (self.toPrefunctor.obj Y) (self.toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X)) (self.μ Y Z)) (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))

  associativity of the tensorator

• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (self.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.ε (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp (self.μ (𝟙_ C) X) (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (self.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X)) self.ε) (CategoryTheory.CategoryStruct.comp (self.μ X (𝟙_ C)) (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_left_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} (f : X ⟶ Y) (X' : C) {Z : D} (h : self.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj Y X') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.toPrefunctor.map f) (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X'))) (CategoryTheory.CategoryStruct.comp (self.μ Y X') h) = CategoryTheory.CategoryStruct.comp (self.μ X X') (CategoryTheory.CategoryStruct.comp (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X'))) h)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_right_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) (f : X ⟶ Y) {Z : D} (h : self.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X' Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X')) (self.toPrefunctor.map f)) (CategoryTheory.CategoryStruct.comp (self.μ X' Y) h) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (CategoryTheory.CategoryStruct.comp (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X') f)) 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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.μ X Y) (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj Z✝))) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) (CategoryTheory.CategoryStruct.comp (self.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z✝).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.toPrefunctor.obj X) (self.toPrefunctor.obj Y) (self.toPrefunctor.obj Z✝)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (self.toPrefunctor.obj X)) (self.μ Y Z✝)) (CategoryTheory.CategoryStruct.comp (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) h))

@[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] (F : CategoryTheory.LaxMonoidalFunctor C D) {X : C} {Y : C} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj Y Y') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (CategoryTheory.CategoryStruct.comp (F.μ Y Y') h) = CategoryTheory.CategoryStruct.comp (F.μ X X') (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g)) h)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural {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} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (F.μ Y Y') = CategoryTheory.CategoryStruct.comp (F.μ X X') (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g))

@[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] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) (Y : C) (Z : C) {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.μ X Y) (F.toPrefunctor.obj Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z✝).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z✝)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) (F.μ Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) h))

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.associativity' {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.whiskerRight (F.μ X Y) (F.toPrefunctor.obj Z)) (CategoryTheory.CategoryStruct.comp (F.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) (F.μ Y Z)) (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))

theorem CategoryTheory.LaxMonoidalFunctor.left_unitality'_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.toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (F.μ (𝟙_ C) X) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom) h))

theorem CategoryTheory.LaxMonoidalFunctor.left_unitality' {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.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (F.μ (𝟙_ C) X) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))

theorem CategoryTheory.LaxMonoidalFunctor.right_unitality'_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.toPrefunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) F.ε) (CategoryTheory.CategoryStruct.comp (F.μ X (𝟙_ C)) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom) h))

theorem CategoryTheory.LaxMonoidalFunctor.right_unitality' {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.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) F.ε) (CategoryTheory.CategoryStruct.comp (F.μ X (𝟙_ C)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_left'_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} (f : X ⟶ Y) (X' : C) {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj Y X') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.toPrefunctor.map f) (F.toPrefunctor.obj X')) (CategoryTheory.CategoryStruct.comp (F.μ Y X') h) = CategoryTheory.CategoryStruct.comp (F.μ X X') (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.whiskerRight f X')) h)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_left' {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} (f : X ⟶ Y) (X' : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.toPrefunctor.map f) (F.toPrefunctor.obj X')) (F.μ Y X') = CategoryTheory.CategoryStruct.comp (F.μ X X') (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_right'_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} (X' : C) (f : X ⟶ Y) {Z : D} (h : F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X' Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X') (F.toPrefunctor.map f)) (CategoryTheory.CategoryStruct.comp (F.μ X' Y) h) = CategoryTheory.CategoryStruct.comp (F.μ X' X) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f)) h)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_right' {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} (X' : C) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X') (F.toPrefunctor.map f)) (F.μ X' Y) = CategoryTheory.CategoryStruct.comp (F.μ X' X) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D ⟶ F.toPrefunctor.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) ⟶ F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) : (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ).ε = ε

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D ⟶ F.toPrefunctor.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) ⟶ F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) (X : C) (Y : C) : (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ).μ X Y = μ X Y

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_toFunctor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D ⟶ F.toPrefunctor.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) ⟶ F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) : ∀ {X Y : C} (a : X ⟶ Y), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ).toFunctor.toPrefunctor.map a = F.toPrefunctor.map a

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_toFunctor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D ⟶ F.toPrefunctor.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) ⟶ F.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) : ∀ (a : C), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ).toFunctor.toPrefunctor.obj a = F.toPrefunctor.obj a

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

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

Equations

• CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ = CategoryTheory.LaxMonoidalFunctor.mk (CategoryTheory.Functor.mk { obj := F.obj, map := fun {X Y : C} => F.toPrefunctor.map }) ε μ

@[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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom F.ε (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp (F.μ (𝟙_ C) X) h)) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.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.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom F.ε (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (F.μ (𝟙_ C) X)) = F.toPrefunctor.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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) F.ε) (CategoryTheory.CategoryStruct.comp (F.μ X (𝟙_ C)) h)) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.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.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) F.ε) (F.μ X (𝟙_ C))) = F.toPrefunctor.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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (F.μ Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z✝).inv) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z✝)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.μ X Y) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z✝))) (CategoryTheory.CategoryStruct.comp (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.toPrefunctor.obj X)) (F.μ Y Z)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.μ X Y) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z))) (F.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z))

@[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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (F.μ (𝟙_ C) X) h)) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.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.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.toPrefunctor.obj X)) (F.μ (𝟙_ C) X)) = F.toPrefunctor.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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) F.ε) (CategoryTheory.CategoryStruct.comp (F.μ X (𝟙_ C)) h)) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.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.toPrefunctor.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) F.ε) (F.μ X (𝟙_ C))) = F.toPrefunctor.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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.toPrefunctor.obj X) (F.μ Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z✝).inv) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z✝)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.μ X Y) (F.toPrefunctor.obj Z✝)) (CategoryTheory.CategoryStruct.comp (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.whiskerLeft (F.toPrefunctor.obj X) (F.μ Y Z)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (F.toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y) (F.toPrefunctor.obj Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.μ X Y) (F.toPrefunctor.obj Z)) (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₂)

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

See .

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

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) : 𝟙_ D ≅ F.toPrefunctor.obj (𝟙_ 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.toPrefunctor.obj X) (F.toPrefunctor.obj Y) ≅ F.toPrefunctor.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 (F.toLaxMonoidalFunctor.μ X Y)

@[simp]

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

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.id_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.LaxMonoidalFunctor.id C).ε = CategoryTheory.CategoryStruct.id (𝟙_ 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

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.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.toLaxMonoidalFunctor.μ X X')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (F.toPrefunctor.map g)) (F.toLaxMonoidalFunctor.μ Y Y'))

theorem CategoryTheory.MonoidalFunctor.map_whiskerLeft {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 : C} (f : Y ⟶ Z) : F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.toLaxMonoidalFunctor.μ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (F.toPrefunctor.map f)) (F.toLaxMonoidalFunctor.μ X Z))

theorem CategoryTheory.MonoidalFunctor.map_whiskerRight {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} (f : X ⟶ Y) (Z : C) : F.toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.toLaxMonoidalFunctor.μ X Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.toPrefunctor.map f) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Z))) (F.toLaxMonoidalFunctor.μ Y Z))

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.toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.toLaxMonoidalFunctor.μ (𝟙_ C) X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv F.ε) (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))) (CategoryTheory.MonoidalCategory.leftUnitor (F.toPrefunctor.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.toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.toLaxMonoidalFunctor.μ X (𝟙_ C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)) (CategoryTheory.inv F.ε)) (CategoryTheory.MonoidalCategory.rightUnitor (F.toPrefunctor.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 : C × C) => CategoryTheory.MonoidalFunctor.μIso F X.1 X.2

@[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 = 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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.μIso F X Y).inv (CategoryTheory.CategoryStruct.comp (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 (F.toLaxMonoidalFunctor.μ X Y) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.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 (F.toLaxMonoidalFunctor.μ X Y) (CategoryTheory.MonoidalFunctor.μIso F X Y).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.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.toPrefunctor.obj (𝟙_ 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.toPrefunctor.obj (𝟙_ 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 (𝟙_ D)

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

@[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 = F.toLaxMonoidalFunctor.μ X✝ X

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.toPrefunctor.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 : C) => 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 = 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.toPrefunctor.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 : C) => CategoryTheory.MonoidalFunctor.μIso F Y X

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

@[simp]

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

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

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_ε {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.toPrefunctor.map F.ε)

@[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) : (F ⊗⋙ G).μ X Y = CategoryTheory.CategoryStruct.comp (G.μ (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) (G.toPrefunctor.map (F.μ X Y))

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

@[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.prod F G).μ X Y = (F.μ X.1 Y.1, G.μ X.2 Y.2)

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.MonoidalFunctor.diag C).toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.diag C).toPrefunctor.obj X) ((CategoryTheory.Functor.diag C).toPrefunctor.obj Y))

@[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 (𝟙_ (C × C))

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

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.prod' F G).μ X Y = (F.μ X Y, 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 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

• CategoryTheory.MonoidalFunctor.prod F G = let src := CategoryTheory.LaxMonoidalFunctor.prod F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor; CategoryTheory.MonoidalFunctor.mk src

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

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)