(Lax) monoidal functors #
A lax monoidal functor F
between monoidal categories C
and D
is a functor between the underlying categories equipped with morphisms
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
(called the unit morphism)μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y)
(called the tensorator, or strength). satisfying various axioms.
A monoidal functor is a lax monoidal functor for which ε
and μ
are isomorphisms.
We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.
See also CategoryTheory.Monoidal.Functorial
for a typeclass decorating an object-level
function with the additional data of a monoidal functor.
This is useful when stating that a pre-existing functor is monoidal.
See CategoryTheory.Monoidal.NaturalTransformation
for monoidal natural transformations.
We show in CategoryTheory.Monoidal.Mon_
that lax monoidal functors take monoid objects
to monoid objects.
Future work #
- Oplax monoidal functors.
References #
- obj : C → D
- map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
- map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
- ε : CategoryTheory.MonoidalCategory.tensorUnit D ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorUnit C)
unit morphism
- μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (s.obj X) (s.obj Y) ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
tensorator
- μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.map f) (s.map g)) (CategoryTheory.LaxMonoidalFunctor.μ s Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s X X') (s.map (CategoryTheory.MonoidalCategory.tensorHom f g))
- associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ s X Y) (CategoryTheory.CategoryStruct.id (s.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (s.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (s.obj X) (s.obj Y) (s.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ s Y Z)) (CategoryTheory.LaxMonoidalFunctor.μ s X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
associativity of the tensorator
- left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.ε (CategoryTheory.CategoryStruct.id (s.obj X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s (CategoryTheory.MonoidalCategory.tensorUnit C) X) (s.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
- right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) s.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s X (CategoryTheory.MonoidalCategory.tensorUnit C)) (s.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
A lax monoidal functor is a functor F : C ⥤ D
between monoidal categories,
equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C)
and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
,
satisfying the appropriate coherences.
Instances For
- obj : C → D
- map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
- map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
- μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (s.obj X) (s.obj Y) ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
- μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.map f) (s.map g)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X X') (s.map (CategoryTheory.MonoidalCategory.tensorHom f g))
- associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y) (CategoryTheory.CategoryStruct.id (s.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (s.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (s.obj X) (s.obj Y) (s.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Z)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
- left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.ε (CategoryTheory.CategoryStruct.id (s.obj X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit C) X) (s.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
- right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) s.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorUnit C)) (s.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
- ε_isIso : CategoryTheory.IsIso s.ε
- μ_isIso : ∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y)
A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.
See https://stacks.math.columbia.edu/tag/0FFL.
Instances For
The unit morphism of a (strong) monoidal functor as an isomorphism.
Instances For
The tensorator of a (strong) monoidal functor as an isomorphism.
Instances For
The identity lax monoidal functor.
Instances For
The tensorator as a natural isomorphism.
Instances For
Monoidal functors commute with left tensoring up to isomorphism
Instances For
Monoidal functors commute with right tensoring up to isomorphism
Instances For
The identity monoidal functor.
Instances For
The composition of two lax monoidal functors is again lax monoidal.
Instances For
The composition of two lax monoidal functors is again lax monoidal.
Instances For
The cartesian product of two lax monoidal functors is lax monoidal.
Instances For
The diagonal functor as a monoidal functor.
Instances For
The cartesian product of two lax monoidal functors starting from the same monoidal category C
is lax monoidal.
Instances For
The composition of two monoidal functors is again monoidal.
Instances For
The composition of two monoidal functors is again monoidal.
Instances For
The cartesian product of two monoidal functors is monoidal.
Instances For
The cartesian product of two monoidal functors starting from the same monoidal category C
is monoidal.
Instances For
If we have a right adjoint functor G
to a monoidal functor F
, then G
has a lax monoidal
structure as well.
Instances For
If a monoidal functor F
is an equivalence of categories then its inverse is also monoidal.