Group (/Monoid/etc) closures are a finite product/sum

Stream: mathlib4

[Alex Meiburg]

The formal definition of the subgroup closure involves the infimum of subgroups that contain a set, but the "undergrad" definition is "the set of elements that you can write as finite products". This fact doesn't actually seem to be in Mathlib, in any form I could recognize. I think this would be written as,

@[to_additive]
theorem closure_mem_iff_list_prod {G : Type*} [Monoid G] (S : Set G) (x : G) :
    x ∈ Submonoid.closure S ↔ (∃ (l : List G), (∀ y ∈ l, y ∈ S) ∧ x = l.prod) := by
  sorry

@[to_additive]
theorem closure_mem_iff_finprod {G : Type*} [CommMonoid G] (S : Set G) (x : G) :
    x ∈ Submonoid.closure S ↔ (∃ (l : Multiset G), (∀ y ∈ l, y ∈ S) ∧ x = l.prod) := by
  sorry

@[to_additive]
theorem closure_mem_iff_inv_list_prod {G : Type*} [Group G] (S : Set G) (x : G) :
    x ∈ Subgroup.closure S ↔ (∃ (l : List G), (∀ y ∈ l, y ∈ S ∨ y⁻¹ ∈ S) ∧ x = l.prod) := by
  sorry

@[to_additive]
theorem closure_mem_iff_inv_finprod {G : Type*} [CommGroup G] (S : Set G) (x : G) :
    x ∈ Subgroup.closure S ↔ (∃ (l : Multiset G), (∀ y ∈ l, y ∈ S ∨ y⁻¹ ∈ S) ∧ x = l.prod) := by
  sorry

Would such a theorem be welcome? Any better names / ideas for better ways to write it?

[Alex Meiburg]

e.g. one alternate statement would be that for a CommGroup it's a Finsupp (G × ℤ) whose product of nsmul's adds up to the right value

[Daniel Weber]

Another option is showing that it's the range of docs#FreeMonoid.lift, docs#FreeGroup.lift, docs#FreeAbelianGroup.lift (I can't find FreeCommMonoid, but maybe there's something equivalent to it), with the type ↥S and the function Subtype.val

[Ruben Van de Velde]

Maybe docs#Submonoid.closure_eq_image_prod ?

[Patrick Massot]

I am a bit surprised that this is missing because some people are bound to complain about it. But I’m not surprised at all that it is not needed.

[Patrick Massot]

And you call it the undergrad definition of closure, but it definitely depends on the kind of undergrad studies you did. I certainly learned the Mathlib definition and saw your definition as a property (well, I saw intersection instead of infimum).

[Patrick Massot]

And, as Ruben pointed out, the monoid version is already there.

[Kevin Buzzard]

There's no harm in having it. I agree with Patrick though, the problem is when people think it might be useful :-) Mathematicians sometimes feel like they like to "have a formula for something". There are times when it's not possible to have a formula, e.g. there's no useful "formula" for a general Borel set as far as I know -- if you want to prove a predicate about Borel sets then you prove it for open sets, complements, countable unions and then say you're done by induction. Here there is a "formula" for the general element of a group closure but again using the recursor usually seems to give slicker proofs.

[Eric Wieser]

Though this wisdom didn't seem to apply to coalgebras, where it looks like machinery to pick a formula did make things easier

[Alex Meiburg]

Ruben Van de Velde said:

Maybe docs#Submonoid.closure_eq_image_prod ?

Oops, I'm embarrassed I missed that :) mostly cause I was looking for a Group version when searching I guess, and a Finset.prod version.

Well, any Submonoid one with Subgroup.closure_toSubmonoid gives the subgroup one, the only thing that wouldn't be a one-liner then is a Finsupp G ℤ version, which would instead be maybe three lines. Meh

[Eric Wieser]

We have the Finsupp version for submodules

[Kevin Buzzard]

Yes the coalgebra example was quite enlightening, it was something where I expected ext to do everything but we really seemed to need that a general element of $A\otimes B$ had a "formula".

[Eric Wieser]

My suspicion is that this is not the case, and that choosing a formula is just pragmatic because:

• that's what the literature does
• we don't have the machinery to make working with the non-category-theoretic version of monoidal categories pleasant

both of which are good enough reasons to use the "formula" version in mathlib