Zulip Chat Archive

Stream: maths

Topic: linear independence


view this post on Zulip Chris Hughes (Jul 18 2019 at 21:43):

I'm struggling to prove this lemma about linear independence. Not sure it's even stated correctly.

lemma le_of_span_le_span  {R : Type*} {M : Type*} [comm_ring R] [add_comm_group M] [module R M]
  [decidable_eq R] [decidable_eq M]  {s t u: set M}
  (hl : linear_independent R (subtype.val : u  M)) (hsu : s  u) (htu : t  u)
  (hst : span R s  span R t) : s  t :=

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:56):

I think it's true

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:57):

I guess the last bit could be an iff, but otherwise it looks fine

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:58):

You could state it with functions; the claim would be that the function from s to u factors through t

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:00):

It certainly looks true. I want to argue that if a \in s then single a or whatever it's called is in the t-span and one of the finitely many functions involved will mention...wait wait What is the definition of span?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:02):

OK I looked. I guess the reason I say it's obvious is that I am thinking about everything in the span being a finite R-linear combination of elements in the set.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:04):

I have some canonical surjection from (s ->0 R) to the R-span and I pull back and argue up there.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:18):

You probably need to assume the ring is nonzero

view this post on Zulip Kenny Lau (Jul 18 2019 at 22:19):

oh no

view this post on Zulip Kenny Lau (Jul 18 2019 at 22:20):

if the ring is zero then hl implies u is empty, so s and t are both empty by hsu and htu, so the theorem is true

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:22):

I think it's the other way around - linear_independent_of_zero_eq_one says everything is independent in the zero ring

view this post on Zulip Kenny Lau (Jul 18 2019 at 22:23):

oh no

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:23):

Is every module over the zero ring equal to {0}?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:23):

I think it is

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:24):

so then s = u = {0} and t = {} violate the theorem

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:25):

Every module over the zero ring is canoncially isomorphic to {0}

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:25):

heh

view this post on Zulip Kenny Lau (Jul 18 2019 at 22:26):

any two singletons are canonically correspondent

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:26):

rofl the result is false

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:26):

Touche Chris

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:27):

The spectrum of the zero ring is empty so there is no point where you can realise your inclusion. There's probably a way to think about this in terms of toposes.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:40):

lemma le_of_span_le_span {R : Type*} {M : Type*} [comm_ring R] [add_comm_group M] [module R M]
  [decidable_eq R] [decidable_eq M]  {s t u: set M} (zero_ne_one : (1 : R)  0)
  (hl : linear_independent R (subtype.val : u  M)) (hsu : s  u) (htu : t  u)
  (hst : span R s  span R t) : s  t :=
begin
  have := eq_of_linear_independent_of_span_subtype zero_ne_one
    (hl.mono (set.union_subset hsu htu))
    (set.subset_union_right _ _)
    (set.union_subset (set.subset.trans subset_span hst) subset_span),
  rw  this, apply set.subset_union_left
end

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:47):

I see that restricting to the true subcase made things easier.

view this post on Zulip Neil Strickland (Jan 11 2020 at 15:44):

(deleted)


Last updated: May 19 2021 at 02:10 UTC