(Lax) monoidal functors

A lax monoidal functor F between monoidal categories C and D is a functor between the underlying categories equipped with morphisms

• ε : 𝟙_ D ⟶ F.obj (𝟙_ C) (called the unit morphism)
• μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y) (called the tensorator, or strength). satisfying various axioms. This is implemented as a typeclass F.LaxMonoidal.

Similarly, we define the typeclass F.OplaxMonoidal. For these oplax monoidal functors, we have similar data η and δ, but with morphisms in the opposite direction.

A monoidal functor (F.Monoidal) is defined here as the combination of F.LaxMonoidal and F.OplaxMonoidal, with the additional conditions that ε/η and μ/δ are inverse isomorphisms.

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

See Mathlib.CategoryTheory.Monoidal.NaturalTransformation for monoidal natural transformations.

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

References

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

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

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

• ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)

  unit morphism

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

  tensorator

• μ'_natural_left {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ' Y X')) (CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.whiskerRight f X')))
• μ'_natural_right {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ' X' Y)) (CategoryStruct.comp (μ' X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f)))
• associativity' (X Y Z : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ' X Y) (F.obj Z)) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z))))

  associativity of the tensorator

• left_unitality' (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ε' (F.obj X)) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)))
• right_unitality' (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)))

def CategoryTheory.Functor.LaxMonoidal.ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)

the unit morphism of a lax monoidal functor

Equations

• Eq (CategoryTheory.Functor.LaxMonoidal.ε F) CategoryTheory.Functor.LaxMonoidal.ε'

def CategoryTheory.Functor.LaxMonoidal.μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y : C) : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))

the tensorator of a lax monoidal functor

Equations

• Eq (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (CategoryTheory.Functor.LaxMonoidal.μ' X Y)

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_left {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ F Y X')) (CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.whiskerRight f X')))

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y : C} (f : Quiver.Hom X Y) (X' : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj Y X')) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryStruct.comp (μ F Y X') h)) (CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h))

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_right {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ F X' Y)) (CategoryStruct.comp (μ F X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f)))

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y : C} (X' : C) (f : Quiver.Hom X Y) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X' Y)) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryStruct.comp (μ F X' Y) h)) (CategoryStruct.comp (μ F X' X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h))

theorem CategoryTheory.Functor.LaxMonoidal.associativity {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (μ F X (MonoidalCategoryStruct.tensorObj Y Z))))

theorem CategoryTheory.Functor.LaxMonoidal.associativity_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z))) Z✝) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h)))

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)))

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F MonoidalCategoryStruct.tensorUnit X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h)))

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)))

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h)))

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y') : Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ F Y Y')) (CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.tensorHom f g)))

theorem CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y') {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj Y Y')) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (μ F Y Y') h)) (CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h))

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (μ F MonoidalCategoryStruct.tensorUnit X))) (F.map (MonoidalCategoryStruct.leftUnitor X).inv)

theorem CategoryTheory.Functor.LaxMonoidal.left_unitality_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj MonoidalCategoryStruct.tensorUnit X)) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F MonoidalCategoryStruct.tensorUnit X) h))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h)

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (μ F X MonoidalCategoryStruct.tensorUnit))) (F.map (MonoidalCategoryStruct.rightUnitor X).inv)

theorem CategoryTheory.Functor.LaxMonoidal.right_unitality_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X MonoidalCategoryStruct.tensorUnit)) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X MonoidalCategoryStruct.tensorUnit) h))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h)

theorem CategoryTheory.Functor.LaxMonoidal.associativity_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) (F.map (MonoidalCategoryStruct.associator X Y Z).inv))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (μ F (MonoidalCategoryStruct.tensorObj X Y) Z)))

theorem CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z)) Z✝) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h)))

def CategoryTheory.Functor.LaxMonoidal.ofTensorHom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)) (μ' : (X Y : C) → Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))) (μ'_natural : ∀ {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y'), Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ' Y Y')) (CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.tensorHom f g))) := by aesop_cat) (associativity' : ∀ (X Y Z : C), Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ' X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z)))) := by aesop_cat) (left_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))) := by aesop_cat) (right_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))) := by aesop_cat) : F.LaxMonoidal

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

Equations

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

theorem CategoryTheory.Functor.LaxMonoidal.ofTensorHom_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)) (μ' : (X Y : C) → Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))) (μ'_natural : ∀ {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y'), Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ' Y Y')) (CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.tensorHom f g))) := by aesop_cat) (associativity' : ∀ (X Y Z : C), Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ' X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z)))) := by aesop_cat) (left_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))) := by aesop_cat) (right_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))) := by aesop_cat) : Eq (ε F) ε'

theorem CategoryTheory.Functor.LaxMonoidal.ofTensorHom_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)) (μ' : (X Y : C) → Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))) (μ'_natural : ∀ {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y'), Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ' Y Y')) (CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.tensorHom f g))) := by aesop_cat) (associativity' : ∀ (X Y Z : C), Eq (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ' X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z)))) := by aesop_cat) (left_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))) := by aesop_cat) (right_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))) := by aesop_cat) : Eq (μ F) μ'

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

Equations

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

theorem CategoryTheory.Functor.LaxMonoidal.id_ε {C : Type u₁} [Category C] [MonoidalCategory C] : Eq (ε (Functor.id C)) (CategoryStruct.id MonoidalCategoryStruct.tensorUnit)

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

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

Equations

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

theorem CategoryTheory.Functor.LaxMonoidal.comp_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] : Eq (ε (F.comp G)) (CategoryStruct.comp (ε G) (G.map (ε F)))

theorem CategoryTheory.Functor.LaxMonoidal.comp_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) : Eq (μ (F.comp G) X Y) (CategoryStruct.comp (μ G (F.obj X) (F.obj Y)) (G.map (μ F X Y)))

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

A functor F : C ⥤ D between monoidal categories is oplax monoidal if it is equipped with morphisms η : F.obj (𝟙_ C) ⟶ 𝟙 _D and δ X Y : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y, satisfying the appropriate coherences.

• η' : Quiver.Hom (F.obj MonoidalCategoryStruct.tensorUnit) MonoidalCategoryStruct.tensorUnit

  counit morphism

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

  cotensorator

• δ'_natural_left {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (δ' X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ' Y X'))
• δ'_natural_right {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (δ' X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ' X' Y))
• oplax_associativity' (X Y Z : C) : Eq (CategoryStruct.comp (δ' (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ' X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ' X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ' Y Z))))

  associativity of the tensorator

• oplax_left_unitality' (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ' MonoidalCategoryStruct.tensorUnit X) (MonoidalCategoryStruct.whiskerRight η' (F.obj X))))
• oplax_right_unitality' (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ' X MonoidalCategoryStruct.tensorUnit) (MonoidalCategoryStruct.whiskerLeft (F.obj X) η')))

def CategoryTheory.Functor.OplaxMonoidal.η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] : Quiver.Hom (F.obj MonoidalCategoryStruct.tensorUnit) MonoidalCategoryStruct.tensorUnit

the counit morphism of a lax monoidal functor

Equations

• Eq (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.Functor.OplaxMonoidal.η'

def CategoryTheory.Functor.OplaxMonoidal.δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X Y)) (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))

the cotensorator of an oplax monoidal functor

Equations

• Eq (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (CategoryTheory.Functor.OplaxMonoidal.δ' X Y)

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_left {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ F Y X'))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y : C} (f : Quiver.Hom X Y) (X' : C) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj X')) Z) : Eq (CategoryStruct.comp (δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) h)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (CategoryStruct.comp (δ F Y X') h))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_right {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (δ F X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ F X' Y))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y : C} (X' : C) (f : Quiver.Hom X Y) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X') (F.obj Y)) Z) : Eq (CategoryStruct.comp (δ F X' X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) h)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (CategoryStruct.comp (δ F X' Y) h))

theorem CategoryTheory.Functor.OplaxMonoidal.associativity {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) : Eq (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z))))

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z))) Z✝) : Eq (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) h)))

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F MonoidalCategoryStruct.tensorUnit X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X))))

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj MonoidalCategoryStruct.tensorUnit (F.obj X)) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv h) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F MonoidalCategoryStruct.tensorUnit X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) h)))

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X MonoidalCategoryStruct.tensorUnit) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F))))

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv h) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) h)))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y') : Eq (CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (δ F Y Y'))

theorem CategoryTheory.Functor.OplaxMonoidal.δ_natural_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y') {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Y')) Z) : Eq (CategoryStruct.comp (δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (δ F Y Y') h))

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : Eq (CategoryStruct.comp (δ F MonoidalCategoryStruct.tensorUnit X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom)) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)

theorem CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (δ F MonoidalCategoryStruct.tensorUnit X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h)

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) : Eq (CategoryStruct.comp (δ F X MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)

theorem CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (δ F X MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h)

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) : Eq (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z))))

theorem CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z)) Z✝) : Eq (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) h)))

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

Equations

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

theorem CategoryTheory.Functor.OplaxMonoidal.id_η {C : Type u₁} [Category C] [MonoidalCategory C] : Eq (η (Functor.id C)) (CategoryStruct.id ((Functor.id C).obj MonoidalCategoryStruct.tensorUnit))

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

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

Equations

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

theorem CategoryTheory.Functor.OplaxMonoidal.comp_η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] : Eq (η (F.comp G)) (CategoryStruct.comp (G.map (η F)) (η G))

theorem CategoryTheory.Functor.OplaxMonoidal.comp_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) : Eq (δ (F.comp G) X Y) (CategoryStruct.comp (G.map (δ F X Y)) (δ G (F.obj X) (F.obj Y)))

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

A functor between monoidal categories is monoidal if it is lax and oplax monoidals, and both data give inverse isomorphisms.

• ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)
• μ' (X Y : C) : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))
• μ'_natural_left {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ' Y X')) (CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.whiskerRight f X')))
• μ'_natural_right {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ' X' Y)) (CategoryStruct.comp (μ' X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f)))
• associativity' (X Y Z : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ' X Y) (F.obj Z)) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z))))
• left_unitality' (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ε' (F.obj X)) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)))
• right_unitality' (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)))
• η' : Quiver.Hom (F.obj MonoidalCategoryStruct.tensorUnit) MonoidalCategoryStruct.tensorUnit
• δ' (X Y : C) : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X Y)) (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))
• δ'_natural_left {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (δ' X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ' Y X'))
• δ'_natural_right {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (δ' X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ' X' Y))
• oplax_associativity' (X Y Z : C) : Eq (CategoryStruct.comp (δ' (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ' X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ' X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ' Y Z))))
• oplax_left_unitality' (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ' MonoidalCategoryStruct.tensorUnit X) (MonoidalCategoryStruct.whiskerRight η' (F.obj X))))
• oplax_right_unitality' (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ' X MonoidalCategoryStruct.tensorUnit) (MonoidalCategoryStruct.whiskerLeft (F.obj X) η')))
• ε_η : Eq (CategoryStruct.comp (LaxMonoidal.ε F) (OplaxMonoidal.η F)) (CategoryStruct.id MonoidalCategoryStruct.tensorUnit)
• η_ε : Eq (CategoryStruct.comp (OplaxMonoidal.η F) (LaxMonoidal.ε F)) (CategoryStruct.id (F.obj MonoidalCategoryStruct.tensorUnit))
• μ_δ (X Y : C) : Eq (CategoryStruct.comp (LaxMonoidal.μ F X Y) (OplaxMonoidal.δ F X Y)) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))
• δ_μ (X Y : C) : Eq (CategoryStruct.comp (OplaxMonoidal.δ F X Y) (LaxMonoidal.μ F X Y)) (CategoryStruct.id (F.obj (MonoidalCategoryStruct.tensorObj X Y)))

theorem CategoryTheory.Functor.Monoidal.ε_η_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] {Z : D} (h : Quiver.Hom MonoidalCategoryStruct.tensorUnit Z) : Eq (CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (OplaxMonoidal.η F) h)) h

theorem CategoryTheory.Functor.Monoidal.μ_δ_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] (X Y : C) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z) : Eq (CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (OplaxMonoidal.δ F X Y) h)) h

theorem CategoryTheory.Functor.Monoidal.η_ε_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] {Z : D} (h : Quiver.Hom (F.obj MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (OplaxMonoidal.η F) (CategoryStruct.comp (LaxMonoidal.ε F) h)) h

theorem CategoryTheory.Functor.Monoidal.δ_μ_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] (X Y : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X Y)) Z) : Eq (CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (LaxMonoidal.μ F X Y) h)) h

def CategoryTheory.Functor.Monoidal.εIso {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : Iso MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)

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

Equations

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

theorem CategoryTheory.Functor.Monoidal.εIso_hom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : Eq (εIso F).hom (LaxMonoidal.ε F)

theorem CategoryTheory.Functor.Monoidal.εIso_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : Eq (εIso F).inv (OplaxMonoidal.η F)

def CategoryTheory.Functor.Monoidal.μIso {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : Iso (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))

The isomorphism F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y) when F is a monoidal functor.

Equations

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

theorem CategoryTheory.Functor.Monoidal.μIso_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : Eq (μIso F X Y).inv (OplaxMonoidal.δ F X Y)

theorem CategoryTheory.Functor.Monoidal.μIso_hom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : Eq (μIso F X Y).hom (LaxMonoidal.μ F X Y)

theorem CategoryTheory.Functor.Monoidal.instIsIsoε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : IsIso (LaxMonoidal.ε F)

theorem CategoryTheory.Functor.Monoidal.instIsIsoη {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : IsIso (OplaxMonoidal.η F)

theorem CategoryTheory.Functor.Monoidal.instIsIsoμ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : IsIso (LaxMonoidal.μ F X Y)

theorem CategoryTheory.Functor.Monoidal.instIsIsoδ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : IsIso (OplaxMonoidal.δ F X Y)

theorem CategoryTheory.Functor.Monoidal.map_ε_η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') : Eq (CategoryStruct.comp (G.map (LaxMonoidal.ε F)) (G.map (OplaxMonoidal.η F))) (CategoryStruct.id (G.obj MonoidalCategoryStruct.tensorUnit))

theorem CategoryTheory.Functor.Monoidal.map_ε_η_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') {Z : C'} (h : Quiver.Hom (G.obj MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (G.map (LaxMonoidal.ε F)) (CategoryStruct.comp (G.map (OplaxMonoidal.η F)) h)) h

theorem CategoryTheory.Functor.Monoidal.map_η_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') : Eq (CategoryStruct.comp (G.map (OplaxMonoidal.η F)) (G.map (LaxMonoidal.ε F))) (CategoryStruct.id (G.obj (F.obj MonoidalCategoryStruct.tensorUnit)))

theorem CategoryTheory.Functor.Monoidal.map_η_ε_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') {Z : C'} (h : Quiver.Hom (G.obj (F.obj MonoidalCategoryStruct.tensorUnit)) Z) : Eq (CategoryStruct.comp (G.map (OplaxMonoidal.η F)) (CategoryStruct.comp (G.map (LaxMonoidal.ε F)) h)) h

theorem CategoryTheory.Functor.Monoidal.map_μ_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) : Eq (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) (G.map (OplaxMonoidal.δ F X Y))) (CategoryStruct.id (G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))))

theorem CategoryTheory.Functor.Monoidal.map_μ_δ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) {Z : C'} (h : Quiver.Hom (G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))) Z) : Eq (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) (CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) h)) h

theorem CategoryTheory.Functor.Monoidal.map_δ_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) : Eq (CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) (G.map (LaxMonoidal.μ F X Y))) (CategoryStruct.id (G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y))))

theorem CategoryTheory.Functor.Monoidal.map_δ_μ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) {Z : C'} (h : Quiver.Hom (G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y))) Z) : Eq (CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerRight_ε_η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T)) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj MonoidalCategoryStruct.tensorUnit T))

theorem CategoryTheory.Functor.Monoidal.whiskerRight_ε_η_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj MonoidalCategoryStruct.tensorUnit T) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerRight_η_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T)) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj MonoidalCategoryStruct.tensorUnit) T))

theorem CategoryTheory.Functor.Monoidal.whiskerRight_η_ε_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj MonoidalCategoryStruct.tensorUnit) T) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) T) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T)) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T))

theorem CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T)) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) T))

theorem CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) T) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F))) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj T MonoidalCategoryStruct.tensorUnit))

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj T MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F))) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (F.obj MonoidalCategoryStruct.tensorUnit)))

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj T (F.obj MonoidalCategoryStruct.tensorUnit)) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.η F)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.ε F)) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y))) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))))

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) h)) h

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y))) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorObj X Y))))

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) (T : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorObj X Y))) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) h)) h

theorem CategoryTheory.Functor.Monoidal.map_tensor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y') : Eq (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (OplaxMonoidal.δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (LaxMonoidal.μ F Y Y')))

theorem CategoryTheory.Functor.Monoidal.map_tensor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y') {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj Y Y')) Z) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h) (CategoryStruct.comp (OplaxMonoidal.δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (LaxMonoidal.μ F Y Y') h)))

theorem CategoryTheory.Functor.Monoidal.map_whiskerLeft {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Y Z : C} (f : Quiver.Hom Y Z) : Eq (F.map (MonoidalCategoryStruct.whiskerLeft X f)) (CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (LaxMonoidal.μ F X Z)))

theorem CategoryTheory.Functor.Monoidal.map_whiskerLeft_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Y Z : C} (f : Quiver.Hom Y Z) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X Z)) Z✝) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X f)) h) (CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (CategoryStruct.comp (LaxMonoidal.μ F X Z) h)))

theorem CategoryTheory.Functor.Monoidal.map_whiskerRight {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y : C} (f : Quiver.Hom X Y) (Z : C) : Eq (F.map (MonoidalCategoryStruct.whiskerRight f Z)) (CategoryStruct.comp (OplaxMonoidal.δ F X Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z)) (LaxMonoidal.μ F Y Z)))

theorem CategoryTheory.Functor.Monoidal.map_whiskerRight_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] {X Y : C} (f : Quiver.Hom X Y) (Z : C) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj Y Z)) Z✝) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f Z)) h) (CategoryStruct.comp (OplaxMonoidal.δ F X Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z)) (CategoryStruct.comp (LaxMonoidal.μ F Y Z) h)))

theorem CategoryTheory.Functor.Monoidal.map_associator {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) : Eq (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z)) (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z))))))

theorem CategoryTheory.Functor.Monoidal.map_associator_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z))) Z✝) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h) (CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z)) (CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h)))))

theorem CategoryTheory.Functor.Monoidal.map_associator_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) : Eq (F.map (MonoidalCategoryStruct.associator X Y Z).inv) (CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z)) (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z)))))

theorem CategoryTheory.Functor.Monoidal.map_associator_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z)) Z✝) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h) (CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z)) (CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h)))))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : Eq (F.map (MonoidalCategoryStruct.leftUnitor X).hom) (CategoryStruct.comp (OplaxMonoidal.δ F MonoidalCategoryStruct.tensorUnit X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) (F.obj X)) (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h) (CategoryStruct.comp (OplaxMonoidal.δ F MonoidalCategoryStruct.tensorUnit X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) (F.obj X)) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h)))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : Eq (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) (F.obj X)) (LaxMonoidal.μ F MonoidalCategoryStruct.tensorUnit X)))

theorem CategoryTheory.Functor.Monoidal.map_leftUnitor_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj MonoidalCategoryStruct.tensorUnit X)) Z) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) (F.obj X)) (CategoryStruct.comp (LaxMonoidal.μ F MonoidalCategoryStruct.tensorUnit X) h)))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : Eq (F.map (MonoidalCategoryStruct.rightUnitor X).hom) (CategoryStruct.comp (OplaxMonoidal.δ F X MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.η F)) (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h) (CategoryStruct.comp (OplaxMonoidal.δ F X MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.η F)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h)))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : Eq (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.ε F)) (LaxMonoidal.μ F X MonoidalCategoryStruct.tensorUnit)))

theorem CategoryTheory.Functor.Monoidal.map_rightUnitor_inv_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X MonoidalCategoryStruct.tensorUnit)) Z) : Eq (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.ε F)) (CategoryStruct.comp (LaxMonoidal.μ F X MonoidalCategoryStruct.tensorUnit) h)))

noncomputable def CategoryTheory.Functor.Monoidal.μNatIso {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] : Iso ((F.prod F).comp (MonoidalCategory.tensor D)) ((MonoidalCategory.tensor C).comp F)

The tensorator as a natural isomorphism.

Equations

• Eq (CategoryTheory.Functor.Monoidal.μNatIso F) (CategoryTheory.NatIso.ofComponents (fun (x : Prod C C) => CategoryTheory.Functor.Monoidal.μIso F x.fst x.snd) ⋯)

theorem CategoryTheory.Functor.Monoidal.μNatIso_hom_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : Prod C C) : Eq ((μNatIso F).hom.app X) (LaxMonoidal.μ F X.fst X.snd)

theorem CategoryTheory.Functor.Monoidal.μNatIso_inv_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : Prod C C) : Eq ((μNatIso F).inv.app X) (OplaxMonoidal.δ F X.fst X.snd)

noncomputable def CategoryTheory.Functor.Monoidal.commTensorLeft {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : Iso (F.comp (MonoidalCategory.tensorLeft (F.obj X))) ((MonoidalCategory.tensorLeft X).comp F)

Monoidal functors commute with left tensoring up to isomorphism

Equations

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

theorem CategoryTheory.Functor.Monoidal.commTensorLeft_hom_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : Eq ((commTensorLeft F X).hom.app X✝) (LaxMonoidal.μ F X X✝)

theorem CategoryTheory.Functor.Monoidal.commTensorLeft_inv_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : Eq ((commTensorLeft F X).inv.app X✝) (OplaxMonoidal.δ F X X✝)

noncomputable def CategoryTheory.Functor.Monoidal.commTensorRight {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : Iso (F.comp (MonoidalCategory.tensorRight (F.obj X))) ((MonoidalCategory.tensorRight X).comp F)

Monoidal functors commute with right tensoring up to isomorphism

Equations

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

theorem CategoryTheory.Functor.Monoidal.commTensorRight_inv_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : Eq ((commTensorRight F X).inv.app X✝) (OplaxMonoidal.δ F X✝ X)

theorem CategoryTheory.Functor.Monoidal.commTensorRight_hom_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X X✝ : C) : Eq ((commTensorRight F X).hom.app X✝) (LaxMonoidal.μ F X✝ X)

def CategoryTheory.Functor.Monoidal.instId {C : Type u₁} [Category C] [MonoidalCategory C] : (Functor.id C).Monoidal

Equations

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

def CategoryTheory.Functor.Monoidal.instComp {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] : (F.comp G).Monoidal

Equations

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

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

Structure which is a helper in order to show that a functor is monoidal. It consists of isomorphisms εIso and μIso such that the morphisms .hom induced by these isomorphisms satisfy the axioms of lax monoidal functors.

• εIso : Iso MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)

  unit morphism

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

  tensorator

• μIso_hom_natural_left {X Y : C} (f : Quiver.Hom X Y) (X' : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (self.μIso Y X').hom) (CategoryStruct.comp (self.μIso X X').hom (F.map (MonoidalCategoryStruct.whiskerRight f X')))
• μIso_hom_natural_right {X Y : C} (X' : C) (f : Quiver.Hom X Y) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (self.μIso X' Y).hom) (CategoryStruct.comp (self.μIso X' X).hom (F.map (MonoidalCategoryStruct.whiskerLeft X' f)))
• associativity (X Y Z : C) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).hom (F.map (MonoidalCategoryStruct.associator X Y Z).hom))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom) (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z)).hom))

  associativity of the tensorator

• left_unitality (X : C) : Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X)) (CategoryStruct.comp (self.μIso MonoidalCategoryStruct.tensorUnit X).hom (F.map (MonoidalCategoryStruct.leftUnitor X).hom)))
• right_unitality (X : C) : Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom) (CategoryStruct.comp (self.μIso X MonoidalCategoryStruct.tensorUnit).hom (F.map (MonoidalCategoryStruct.rightUnitor X).hom)))

theorem CategoryTheory.Functor.CoreMonoidal.associativity_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) (X Y Z : C) {Z✝ : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z))) Z✝) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h))) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom) (CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z)).hom h)))

theorem CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) {X Y : C} (f : Quiver.Hom X Y) (X' : C) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj Y X')) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryStruct.comp (self.μIso Y X').hom h)) (CategoryStruct.comp (self.μIso X X').hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h))

theorem CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) {X Y : C} (X' : C) (f : Quiver.Hom X Y) {Z : D} (h : Quiver.Hom (F.obj (MonoidalCategoryStruct.tensorObj X' Y)) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryStruct.comp (self.μIso X' Y).hom h)) (CategoryStruct.comp (self.μIso X' X).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h))

theorem CategoryTheory.Functor.CoreMonoidal.left_unitality_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X)) (CategoryStruct.comp (self.μIso MonoidalCategoryStruct.tensorUnit X).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h)))

theorem CategoryTheory.Functor.CoreMonoidal.right_unitality_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (self : F.CoreMonoidal) (X : C) {Z : D} (h : Quiver.Hom (F.obj X) Z) : Eq (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom) (CategoryStruct.comp (self.μIso X MonoidalCategoryStruct.tensorUnit).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h)))

def CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : F.LaxMonoidal

The lax monoidal functor structure induced by a Functor.CoreMonoidal structure.

Equations

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

theorem CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : Eq (LaxMonoidal.ε F) h.εIso.hom

theorem CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) (X Y : C) : Eq (LaxMonoidal.μ F X Y) (h.μIso X Y).hom

def CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : F.OplaxMonoidal

The oplax monoidal functor structure induced by a Functor.CoreMonoidal structure.

Equations

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

theorem CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : Eq (OplaxMonoidal.η F) h.εIso.inv

theorem CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) (X Y : C) : Eq (OplaxMonoidal.δ F X Y) (h.μIso X Y).inv

def CategoryTheory.Functor.CoreMonoidal.toMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : F.Monoidal

The monoidal functor structure induced by a Functor.CoreMonoidal structure.

Equations

• Eq h.toMonoidal { toLaxMonoidal := h.toLaxMonoidal, toOplaxMonoidal := h.toOplaxMonoidal, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }

theorem CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : Eq Monoidal.toLaxMonoidal h.toLaxMonoidal

theorem CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (h : F.CoreMonoidal) : Eq Monoidal.toOplaxMonoidal h.toOplaxMonoidal

noncomputable def CategoryTheory.Functor.CoreMonoidal.ofLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] [IsIso (LaxMonoidal.ε F)] [∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)] : F.CoreMonoidal

The Functor.CoreMonoidal structure given by a lax monoidal functor such that ε and μ are isomorphisms.

Equations

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

noncomputable def CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] : F.CoreMonoidal

The Functor.CoreMonoidal structure given by an oplax monoidal functor such that η and δ are isomorphisms.

Equations

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

noncomputable def CategoryTheory.Functor.Monoidal.ofLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] [IsIso (LaxMonoidal.ε F)] [∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)] : F.Monoidal

The Functor.Monoidal structure given by a lax monoidal functor such that ε and μ are isomorphisms.

Equations

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

noncomputable def CategoryTheory.Functor.Monoidal.ofOplaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] : F.Monoidal

The Functor.Monoidal structure given by an oplax monoidal functor such that η and δ are isomorphisms.

Equations

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

def CategoryTheory.Functor.instLaxMonoidalProdProd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] : (F.prod G).LaxMonoidal

Equations

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

theorem CategoryTheory.Functor.prod_ε_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] : Eq (LaxMonoidal.ε (F.prod G)).fst (LaxMonoidal.ε F)

theorem CategoryTheory.Functor.prod_ε_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] : Eq (LaxMonoidal.ε (F.prod G)).snd (LaxMonoidal.ε G)

theorem CategoryTheory.Functor.prod_μ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] (X Y : Prod C E) : Eq (LaxMonoidal.μ (F.prod G) X Y).fst (LaxMonoidal.μ F X.fst Y.fst)

theorem CategoryTheory.Functor.prod_μ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] (X Y : Prod C E) : Eq (LaxMonoidal.μ (F.prod G) X Y).snd (LaxMonoidal.μ G X.snd Y.snd)

def CategoryTheory.Functor.instOplaxMonoidalProdProd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] : (F.prod G).OplaxMonoidal

Equations

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

theorem CategoryTheory.Functor.prod_η_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] : Eq (OplaxMonoidal.η (F.prod G)).fst (OplaxMonoidal.η F)

theorem CategoryTheory.Functor.prod_η_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] : Eq (OplaxMonoidal.η (F.prod G)).snd (OplaxMonoidal.η G)

theorem CategoryTheory.Functor.prod_δ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : Prod C E) : Eq (OplaxMonoidal.δ (F.prod G) X Y).fst (OplaxMonoidal.δ F X.fst Y.fst)

theorem CategoryTheory.Functor.prod_δ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : Prod C E) : Eq (OplaxMonoidal.δ (F.prod G) X Y).snd (OplaxMonoidal.δ G X.snd Y.snd)

def CategoryTheory.Functor.instMonoidalProdProd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.Monoidal] [G.Monoidal] : (F.prod G).Monoidal

Equations

• Eq (F.instMonoidalProdProd G) { toLaxMonoidal := F.instLaxMonoidalProdProd G, toOplaxMonoidal := F.instOplaxMonoidalProdProd G, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }

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

Equations

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

theorem CategoryTheory.Functor.diag_ε {C : Type u₁} [Category C] [MonoidalCategory C] : Eq (LaxMonoidal.ε (diag C)) (CategoryStruct.id MonoidalCategoryStruct.tensorUnit)

theorem CategoryTheory.Functor.diag_η {C : Type u₁} [Category C] [MonoidalCategory C] : Eq (OplaxMonoidal.η (diag C)) (CategoryStruct.id ((diag C).obj MonoidalCategoryStruct.tensorUnit))

theorem CategoryTheory.Functor.diag_μ {C : Type u₁} [Category C] [MonoidalCategory C] (X Y : C) : Eq (LaxMonoidal.μ (diag C) X Y) (CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((diag C).obj X) ((diag C).obj Y)))

theorem CategoryTheory.Functor.diag_δ {C : Type u₁} [Category C] [MonoidalCategory C] (X Y : C) : Eq (OplaxMonoidal.δ (diag C) X Y) (CategoryStruct.id ((diag C).obj (MonoidalCategoryStruct.tensorObj X Y)))

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

The functor C ⥤ D × E obtained from two lax monoidal functors is lax monoidal.

Equations

• Eq (CategoryTheory.Functor.LaxMonoidal.prod' F G) (inferInstanceAs ((CategoryTheory.Functor.diag C).comp (F.prod G)).LaxMonoidal)

theorem CategoryTheory.Functor.prod'_ε_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] : Eq (LaxMonoidal.ε (F.prod' G)).fst (LaxMonoidal.ε F)

theorem CategoryTheory.Functor.prod'_ε_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] : Eq (LaxMonoidal.ε (F.prod' G)).snd (LaxMonoidal.ε G)

theorem CategoryTheory.Functor.prod'_μ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) : Eq (LaxMonoidal.μ (F.prod' G) X Y).fst (LaxMonoidal.μ F X Y)

theorem CategoryTheory.Functor.prod'_μ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) : Eq (LaxMonoidal.μ (F.prod' G) X Y).snd (LaxMonoidal.μ G X Y)

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

The functor C ⥤ D × E obtained from two oplax monoidal functors is oplax monoidal.

Equations

• Eq (CategoryTheory.Functor.OplaxMonoidal.prod' F G) (inferInstanceAs ((CategoryTheory.Functor.diag C).comp (F.prod G)).OplaxMonoidal)

theorem CategoryTheory.Functor.prod'_η_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] : Eq (OplaxMonoidal.η (F.prod' G)).fst (OplaxMonoidal.η F)

theorem CategoryTheory.Functor.prod'_η_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] : Eq (OplaxMonoidal.η (F.prod' G)).snd (OplaxMonoidal.η G)

theorem CategoryTheory.Functor.prod'_δ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) : Eq (OplaxMonoidal.δ (F.prod' G) X Y).fst (OplaxMonoidal.δ F X Y)

theorem CategoryTheory.Functor.prod'_δ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) : Eq (OplaxMonoidal.δ (F.prod' G) X Y).snd (OplaxMonoidal.δ G X Y)

theorem CategoryTheory.Functor.prod_comp_fst {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) : Eq (CategoryStruct.comp f g).fst (CategoryStruct.comp f.fst g.fst)

theorem CategoryTheory.Functor.prod_comp_fst_assoc {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) {Z✝ : C} (h : Quiver.Hom Z.fst Z✝) : Eq (CategoryStruct.comp (CategoryStruct.comp f g).fst h) (CategoryStruct.comp f.fst (CategoryStruct.comp g.fst h))

theorem CategoryTheory.Functor.prod_comp_snd {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) : Eq (CategoryStruct.comp f g).snd (CategoryStruct.comp f.snd g.snd)

theorem CategoryTheory.Functor.prod_comp_snd_assoc {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) {Z✝ : D} (h : Quiver.Hom Z.snd Z✝) : Eq (CategoryStruct.comp (CategoryStruct.comp f g).snd h) (CategoryStruct.comp f.snd (CategoryStruct.comp g.snd h))

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

The functor C ⥤ D × E obtained from two monoidal functors is monoidal.

Equations

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

def CategoryTheory.Adjunction.rightAdjointLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] : G.LaxMonoidal

The right adjoint of an oplax monoidal functor is lax monoidal.

Equations

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

theorem CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] : Eq (Functor.LaxMonoidal.ε G) (DFunLike.coe (adj.homEquiv MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.tensorUnit) (Functor.OplaxMonoidal.η F))

theorem CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] (X Y : D) : Eq (Functor.LaxMonoidal.μ G X Y) (DFunLike.coe (adj.homEquiv (MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorObj ((Functor.id D).obj X) ((Functor.id D).obj Y))) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))))

structure CategoryTheory.Adjunction.IsMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] : Prop

When adj : F ⊣ G is an adjunction, with F oplax monoidal and G monoidal, this typeclass expresses compatibilities between the adjunction and the (op)lax monoidal structures.

• leftAdjoint_ε : Eq (Functor.LaxMonoidal.ε G) (DFunLike.coe (adj.homEquiv MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.tensorUnit) (Functor.OplaxMonoidal.η F))
• leftAdjoint_μ (X Y : D) : Eq (Functor.LaxMonoidal.μ G X Y) (DFunLike.coe (adj.homEquiv (MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorObj ((Functor.id D).obj X) ((Functor.id D).obj Y))) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))))

theorem CategoryTheory.Adjunction.instIsMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] : adj.IsMonoidal

theorem CategoryTheory.Adjunction.unit_app_unit_comp_map_η {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] : Eq (CategoryStruct.comp (adj.unit.app MonoidalCategoryStruct.tensorUnit) (G.map (Functor.OplaxMonoidal.η F))) (Functor.LaxMonoidal.ε G)

theorem CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {Z : C} (h : Quiver.Hom (G.obj MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (adj.unit.app MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (G.map (Functor.OplaxMonoidal.η F)) h)) (CategoryStruct.comp (Functor.LaxMonoidal.ε G) h)

theorem CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : C) : Eq (CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (G.map (Functor.OplaxMonoidal.δ F X Y))) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y)) (Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)))

theorem CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : C) {Z : C} (h : Quiver.Hom (G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))) Z) : Eq (CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (G.map (Functor.OplaxMonoidal.δ F X Y)) h)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)) h))

theorem CategoryTheory.Adjunction.map_ε_comp_counit_app_unit {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] : Eq (CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G)) (adj.counit.app MonoidalCategoryStruct.tensorUnit)) (Functor.OplaxMonoidal.η F)

theorem CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {Z : D} (h : Quiver.Hom MonoidalCategoryStruct.tensorUnit Z) : Eq (CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G)) (CategoryStruct.comp (adj.counit.app MonoidalCategoryStruct.tensorUnit) h)) (CategoryStruct.comp (Functor.OplaxMonoidal.η F) h)

theorem CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : D) : Eq (CategoryStruct.comp (F.map (Functor.LaxMonoidal.μ G X Y)) (adj.counit.app (MonoidalCategoryStruct.tensorObj X Y))) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)))

theorem CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] (X Y : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj X Y) Z) : Eq (CategoryStruct.comp (F.map (Functor.LaxMonoidal.μ G X Y)) (CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorObj X Y)) h)) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)) h))

theorem CategoryTheory.Adjunction.instIsMonoidalId {C : Type u₁} [Category C] [MonoidalCategory C] : id.IsMonoidal

theorem CategoryTheory.Adjunction.isMonoidal_comp {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {F' : Functor D E} {G' : Functor E D} (adj' : Adjunction F' G') [F'.OplaxMonoidal] [G'.LaxMonoidal] [adj'.IsMonoidal] : (adj.comp adj').IsMonoidal

def CategoryTheory.Equivalence.instMonoidalFunctorSymmOfInverse {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.inverse.Monoidal] : e.symm.functor.Monoidal

Equations

• Eq e.instMonoidalFunctorSymmOfInverse (inferInstanceAs e.inverse.Monoidal)

def CategoryTheory.Equivalence.instMonoidalInverseSymmOfFunctor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] : e.symm.inverse.Monoidal

Equations

• Eq e.instMonoidalInverseSymmOfFunctor (inferInstanceAs e.functor.Monoidal)

noncomputable def CategoryTheory.Equivalence.inverseMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] : e.inverse.Monoidal

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

Equations

• Eq e.inverseMonoidal (CategoryTheory.Functor.Monoidal.ofLaxMonoidal e.inverse)

@[reducible, inline]

abbrev CategoryTheory.Equivalence.IsMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] : Prop

An equivalence of categories involving monoidal functors is monoidal if the underlying adjunction satisfies certain compatibilities with respect to the monoidal functor data.

Equations

• Eq e.IsMonoidal e.toAdjunction.IsMonoidal

theorem CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : Eq (CategoryStruct.comp (e.unitIso.hom.app MonoidalCategoryStruct.tensorUnit) (e.inverse.map (Functor.OplaxMonoidal.η e.functor))) (Functor.LaxMonoidal.ε e.inverse)

theorem CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : C} (h : Quiver.Hom (e.inverse.obj MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (e.unitIso.hom.app MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.η e.functor)) h)) (CategoryStruct.comp (Functor.LaxMonoidal.ε e.inverse) h)

theorem CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) : Eq (CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y))) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)) (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)))

theorem CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : C} (h : Quiver.Hom (e.inverse.obj (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) Z) : Eq (CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) (CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) h)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h))

theorem CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : Eq (CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (e.counitIso.hom.app MonoidalCategoryStruct.tensorUnit)) (Functor.OplaxMonoidal.η e.functor)

theorem CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : Quiver.Hom MonoidalCategoryStruct.tensorUnit Z) : Eq (CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.ε e.inverse)) (CategoryStruct.comp (e.counitIso.hom.app MonoidalCategoryStruct.tensorUnit) h)) (CategoryStruct.comp (Functor.OplaxMonoidal.η e.functor) h)

theorem CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) : Eq (CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y)) (e.counitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y))) (CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y)) (MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y)))

theorem CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : D) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj X Y) Z) : Eq (CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y)) (CategoryStruct.comp (e.counitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) h)) (CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y)) h))

theorem CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : Eq (CategoryStruct.comp (e.counitIso.inv.app MonoidalCategoryStruct.tensorUnit) (e.functor.map (Functor.OplaxMonoidal.η e.inverse))) (Functor.LaxMonoidal.ε e.functor)

theorem CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] {Z : D} (h : Quiver.Hom (e.functor.obj MonoidalCategoryStruct.tensorUnit) Z) : Eq (CategoryStruct.comp (e.counitIso.inv.app MonoidalCategoryStruct.tensorUnit) (CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.η e.inverse)) h)) (CategoryStruct.comp (Functor.LaxMonoidal.ε e.functor) h)

theorem CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) : Eq (CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y)))) (CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y) (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))))

theorem CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : D} (h : Quiver.Hom (e.functor.obj (MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y)))) Z) : Eq (CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y))) (CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h)) (CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y) (CategoryStruct.comp (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))) h))

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

Equations

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

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

Equations

• Eq CategoryTheory.Equivalence.instMonoidalInverseRefl (inferInstanceAs (CategoryTheory.Functor.id C).Monoidal)

theorem CategoryTheory.Equivalence.isMonoidal_refl {C : Type u₁} [Category C] [MonoidalCategory C] : refl.IsMonoidal

The obvious auto-equivalence of a monoidal category is monoidal.

theorem CategoryTheory.Equivalence.isMonoidal_symm {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.symm.IsMonoidal

The inverse of a monoidal category equivalence is also a monoidal category equivalence.

def CategoryTheory.Equivalence.instMonoidalFunctorTrans {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (e : Equivalence C D) [e.functor.Monoidal] (e' : Equivalence D E) [e'.functor.Monoidal] : (e.trans e').functor.Monoidal

Equations

• Eq (e.instMonoidalFunctorTrans e') (inferInstanceAs (e.functor.comp e'.functor).Monoidal)

def CategoryTheory.Equivalence.instMonoidalInverseTrans {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (e : Equivalence C D) [e.inverse.Monoidal] (e' : Equivalence D E) [e'.inverse.Monoidal] : (e.trans e').inverse.Monoidal

Equations

• Eq (e.instMonoidalInverseTrans e') (inferInstanceAs (e'.inverse.comp e.inverse).Monoidal)

theorem CategoryTheory.Equivalence.isMonoidal_trans {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (e : Equivalence C D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] (e' : Equivalence D E) [e'.functor.Monoidal] [e'.inverse.Monoidal] [e'.IsMonoidal] : (e.trans e').IsMonoidal

The composition of two monoidal category equivalences is monoidal.

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

Bundled version of lax monoidal functors. This type is equipped with a category structure in CategoryTheory.Monoidal.NaturalTransformation.

• obj : C → D
• map {X Y : C} : Quiver.Hom X Y → Quiver.Hom (self.obj X) (self.obj Y)
• map_id (X : C) : Eq (self.map (CategoryStruct.id X)) (CategoryStruct.id (self.obj X))
• map_comp {X Y Z : C} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) : Eq (self.map (CategoryStruct.comp f g)) (CategoryStruct.comp (self.map f) (self.map g))
• laxMonoidal : self.LaxMonoidal

def CategoryTheory.LaxMonoidalFunctor.of {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : LaxMonoidalFunctor C D

Constructor for LaxMonoidalFunctor C D.

Equations

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

theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : Eq (of F).toFunctor F