Membership in Sup of submodules

Stream: Is there code for X?

[Adam Topaz]

Do we have something along the following lines?

import linear_algebra

variables (A : Type*) [ring A] (M : Type*) [add_comm_group M] [module A M]

example {ι} (T : ι → submodule A M) (m : M) (cond : m ∈ ⨆ (i : ι), T i) :
  ∃ (F : finset ι), m ∈ ⨆ (f ∈ F), T f := sorry

[Heather Macbeth]

docs#submodule.exists_finset_of_mem_supr ?

[Adam Topaz]

Thanks! I don't know how I missed that!

[Heather Macbeth]

Take comfort in the fact that your lemma statement is virtually identical to the mathlib gold standard :)

[Adam Topaz]

The proof in mathlib seems more complicated than necessary.

[Adam Topaz]

import data.finset.basic
import linear_algebra

open_locale classical

variables {A : Type*} [ring A] {M : Type*} [add_comm_group M] [module A M] {ι : Type*} (T : ι → submodule A M)

example {ι} (T : ι → submodule A M) (m : M) (cond : m ∈ ⨆ (i : ι), T i) :
  ∃ (F : finset ι), m ∈ ⨆ (f ∈ F), T f :=
begin
  let ι' : finset ι → submodule A M := λ S, ⨆ (s ∈ S), T s,
  have : directed (≤) ι',
  { intros S T,
    refine ⟨S ⊔ T, supr_le_supr _, supr_le_supr _⟩,
    all_goals { intros y,
    simp only [supr_le_iff, finset.sup_eq_union, finset.mem_union],
    intros hy v hv,
    refine submodule.mem_supr_of_mem (finset.mem_union_left _ hy) hv <|>
    refine submodule.mem_supr_of_mem (finset.mem_union_right _ hy) hv } },
  rw ← submodule.mem_supr_of_directed ι' this,
  suffices : (⨆ (i : ι), T i) ≤ supr ι', by exact this cond,
  refine supr_le_supr2 (λ i, ⟨{i},_⟩),
  dsimp only [ι'],
  simp [le_refl],
end

[Adam Topaz]

Maybe that's not much better :)