Free monoids in a monoidal category

Stream: maths

[Albus Dompeldorius]

I'm wondering how to define free monoids in a monoidal category in Mathlib, as in
here.

In Mathlib there is currently a definition of the category of monoid objects in a monoidal category, and a forgetful functor from this category to the underlying monoidal category, so it seems we want to prove that under some conditions on the monoidal category, this functor has a left adjoint.

My questions are:

1. Is this defined already in Mathlib (I couldn't find it)?
2. Any ideas on how to prove this? It doesn't need to be the most general version, for my usecase, the category is cartesian closed.
3. Should I open an issue on this?

[Joël Riou]

We have some of the ingredients which could be helpful here. Let us say C is a monoidal category, and X : C.
I think the first step is to define a monoidal functor Discrete ℕ ⥤ C which sends 1 to X. (We have such a universal property for the free monoidal category on a single element, see docs#CategoryTheory.FreeMonoidalCategory.project but not yet with Discrete ℕ). Then, if M is a monoid and we have a monoidal functor F : Discrete M ⥤ C, you may investigate the conditions which allow to put a monoid structure on the colimit of F. Also, does it work for the colimit of any monoidal functor F : D ⥤ C, even if D is not necessarily Discrete M?! If so, the proofs of the compatibilities would probably be cleaner than in the particular case of coproducts.

[Albus Dompeldorius]

Thanks! To get the universal property for
Discrete ℕ, I guess we could show that Discrete is left adjoint to the forgetful functor from strict monoidal categories to monoids, which sends a strict monoidal category to its underlying monoid of objects?

[Joël Riou]

We do not have (and I am not sure mathlib would like to have) a notion of "strict" monoidal category. I would state what we want by saying that the category of monoidal functors from Discrete ℕ to C is equivalent to C.

[Albus Dompeldorius]

I see! I'm also considering a different approach, where we define a free monoid in C, where C is a closed monoidal category, to be the initial algebra of the endofunctor X ↦ 1 + (A ⊗ X).