## Stream: maths

### Topic: linear independence

#### 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 :=


#### Mario Carneiro (Jul 18 2019 at 21:56):

I think it's true

#### Mario Carneiro (Jul 18 2019 at 21:57):

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

#### 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

#### 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?

#### 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.

#### 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.

#### Mario Carneiro (Jul 18 2019 at 22:18):

You probably need to assume the ring is nonzero

oh no

#### 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

#### 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

oh no

#### Mario Carneiro (Jul 18 2019 at 22:23):

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

I think it is

#### Mario Carneiro (Jul 18 2019 at 22:24):

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

#### Kevin Buzzard (Jul 18 2019 at 22:25):

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

heh

#### Kenny Lau (Jul 18 2019 at 22:26):

any two singletons are canonically correspondent

#### Kevin Buzzard (Jul 18 2019 at 22:26):

rofl the result is false

Touche Chris

#### 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.

#### 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


#### Kevin Buzzard (Jul 18 2019 at 22:47):

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

#### Neil Strickland (Jan 11 2020 at 15:44):

(deleted)

Last updated: May 19 2021 at 02:10 UTC