## Stream: Is there code for X?

### Topic: Membership in Sup of submodules

#### Adam Topaz (Feb 09 2021 at 03:02):

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


#### Adam Topaz (Feb 09 2021 at 03:13):

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

#### Heather Macbeth (Feb 09 2021 at 03:13):

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

#### Adam Topaz (Feb 09 2021 at 03:14):

The proof in mathlib seems more complicated than necessary.

#### Adam Topaz (Feb 09 2021 at 03:47):

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 (Feb 09 2021 at 03:47):

Maybe that's not much better :)

Last updated: May 16 2021 at 05:21 UTC