freeness in monoids

Stream: new members

[Philippe Duchon]

(Not sure if this is the right channel for this question; I am thinking maybe it is because the question clearly demonstrates I am not - yet - proficient enough with searching Mathlib documentation)

Background: I have a colleague with whom I often discuss various mathematical topics over lunch; today, for some reason we discussed theorems about free monoids. And at some point, I said "let's see what Mathlib knows about free monoids", took out my laptop and made a quick search.

I quickly found docs#FreeMonoid, but this is the description of the free monoid generated by some type (and understandably, even to me, it is "just" the type of lists over the same type, with concatenation as multiplication); but what I was looking for was a way to state that a given monoid is free, or that it is freely generated by some collection of monoid elements; something like docs#IsFreeGroup but for monoids instead of groups.

Does something like this exist in Mathlib? (If not, then very likely the theorems we were discussing are not in there either; of course I tried to search for IsFreeMonoid, but the fact that I did not find anything is just proof that, if it exists, the name is somewhat different )

[Aaron Liu]

No we don't have this

[Philippe Duchon]

OK, thanks. Is it because it's not interesting enough, or just because nobody had the time/energy/willingness to work on it? Or maybe it's difficult to integrate properly with the rest of the library?

[Aaron Liu]

probably some combination of the three

[Aaron Liu]

I just did a search of all the predicates mentioning monoids and checked all the results and none of them were "is free monoid"