mathlib documentation

category_theory.monoidal.functor

(Lax) monoidal functors #

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

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

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

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

See category_theory.monoidal.natural_transformation for monoidal natural transformations.

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

Future work #

References #

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

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

@[simp]
theorem category_theory.lax_monoidal_functor.μ_natural {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X Y) (g : X' Y') :
(self.to_functor.map f self.to_functor.map g) self.μ Y Y' = self.μ X X' self.to_functor.map (f g)
@[simp]
theorem category_theory.lax_monoidal_functor.μ_natural_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X Y) (g : X' Y') {X'_1 : D} (f' : self.to_functor.obj (Y Y') X'_1) :
(self.to_functor.map f self.to_functor.map g) self.μ Y Y' f' = self.μ X X' self.to_functor.map (f g) f'
@[simp]
theorem category_theory.lax_monoidal_functor.associativity {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) (X Y Z : C) :
(self.μ X Y 𝟙 (self.to_functor.obj Z)) self.μ (X Y) Z self.to_functor.map (α_ X Y Z).hom = (α_ (self.to_functor.obj X) (self.to_functor.obj Y) (self.to_functor.obj Z)).hom (𝟙 (self.to_functor.obj X) self.μ Y Z) self.μ X (Y Z)
@[simp]
theorem category_theory.lax_monoidal_functor.associativity_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) (X Y Z : C) {X' : D} (f' : self.to_functor.obj (X (Y Z)) X') :
(self.μ X Y 𝟙 (self.to_functor.obj Z)) self.μ (X Y) Z self.to_functor.map (α_ X Y Z).hom f' = (α_ (self.to_functor.obj X) (self.to_functor.obj Y) (self.to_functor.obj Z)).hom (𝟙 (self.to_functor.obj X) self.μ Y Z) self.μ X (Y Z) f'
structure category_theory.monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] :
Type (max u₁ u₂ v₁ v₂)

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

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

The identity lax monoidal functor.

Equations

The identity monoidal functor.

Equations

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

Equations