more linear algebra

Stream: Is there code for X?

[Alex Kontorovich]

What's the easiest way to prove a bunch of vectors are linearly independent? Say I have an n-dimensional vector space E with a bilinear form Q, and a collection of n vectors vs so that the gram matrix G=vs Q vs of Q-inner products is invertible. (As a human, this means the matrix of vs is invertible too, and hence linearly independent, in fact a basis. Actually, showing that they span will be my next annoying question...) Any help would be much appreciated! Thanks!

import analysis.inner_product_space.basic
import data.real.basic

example (E : Type*) {n : ℕ} [inner_product_space ℝ E] [finite_dimensional ℝ E]
  [fact (finite_dimensional.finrank ℝ E = n)] [fact (n ≠ 0)] (vs : fin n → E) (Q : E →ₗ[ℝ] E →ₗ[ℝ] ℝ )
  (G : matrix (fin n) (fin n) ℝ) (hG : invertible G) (h : ∀ i j, Q (vs i) (vs j) = G i j) :
  linear_independent ℝ vs
:= begin
  sorry,
end

[Eric Wieser]

I suspect docs#matrix.to_linear_equiv' will be useful here

[Junyan Xu]

Here's a proof; the simple lemma matrix.range_to_lin' is apparently missing from mathlib.

import analysis.inner_product_space.basic
import data.real.basic
import data.matrix.rank

lemma matrix.range_to_lin' {R} [comm_semiring R] {m n} [fintype n] [decidable_eq n]
  (G : matrix m n R) : G.to_lin'.range = submodule.span R (set.range G.transpose) :=
begin
  rw [linear_map.range_eq_map, ← linear_map.supr_range_std_basis],
  simp_rw [submodule.map_supr, linear_map.range_eq_map, ← ideal.span_one, ideal.span,
    submodule.map_span, set.image_image],
  dsimp only [set.has_one, has_one.one],
  simp_rw set.image_singleton,
  apply le_antisymm,
  { refine supr_le (λ i, submodule.span_mono _),
    rintro _ ⟨_, rfl⟩,
    exact ⟨i, (G.mul_vec_std_basis_apply i).symm⟩ },
  { rw submodule.span_le,
    rintro _ ⟨i, rfl⟩,
    apply submodule.mem_supr_of_mem i,
    exact submodule.subset_span (G.mul_vec_std_basis_apply i).symm },
end

example (E : Type*) {n : ℕ} [inner_product_space ℝ E] [finite_dimensional ℝ E]
  (hr : finite_dimensional.finrank ℝ E = n) (vs : fin n → E) (Q : E →ₗ[ℝ] E →ₗ[ℝ] ℝ)
  (G : matrix (fin n) (fin n) ℝ) (hG : invertible G) (h : ∀ i j, Q (vs i) (vs j) = G i j) :
  linear_independent ℝ vs :=
begin
  apply linear_independent.of_comp Q.flip,
  rw linear_independent_iff_card_eq_finrank_span,
  apply le_antisymm,
  { rw ← G.rank_of_is_unit (is_unit_of_invertible G),
    unfold set.finrank matrix.rank,
    rw G.range_to_lin',
    let f : (E →ₗ[ℝ] ℝ) →ₗ[ℝ] fin n → ℝ := linear_map.pi (λ i, linear_map.applyₗ $ vs i),
    rw (by { ext j i, exact (h i j).symm } : G.transpose = f ∘ (Q.flip ∘ vs)),
    rw [set.range_comp, ← submodule.map_span],
    apply finite_dimensional.finrank_map_le },
  { apply (finrank_span_le_card _).trans,
    { classical, rw set.to_finset_range, exact finset.card_image_le },
    { apply set.fintype_range } },
end

[Junyan Xu]

To show it spans, it should be easy from linear independence + docs#span_eq_top_of_linear_independent_of_card_eq_finrank.

[Alex Kontorovich]

That's fantastic, thanks!