feat(linear_algebra/finite_dimensional): cardinalities and linear independence (#3056)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: jcommelin

src/linear_algebra/finite_dimensional.lean

@@ -182,7 +182,7 @@ end
 /-- If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
 `findim`. -/
 lemma findim_eq_card_basis' [finite_dimensional K V] {ι : Type w} {b : ι → V} (h : is_basis K b) :
-  (findim K V : cardinal.{w}) = cardinal.mk ι  :=
+  (findim K V : cardinal.{w}) = cardinal.mk ι :=
 begin
   rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
   letI: fintype s := s_finite.fintype,
@@ -196,6 +196,153 @@ begin
   exact (lift_inj.mp this).symm
 end
 
+-- Note here we've restrictied the universe levels of `ι` and `V` to be the same, for convenience.
+lemma cardinal_mk_le_findim_of_linear_independent
+  [finite_dimensional K V] {ι : Type v} {b : ι → V} (h : linear_independent K b) :
+  cardinal.mk ι ≤ findim K V :=
+begin
+  convert cardinal_le_dim_of_linear_independent h,
+  rw ←findim_eq_dim K V
+end
+
+-- Note here we've restrictied the universe levels of `ι` and `V` to be the same, for convenience.
+lemma fintype_card_le_findim_of_linear_independent
+  [finite_dimensional K V] {ι : Type v} [fintype ι] {b : ι → V} (h : linear_independent K b) :
+  fintype.card ι ≤ findim K V :=
+by simpa [fintype_card] using cardinal_mk_le_findim_of_linear_independent h
+
+lemma finset_card_le_findim_of_linear_independent [finite_dimensional K V] {b : finset V}
+  (h : linear_independent K (λ x, x : (↑b : set V) → V)) :
+  b.card ≤ findim K V :=
+begin
+  rw ←fintype.card_coe,
+  exact fintype_card_le_findim_of_linear_independent h,
+end
+
+section
+open_locale big_operators
+open finset
+
+/--
+If a finset has cardinality larger than the dimension of the space,
+then there is a nontrivial linear relation amongst its elements.
+-/
+lemma exists_nontrivial_relation_of_dim_lt_card
+  [finite_dimensional K V] {t : finset V} (h : findim K V < t.card) :
+  ∃ f : V → K, ∑ e in t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0 :=
+begin
+  have := mt finset_card_le_findim_of_linear_independent (by { simpa using h }),
+  rw linear_dependent_iff at this,
+  obtain ⟨s, g, sum, z, zm, nonzero⟩ := this,
+  -- Now we have to extend `g` to all of `t`, then to all of `V`.
+  let f : V → K := λ x, if h : x ∈ t then if (⟨x, h⟩ : (↑t : set V)) ∈ s then g ⟨x, h⟩ else 0 else 0,
+  -- and finally clean up the mess caused by the extension.
+  refine ⟨f, _, _⟩,
+  { dsimp [f],
+    rw ← sum,
+    fapply sum_bij_ne_zero (λ v hvt _, (⟨v, hvt⟩ : {v // v ∈ t})),
+    { intros v hvt H, dsimp,
+      rw [dif_pos hvt] at H,
+      contrapose! H,
+      rw [if_neg H, zero_smul], },
+    { intros _ _ _ _ _ _, exact subtype.mk.inj, },
+    { intros b hbs hb,
+      use b,
+      simpa only [hbs, exists_prop, dif_pos, mk_coe, and_true, if_true, finset.coe_mem,
+        eq_self_iff_true, exists_prop_of_true, ne.def] using hb, },
+    { intros a h₁, dsimp, rw [dif_pos h₁],
+      intro h₂, rw [if_pos], contrapose! h₂,
+      rw [if_neg h₂, zero_smul], }, },
+  { refine ⟨z, z.2, _⟩, dsimp only [f], erw [dif_pos z.2, if_pos]; rwa [subtype.coe_eta] },
+end
+
+/--
+If a finset has cardinality larger than `findim + 1`,
+then there is a nontrivial linear relation amongst its elements,
+such that the coefficients of the relation sum to zero.
+-/
+lemma exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card
+  [finite_dimensional K V] {t : finset V} (h : findim K V + 1 < t.card) :
+  ∃ f : V → K, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0 :=
+begin
+  -- Pick an element x₀ ∈ t,
+  have card_pos : 0 < t.card := lt_trans (nat.succ_pos _) h,
+  obtain ⟨x₀, m⟩ := (finset.card_pos.1 card_pos).bex,
+  -- and apply the previous lemma to the {xᵢ - x₀}
+  let shift : V ↪ V := ⟨λ x, x - x₀, add_left_injective (-x₀)⟩,
+  let t' := (t.erase x₀).map shift,
+  have h' : findim K V < t'.card,
+  { simp only [t', card_map, finset.card_erase_of_mem m],
+    exact nat.lt_pred_iff.mpr h, },
+  -- to obtain a function `g`.
+  obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_dim_lt_card h',
+  -- Then obtain `f` by translating back by `x₀`,
+  -- and setting the value of `f` at `x₀` to ensure `∑ e in t, f e = 0`.
+  let f : V → K := λ z, if z = x₀ then - ∑ z in (t.erase x₀), g (z - x₀) else g (z - x₀),
+  refine ⟨f, _ ,_ ,_⟩,
+  -- After this, it's a matter of verifiying the properties,
+  -- based on the corresponding properties for `g`.
+  { show ∑ (e : V) in t, f e • e = 0,
+    -- We prove this by splitting off the `x₀` term of the sum,
+    -- which is itself a sum over `t.erase x₀`,
+    -- combining the two sums, and
+    -- observing that after reindexing we have exactly
+    -- ∑ (x : V) in t', g x • x = 0.
+    simp only [f],
+    conv_lhs { apply_congr, skip, rw [ite_smul], },
+    rw [finset.sum_ite],
+    conv { congr, congr, apply_congr, simp [filter_eq', m], },
+    conv { congr, congr, skip, apply_congr, simp [filter_ne'], },
+    rw [sum_singleton, neg_smul, add_comm, ←sub_eq_add_neg, sum_smul, ←sum_sub_distrib],
+    simp only [←smul_sub],
+    -- At the end we have to reindex the sum, so we use `change` to
+    -- express the summand using `shift`.
+    change (∑ (x : V) in t.erase x₀, (λ e, g e • e) (shift x)) = 0,
+    rw ←sum_map _ shift,
+    exact gsum, },
+  { show ∑ (e : V) in t, f e = 0,
+    -- Again we split off the `x₀` term,
+    -- observing that it exactly cancels the other terms.
+    rw [← insert_erase m, sum_insert (not_mem_erase x₀ t)],
+    dsimp [f],
+    rw [if_pos rfl],
+    conv_lhs { congr, skip, apply_congr, skip, rw if_neg (show x ≠ x₀, from (mem_erase.mp H).1), },
+    exact neg_add_self _, },
+  { show ∃ (x : V) (H : x ∈ t), f x ≠ 0,
+    -- We can use x₁ + x₀.
+    refine ⟨x₁ + x₀, _, _⟩,
+    { rw finset.mem_map at x₁_mem,
+      rcases x₁_mem with ⟨x₁, x₁_mem, rfl⟩,
+      rw mem_erase at x₁_mem,
+      simp only [x₁_mem, sub_add_cancel, function.embedding.coe_fn_mk], },
+    { dsimp only [f],
+      rwa [if_neg, add_sub_cancel],
+      rw [add_left_eq_self], rintro rfl,
+      simpa only [sub_eq_zero, exists_prop, finset.mem_map, embedding.coe_fn_mk, eq_self_iff_true,
+        mem_erase, not_true, exists_eq_right, ne.def, false_and] using x₁_mem, } },
+end
+
+section
+variables {L : Type*} [discrete_linear_ordered_field L]
+variables {W : Type v} [add_comm_group W] [vector_space L W]
+
+/--
+A slight strengthening of `exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card`
+available when working over an ordered field:
+we can ensure a positive coefficient, not just a nonzero coefficient.
+-/
+lemma exists_relation_sum_zero_pos_coefficient_of_dim_succ_lt_card
+  [finite_dimensional L W] {t : finset W} (h : findim L W + 1 < t.card) :
+  ∃ f : W → L, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x ∈ t, 0 < f x :=
+begin
+  obtain ⟨f, sum, total, nonzero⟩ := exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card h,
+  exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩,
+end
+
+end
+
+end
+
 /-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
 whole space. -/
 lemma eq_top_of_findim_eq [finite_dimensional K V] {S : submodule K V}