Unbundled lax monoidal functors
Design considerations
The essential problem I've encountered that requires unbundled functors is
having an existing (non-monoidal) functor F : C ⥤ D between monoidal categories,
and wanting to assert that it has an extension to a lax monoidal functor.
The two options seem to be
- Construct a separate
F' : lax_monoidal_functor C D, and assertF'.to_functor ≅ F. - Introduce unbundled functors and unbundled lax monoidal functors,
and construct
lax_monoidal F.obj, then constructF' := lax_monoidal_functor.of F.obj.
Both have costs, but as for option 2. the cost is in library design, while in option 1. the cost is users having to carry around additional isomorphisms forever, I wanted to introduce unbundled functors.
TODO: later, we may want to do this for strong monoidal functors as well, but the immediate application, for enriched categories, only requires this notion.
- ε : 𝟙_ D ⟶ F (𝟙_ C)
- μ : Π (X Y : C), F X ⊗ F Y ⟶ F (X ⊗ Y)
- μ_natural' : (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (category_theory.map F f ⊗ category_theory.map F g) ≫ category_theory.lax_monoidal.μ F Y Y' = category_theory.lax_monoidal.μ F X X' ≫ category_theory.map F (f ⊗ g)) . "obviously"
- associativity' : (∀ (X Y Z : C), (category_theory.lax_monoidal.μ F X Y ⊗ 𝟙 (F Z)) ≫ category_theory.lax_monoidal.μ F (X ⊗ Y) Z ≫ category_theory.map F (α_ X Y Z).hom = (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ category_theory.lax_monoidal.μ F Y Z) ≫ category_theory.lax_monoidal.μ F X (Y ⊗ Z)) . "obviously"
- left_unitality' : (∀ (X : C), (λ_ (F X)).hom = (category_theory.lax_monoidal.ε F ⊗ 𝟙 (F X)) ≫ category_theory.lax_monoidal.μ F (𝟙_ C) X ≫ category_theory.map F (λ_ X).hom) . "obviously"
- right_unitality' : (∀ (X : C), (ρ_ (F X)).hom = (𝟙 (F X) ⊗ category_theory.lax_monoidal.ε F) ≫ category_theory.lax_monoidal.μ F X (𝟙_ C) ≫ category_theory.map F (ρ_ X).hom) . "obviously"
An unbundled description of lax monoidal functors.
Construct a bundled lax_monoidal_functor from the object level function
and functorial and lax_monoidal typeclasses.
Equations
- category_theory.lax_monoidal_functor.of F = {to_functor := {obj := F, map := category_theory.functorial.map I₁, map_id' := _, map_comp' := _}, ε := category_theory.lax_monoidal.ε F I₂, μ := category_theory.lax_monoidal.μ F I₂, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
Equations
- category_theory.category_theory.lax_monoidal F = {ε := F.ε, μ := F.μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
Equations
- category_theory.lax_monoidal_id = {ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 (id X ⊗ id Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}