linear independence

Stream: maths

[Chris Hughes]

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]

I think it's true

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

You probably need to assume the ring is nonzero

[Kenny Lau]

oh no

[Kenny Lau]

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]

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

[Kenny Lau]

oh no

[Mario Carneiro]

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

[Mario Carneiro]

I think it is

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

heh

[Kenny Lau]

any two singletons are canonically correspondent

[Kevin Buzzard]

rofl the result is false

[Kevin Buzzard]

Touche Chris

[Kevin Buzzard]

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]

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]

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

[Neil Strickland]

(deleted)