# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: submonoid.mem_supr

#### Kevin Buzzard (Apr 15 2021 at 13:18):

For `mem_supr`

for submonoids, subgroups and submodules we tend to have `mem_supr_of_directed`

(if in the supr of a directed collection then it's in one of the collection), and `mem_supr_of_mem`

(if in one of them, then in the supr). Do we have any of the following (I probably only need one):

```
import algebra.big_operators.finprod
import data.finsupp
open_locale big_operators
-- finprod variant
lemma submonoid.mem_supr {M : Type*} [comm_monoid M] (ι : Type*) (f : ι → submonoid M) (m : M) :
m ∈ (⨆ i, f i) ↔ ∃ s : ι → M, ∏ᶠ i, s i = m ∧ ∀ i, s i ∈ f i := sorry
-- finset variant
lemma submonoid.mem_supr' {M : Type*} [add_comm_monoid M] (ι : Type*)
(f : ι → add_submonoid M) (m : M) :
m ∈ (⨆ i, f i) ↔ ∃ (J : finset ι) (s : ι → M), Π j ∈ J, s j = m ∧ ∀ i, s i ∈ f i := sorry
-- finsupp variant which I only know how to make for add_monoids because maybe we don't have `→₁`?
lemma add_submonoid.mem_supr {M : Type*} [add_comm_monoid M] (ι : Type*)
(f : ι → add_submonoid M) (m : M) :
m ∈ (⨆ i, f i) ↔ ∃ s : ι →₀ M, s.sum (λ a b, b) = m ∧ ∀ i, s i ∈ f i := sorry
```

[There are also versions for `subgroup`

and `submodule`

]. It would not surprise me if we had ways of moving from any of these three lemmas to any other (modulo issues with the multiplicative version with finsupp). I would imagine it would not be hard to prove any or all of these using some kind of induction principle if we knew that the supr was the closure of the set.Union, because we have docs#submonoid.closure_induction . Do we already have anything else which would make one of these short?

#### Eric Wieser (Apr 15 2021 at 13:26):

Does docs#add_submonoid.closure_Union help?

#### Kevin Buzzard (Apr 15 2021 at 13:44):

It's definitely a step in the right direction. From then on it's just some induction I guess. Thanks!

Last updated: May 16 2021 at 05:21 UTC