subfamilies are linearly independent

Stream: Is there code for X?

[Michael Stoll]

I'm trying to prove some results in linear algebra (see this discussion), and I am having problems dealing with the API successfully. Right now, I am a bit stuck on this simple fact:

import linear_algebra.linear_independent

variables {F V ι : Type*} [field F] [add_comm_group V] [module F V]

lemma linear_idependent.subfamily {I J : set ι} (hJI : J ⊆ I) (v : ι → V)
  (hI : linear_independent F (I.restrict v)) : linear_independent F (J.restrict v) := sorry

This looks like it should be simple (or even in the library), but so far I don't really see how to do it without tying myself in knots. Any suggestions?

[Reid Barton]

I would try starting with docs#inear_independent.comp

[Michael Stoll]

That's the conclusion I just reached myself:

lemma linear_idependent.subfamily {I J : set ι} (hJI : J ⊆ I) (v : ι → V)
  (hI : linear_independent F (I.restrict v)) : linear_independent F (J.restrict v) :=
begin
  rw (show J.restrict v = (I.restrict v) ∘ (set.inclusion hJI), from by {ext, simp}),
  exact linear_independent.comp hI _ (set.inclusion_injective hJI),
end

Still, I'd expect this to be in mathlib...

[Eric Wieser]

Does the proof still work without the first tactic line?

[Xavier Roblot]

Did you try to use docs#linear_independent.mono?

[Eric Wieser]

docs#linear_independent.restrict_of_comp_subtype looks helpful too

[Eric Wieser]

Xavier Roblot said:

Did you try to use docs#linear_independent.mono?

Maybe this lemma should be generalized to take a v : ι → V, with the current spelling being v = id

[Michael Stoll]

Eric Wieser said:

Does the proof still work without the first tactic line?

No:

type mismatch at application
  hI.comp
term
  hI
has type
  linear_independent F (I.restrict v)
but is expected to have type
  linear_independent F v

(I think I tried that first...)

[Michael Stoll]

Xavier Roblot said:

Did you try to use docs#linear_independent.mono?

Then you first have to convert to the identity family on the images. I don't think this will be simpler.
(See @Eric Wieser's remark.)

[Michael Stoll]

Eric Wieser said:

docs#linear_independent.restrict_of_comp_subtype looks helpful too

  refine linear_independent.restrict_of_comp_subtype _,

leads to the goal linear_independent F (v ∘ (coe :↥J → ι)). I think the problem here is that set.inclusion hJI is not a coercion, so you cannot directly use linear_independent.restrict_of_comp_subtype (you'd have to replace ι by ↥I to be able to make use of the assumption).

[Michael Stoll]

Now for the next level:

lemma linear_independent.quotient₁ {I J : set ι} (hIJ : disjoint I J) {v : ι → V}
  (hv : linear_independent F ((I ∪ J).restrict v)) :
  linear_independent F (J.restrict ((mkq (span F (v '' I))) ∘ v)) :=

I guess the way to go is to use linear_independent.map and linear_independent.disjoint_span_image. But to get there was not so easy...
The best I have come up with is the following:

import linear_algebra.linear_independent
import linear_algebra.quotient

namespace set

lemma restrict_image_union_left {α β} (s t : set α) (f : α → β) :
  f '' s = ((s ∪ t).restrict f) '' ((inclusion (subset_union_left s t)) '' univ) :=
begin
  ext,
  simp only [mem_image, restrict_apply, mem_univ, true_and, set_coe.exists, inclusion_mk,
             mem_union, subtype.mk_eq_mk, exists_prop, exists_eq_right, subtype.coe_mk],
  exact ⟨Exists.imp (λ a, by tauto), Exists.imp (λ a, by tauto)⟩,
end

lemma restrict_image_union_right {α β} (s t : set α) (f : α → β) :
  f '' t = ((s ∪ t).restrict f) '' ((inclusion (subset_union_right s t)) '' univ) :=
begin
  ext,
  simp only [mem_image, restrict_apply, mem_univ, true_and, set_coe.exists, inclusion_mk,
             mem_union, subtype.mk_eq_mk, exists_prop, exists_eq_right, subtype.coe_mk],
  exact ⟨Exists.imp (λ a, by tauto), Exists.imp (λ a, by tauto)⟩,
end

end set

variables {F V ι : Type*} [field F] [add_comm_group V] [module F V]

open submodule set

lemma linear_independent.subfamily {I J : set ι} (hJI : J ⊆ I) {v : ι → V}
  (hI : linear_independent F (I.restrict v)) : linear_independent F (J.restrict v) :=
begin
  rw (show J.restrict v = (I.restrict v) ∘ (inclusion hJI), from by {ext, simp}),
  exact linear_independent.comp hI _ (inclusion_injective hJI),
end

lemma linear_independent.quotient₁ {I J : set ι} (hIJ : disjoint I J) {v : ι → V}
  (hv : linear_independent F ((I ∪ J).restrict v)) :
  linear_independent F (J.restrict ((mkq (span F (v '' I))) ∘ v)) :=
begin
  rw (show J.restrict (mkq (span F (v '' I)) ∘ v) = mkq (span F (v '' I)) ∘ (J.restrict v),
      from by {ext, simp}),
  refine linear_independent.map (linear_independent.subfamily (subset_union_right I J) hv) _,
  simp only [range_restrict, ker_mkq, restrict_image_union_left I J v,
             restrict_image_union_right I J v],
  refine linear_independent.disjoint_span_image hv (set.disjoint_iff.mpr (λ i hi, _)),
  simp only [mem_inter_iff, mem_image, mem_univ, true_and, set_coe.exists, inclusion_mk] at hi,
  obtain ⟨⟨x₁, hx₁J, hx₁⟩, ⟨x₂, hx₂I, hx₂⟩⟩ := hi,
  rw [← hx₁, subtype.mk_eq_mk] at hx₂,
  exact disjoint.ne_of_mem hIJ hx₂I hx₁J hx₂,
end

But I'm not exactly happy with it (in particular with the need for the set lemmas). Can this be improved?

[Anne Baanen]

I think this should be doable with docs#linear_independent.map and docs#linear_independent.disjoint_span_image, but the last one requires linear_independent F v instead of linear_independent F ((I ∪ J).restrict v). Let me see if I can weaken the hypothesis sufficiently...

[Anne Baanen]

import linear_algebra.linear_independent
import linear_algebra.quotient

variables {F V ι : Type*} [field F] [add_comm_group V] [module F V]

open submodule set

lemma linear_independent.subfamily {I J : set ι} (hJI : J ⊆ I) {v : ι → V}
  (hI : linear_independent F (I.restrict v)) : linear_independent F (J.restrict v) :=
begin
  rw (show J.restrict v = (I.restrict v) ∘ (inclusion hJI), from by {ext, simp}),
  exact linear_independent.comp hI _ (inclusion_injective hJI),
end

lemma linear_independent.disjoint_span_image' {ι R M : Type*} {v : ι → M} {I J : set ι}
  [ring R] [add_comm_group M] [module R M] (hv : linear_independent R ((I ∪ J).restrict v)) (hs : disjoint I J) :
  disjoint (submodule.span R (v '' I)) (submodule.span R (v '' J)) :=
begin
  set I' : set (coe_sort (I ∪ J)) := (coe ⁻¹' I) with I'_def,
  set J' : set (coe_sort (I ∪ J)) := (coe ⁻¹' J) with J'_def,
  have : disjoint I' J',
  { rw [set.disjoint_iff, I'_def, J'_def] at *,
    rintros ⟨x, (hxI | hxJ)⟩ hx;
      exact hs hx },
  convert linear_independent.disjoint_span_image hv this using 2,
  { ext, rw [I'_def, set.image_restrict, set.inter_comm, set.union_inter_cancel_left] },
  { ext, rw [J'_def, set.image_restrict, set.inter_comm, set.union_inter_cancel_right] }
end


lemma linear_independent.quotient₁ {I J : set ι} (hIJ : disjoint I J) {v : ι → V}
  (hv : linear_independent F ((I ∪ J).restrict v)) :
  linear_independent F (J.restrict ((mkq (span F (v '' I))) ∘ v)) :=
begin
  refine linear_independent.map (linear_independent.subfamily (set.subset_union_right I J) hv) _,
  rw [submodule.ker_mkq],
  convert (linear_independent.disjoint_span_image' hv hIJ).symm,
  ext,
  simp
end

[Michael Stoll]

Thanks; that looks a bit better (even though it is built from the same building blocks).

[Michael Stoll]

Next level: After defining

variables (R : Type*) {M ι : Type*} [semiring R] [add_comm_monoid M] [module R M]

def linear_independent_on (v : ι → M) (s : set ι) : Prop := linear_independent R (s.restrict v)

I want to show

variables {R M ι : Type*} [ring R] [add_comm_group M] [module R M]

lemma linear_independent_on.union {s t : set ι} {v : ι → M} (hs : linear_independent_on R v s)
  (ht : linear_independent_on R v t)
  (h : disjoint (submodule.span R (v '' s)) (submodule.span R (v '' t))) :
  linear_independent_on R v (s ∪ t) := sorry

I have come up with the following proof, which needs some extra stuff connected to sets and sum types.

import linear_algebra.linear_independent
import linear_algebra.quotient

namespace set

def union_to_sum {α} (s t : set α) [decidable_pred (λ x, x ∈ s)] : (s ∪ t) → sum s t :=
    λ x, if hx : x.val ∈ s then sum.inl ⟨x.val, hx⟩
                           else sum.inr ⟨x.val, x.property.resolve_left hx⟩

lemma union_to_sum_inj {α} (s t : set α) [decidable_pred (λ x, x ∈ s)] :
  function.injective (union_to_sum s t) :=
begin
  intros x y hf,
  simp only [union_to_sum, subtype.val_eq_coe] at hf,
  by_cases hx : ↑x ∈ s; by_cases hy : ↑y ∈ s;
    simp only [hx, hy, not_false_iff, dif_neg, dif_pos, subtype.mk_eq_mk] at hf,
  { exact subtype.ext hf, },
  { exact false.elim hf, },
  { exact false.elim hf, },
  { exact subtype.ext hf, }
end

end set

section linear_indep

variables {R M ι : Type*} [ring R] [add_comm_group M] [module R M]

variables (R)
def linear_independent_on (v : ι → M) (s : set ι) : Prop := linear_independent R (s.restrict v)

variables {R}

open set submodule

lemma linear_independent_on.union {s t : set ι} {v : ι → M} (hs : linear_independent_on R v s)
  (ht : linear_independent_on R v t)
  (h : disjoint (submodule.span R (v '' s)) (submodule.span R (v '' t))) :
  linear_independent_on R v (s ∪ t) :=
begin
  simp_rw ← range_restrict at h,
  dsimp [linear_independent_on],
  classical,
  convert linear_independent.comp (linear_independent.sum_type hs ht h)
            (union_to_sum s t) (union_to_sum_inj s t),
  { ext x,
    simp only [union_to_sum, subtype.val_eq_coe, restrict_apply, function.comp_app],
    split_ifs with hx hx,
    { simp only [sum.elim_inl, restrict_apply, subtype.coe_mk], },
    { simp only [sum.elim_inr, restrict_apply, subtype.coe_mk], } },
end

end linear_indep

and I'm wondering again whether there might be a simpler way.

[Michael Stoll]

I need the fact that a family f : ι → M is linearly independent if and only if s.card ≤ finrank R (span R (s.image f : set M)) for all s : finset ι (where M is a vector space over R), but I can't find it in mathlib.

There is docs#linear_independent_iff_card_le_finrank_span, which is sort of half of what I need, but there does not seem to be an obvious way to connect this easily with linear independence on an arbitrary type. What I have come up with so far is the following.

import tactic
import algebra.module.basic
import linear_algebra.finrank
import linear_algebra.finite_dimensional

namespace linear_independent

open finite_dimensional submodule

variables (R : Type*) [division_ring R]
variables (M : Type*) [add_comm_group M] [decidable_eq M] [module R M]
variables {ι : Type*} [decidable_eq ι]

lemma iff_card_le_rank_span_on_finsets (f : ι → M) :
  linear_independent R f ↔ ∀ s : finset ι, s.card ≤ finrank R (span R (s.image f : set M)) :=
begin
  have h : ∀ s : finset ι, (finset.image f s : set M) = set.range (f ∘ (coe : s → ι)),
  { intro s,
    ext,
    simp only [finset.coe_image, set.mem_image, finset.mem_coe, set.mem_range,
               function.comp_app, finset.exists_coe, subtype.coe_mk, exists_prop], },
  refine ⟨λ H s, _, λ H, _⟩,
  { have H₁ := comp H (coe : s → ι) subtype.coe_injective,
    convert linear_independent_iff_card_le_finrank_span.mp H₁ using 1,
    { exact (fintype.card_coe s).symm, },
    { simp only [set.finrank],
      rw h, } },
  { rw linear_independent_iff',
    refine λ s g hg i hi, _,
    rw ← finset.sum_finset_coe at hg,
    specialize H s,
    rw [← fintype.card_coe, h] at H,
    replace H := fintype.linear_independent_iff.mp
                   (linear_independent_iff_card_le_finrank_span.mpr H) (g ∘ coe) hg ⟨i, hi⟩,
    exact H, }
end

Is there a better way?
(BTW, exact fintype.linear_independent_iff.mp ... does not work; it wants a fintype ι instance...)