docs#Group.FG vs docs#Monoid.FG

Stream: mathlib4

[Yaël Dillies]

Is there any reason we have both docs#Group.FG and docs#Monoid.FG given that they are unconditionally equivalent (cf docs#Group.fg_iff_monoid_fg)?

[Kevin Buzzard]

I could imagine that it's slightly more convenient to get access to the finite set which generates the group this way. Perhaps more importantly if we don't have it, then we'll just get people asking where it is and the answer "aha, if you think about it then it's equivalent to saying it's finitely-generated as a monoid (so that's why you couldn't find it, aren't we clever hiding it from you like that)" is kind of a crappy answer.

[Eric Wieser]

I think that's the same story as VectorSpace vs Module though. If we care about this kind of thing, I think we want something like @[pedagogical_alias] which makes it appear in the docs, but emits a deprecation-like warning if you actually use it

[Damiano Testa]

Or just deprecated pointing to the "mature" version.

[Kevin Buzzard]

The difference here is that mathematically a vector space is literally by definition a module over a field, but the proof that a group is group-fg iff it's monoid-fg needs an observation, ie it's not completely content-free

[Damiano Testa]

The attribute could also take a string input that could mention that (at most) doubling a finite set yields a finite set.

[Kevin Buzzard]

I think that if Group.FG emits a warning to use Monoid.FG instead then it will make mathlib less readable. Finitely-generated groups are a well-studied thing and a serious area of mathematics; conversely most mathematicians haven't heard of monoids (this is another way that this question differs from the vector space question). So I propose that if we're going to deprecate one, we deprecate Monoid.FG, just like we talk about RingHoms between semirings etc. More precisely I mean we just delete Monoid.FG and redefine Group.FG to mean Monoid.FG and eat a monoid.

[Yaël Dillies]

Do you also want us to rename docs#Monoid.IsTorsionFree to Group.IsTorsionFree?

[Kevin Buzzard]

I can say with confidence that I have worked with people whose job it is to study finitely-generated groups (and who I'm assuming would be annoyed if all their theorems have to be written Monoid.FG G), but I am less sure about torsionfreeness.

[Eric Wieser]

Damiano Testa said:

Or just deprecated pointing to the "mature" version.

deprecated has semantics "you can delete this from mathlib eventually", which we don't want here

[Eric Wieser]

Kevin Buzzard said:

The difference here is that mathematically a vector space is literally by definition a module over a field, but the proof that a group is group-fg iff it's monoid-fg needs an observation, ie it's not completely content-free

Maybe the fact that Module is actually a semimodule is more relevant here then

[Kevin Buzzard]

Yes, it seems Field : VectorSpace :: Ring : Module :: Semiring : Semimodule and we have chosen Module as the name, perhaps because it is somehow the inf of the names which are commonly used in e.g. a typical undergraduate mathematics course.

[Damiano Testa]

Anyway, I think that I agree with Kevin that switching to fg monoids rather than fg groups is not great from the point of view of "informal" maths.

[Eric Wieser]

Should we play a similar game for monoids and use Group.FG to refer to monoids too?

[Damiano Testa]

My feeling is that trying to apply a uniform heuristic to resolve all/most of these issues will result in the heuristic that we go on a case-by-case basis.