submonoid.mem_supr

Stream: Is there code for X?

[Kevin Buzzard]

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]

Does docs#add_submonoid.closure_Union help?

[Kevin Buzzard]

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

[Eric Wieser]

docs#submodule.mem_supr_iff_exists_dfinsupp (once CI rebuilds the docs)