(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 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
- Oplax monoidal functors.
References
See https://stacks.math.columbia.edu/tag/0FFL.
- to_functor : C ⥤ D
- ε : 𝟙_ D ⟶ c.to_functor.obj (𝟙_ C)
- μ : Π (X Y : C), c.to_functor.obj X ⊗ c.to_functor.obj Y ⟶ c.to_functor.obj (X ⊗ Y)
- μ_natural' : (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' = c.μ X X' ≫ c.to_functor.map (f ⊗ g)) . "obviously"
- associativity' : (∀ (X Y Z : C), (c.μ X Y ⊗ 𝟙 (c.to_functor.obj Z)) ≫ c.μ (X ⊗ Y) Z ≫ c.to_functor.map (α_ X Y Z).hom = (α_ (c.to_functor.obj X) (c.to_functor.obj Y) (c.to_functor.obj Z)).hom ≫ (𝟙 (c.to_functor.obj X) ⊗ c.μ Y Z) ≫ c.μ X (Y ⊗ Z)) . "obviously"
- left_unitality' : (∀ (X : C), (λ_ (c.to_functor.obj X)).hom = (c.ε ⊗ 𝟙 (c.to_functor.obj X)) ≫ c.μ (𝟙_ C) X ≫ c.to_functor.map (λ_ X).hom) . "obviously"
- right_unitality' : (∀ (X : C), (ρ_ (c.to_functor.obj X)).hom = (𝟙 (c.to_functor.obj X) ⊗ c.ε) ≫ c.μ X (𝟙_ C) ≫ c.to_functor.map (ρ_ X).hom) . "obviously"
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
the appropriate coherences.
- to_lax_monoidal_functor : category_theory.lax_monoidal_functor C D
- ε_is_iso : category_theory.is_iso c.to_lax_monoidal_functor.ε . "apply_instance"
- μ_is_iso : (Π (X Y : C), category_theory.is_iso (c.to_lax_monoidal_functor.μ X Y)) . "apply_instance"
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 unit morphism of a (strong) monoidal functor as an isomorphism.
Equations
The tensorator of a (strong) monoidal functor as an isomorphism.
Equations
- F.μ_iso X Y = category_theory.as_iso (F.to_lax_monoidal_functor.μ X Y)
The identity lax monoidal functor.
Equations
- category_theory.lax_monoidal_functor.id C = {to_functor := {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
Equations
The tensorator as a natural isomorphism.
The identity monoidal functor.
Equations
- category_theory.monoidal_functor.id C = {to_lax_monoidal_functor := {to_functor := {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := category_theory.is_iso.id (𝟙_ C), μ_is_iso := λ (X Y : C), category_theory.is_iso.id ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y)}
Equations
The composition of two lax monoidal functors is again lax monoidal.
Equations
- F ⊗⋙ G = {to_functor := {obj := (F.to_functor ⋙ G.to_functor).obj, map := (F.to_functor ⋙ G.to_functor).map, map_id' := _, map_comp' := _}, ε := G.ε ≫ G.to_functor.map F.ε, μ := λ (X Y : C), G.μ (F.to_functor.obj X) (F.to_functor.obj Y) ≫ G.to_functor.map (F.μ X Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
The composition of two monoidal functors is again monoidal.
Equations
- F ⊗⋙ G = {to_lax_monoidal_functor := {to_functor := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).to_functor, ε := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).ε, μ := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := id category_theory.is_iso.comp_is_iso, μ_is_iso := id (λ (X Y : C), category_theory.is_iso.comp_is_iso)}