Zulip Chat Archive

Stream: Is there code for X?

Topic: Membership in Sup of submodules


view this post on Zulip 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

view this post on Zulip Heather Macbeth (Feb 09 2021 at 03:10):

docs#submodule.exists_finset_of_mem_supr ?

view this post on Zulip Adam Topaz (Feb 09 2021 at 03:13):

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

view this post on Zulip 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 :)

view this post on Zulip Adam Topaz (Feb 09 2021 at 03:14):

The proof in mathlib seems more complicated than necessary.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 09 2021 at 03:47):

Maybe that's not much better :)


Last updated: May 16 2021 at 05:21 UTC