Linear basis from spanning set

Stream: Is there code for X?

[Oliver Nash]

I'm having trouble finding this:

import linear_algebra.linear_independent
import linear_algebra.basis

variables (k V : Type*) [field k] [add_comm_group V] [module k V]

example (s : set V) : ∃ (t : set V),
  t ⊆ s ∧
  submodule.span k t = submodule.span k s ∧
  linear_independent k (coe : t → V) :=
sorry

[Oliver Nash]

Surely we have this (or I guess maybe the family version with v : ι → V instead of s) somewhere?

[Oliver Nash]

Well I now have this disgusting proof:

import linear_algebra.linear_independent
import linear_algebra.basis

variables (k V : Type*) [division_ring k] [add_comm_group V] [module k V]

example {ι : Type*} (v : ι → V) : ∃ I : set ι,
  submodule.span k (v '' I) = submodule.span k (v '' set.univ) ∧
  linear_independent k (v ∘ (coe : I → ι)) :=
begin
  obtain ⟨I, hI₁, hI₂⟩ := exists_maximal_independent k v,
  refine ⟨I, _, hI₁⟩,
  apply le_antisymm,
  { apply submodule.span_mono,
    simp, },
  { rw submodule.span_le,
    rintros - ⟨i, -, rfl⟩,
    by_cases hi : i ∈ I,
    { apply submodule.subset_span,
      exact ⟨i, hi, rfl⟩, },
    { obtain ⟨t, ht₁, ht₂⟩ := hI₂ i hi,
      replace ht₂ := submodule.smul_mem _ t⁻¹ ht₂,
      rwa [smul_smul, inv_mul_cancel ht₁, one_smul] at ht₂, }, },
end

but I'm sure this must already exist somewhere. Any advice, much appreciated.

[Scott Morrison]

Haha, the module doc claims it's there: "We also prove that, when working over a field,
any family of vectors includes a linear independent subfamily spanning the same subspace."

But I don't see it yet.

[Oliver Nash]

OK I'm just about done for the day but I'll pick this up again tomorrow then.

[Oliver Nash]

The linear algebra library (esp. the fancy strong rank condition stuff) is really awesome so I guess I was surprised at this (apparent?) gap.

[Scott Morrison]

The linear algebra library has undergone lots of revisions and modifications: it could really do with a nice tutorial / howto document!

[Yaël Dillies]

Scott Morrison said:

Haha, the module doc claims it's there: "We also prove that, when working over a field,
any family of vectors includes a linear independent subfamily spanning the same subspace."

Filippo was looking for the set version, not the indexed family one, but I guess you looked for both.

[Scott Morrison]

Yes, I couldn't find either. I'm fearing that when someone tracks this down it will be me that accidentally deleted it in some PR. :-)

[Yaël Dillies]

Exciting! :rofl:

[Eric Wieser]

Does a git blame on that docstring help?

[Oliver Nash]

Somehow I was blind yesterday evening. We have docs#exists_linear_independent So for example we can do the following:

import linear_algebra.linear_independent

variables (k V : Type*) [division_ring k] [add_comm_group V] [module k V]

example (s : set V) : ∃ (t : set V),
  t ⊆ s ∧
  submodule.span k t = submodule.span k s ∧
  linear_independent k (coe : t → V) :=
begin
  obtain ⟨t, ht₁, -, ht₂, ht₃⟩ :=
    exists_linear_independent (linear_independent_empty k V) (set.empty_subset s),
  exact ⟨t, ht₁, le_antisymm (submodule.span_mono ht₁) (submodule.span_le.mpr ht₂), ht₃⟩,
end

[Oliver Nash]

I'm not sure if I prefer my submodule.span k t = submodule.span k s or the equivalent statement in the conclusion of docs#exists_linear_independent s ⊆ submodule.span k t but I think the specialisation of docs#exists_linear_independent to the case when we're extending the empty set is worth adding so I'll do that now.

[Oliver Nash]

#9708

[Scott Morrison]

Yes, the specialization is definitely helpful: at least two of us looks at exists_linear_independent and failed to see how to use it immediately. :-)