feat(linear_algebra/affine_space/finite_dimensional): more lemmas (#4389

)

Add more lemmas concerning dimensions of affine spans of finite
families of points.  In particular, various forms of the lemma that `n + 1`
points are affinely independent if and only if their `vector_span` has
dimension `n` (or equivalently, at least `n`).  With suitable
definitions, this is equivalent to saying that three points are
affinely independent or collinear, four are affinely independent or
coplanar, etc., thus preparing for giving a definition of `collinear`
(for any set of points in an affine space for a vector space) in terms
of dimension and proving some basic properties of it including
relating it to affine independence.

src/linear_algebra/affine_space/basic.lean

@@ -941,6 +941,38 @@ lemma vector_span_range_eq_span_range_vsub_right (p : ι → P) (i0 : ι) :
   vector_span k (set.range p) = submodule.span k (set.range (λ (i : ι), p i -ᵥ p i0)) :=
 by rw [vector_span_eq_span_vsub_set_right k (set.mem_range_self i0), ←set.range_comp]
 
+/-- The `vector_span` of an indexed family is the span of the pairwise
+subtractions with a given point on the left, excluding the subtraction
+of that point from itself. -/
+lemma vector_span_range_eq_span_range_vsub_left_ne (p : ι → P) (i₀ : ι) :
+  vector_span k (set.range p) = submodule.span k (set.range (λ (i : {x // x ≠ i₀}), p i₀ -ᵥ p i)) :=
+begin
+  rw [←set.image_univ, vector_span_image_eq_span_vsub_set_left_ne k _ (set.mem_univ i₀)],
+  congr' with v,
+  simp only [set.mem_range, set.mem_image, set.mem_diff, set.mem_singleton_iff, subtype.exists,
+             subtype.coe_mk],
+  split,
+  { rintros ⟨x, ⟨i₁, ⟨⟨hi₁u, hi₁⟩, rfl⟩⟩, hv⟩,
+    exact ⟨i₁, hi₁, hv⟩ },
+  { exact λ ⟨i₁, hi₁, hv⟩, ⟨p i₁, ⟨i₁, ⟨set.mem_univ _, hi₁⟩, rfl⟩, hv⟩ }
+end
+
+/-- The `vector_span` of an indexed family is the span of the pairwise
+subtractions with a given point on the right, excluding the subtraction
+of that point from itself. -/
+lemma vector_span_range_eq_span_range_vsub_right_ne (p : ι → P) (i₀ : ι) :
+  vector_span k (set.range p) = submodule.span k (set.range (λ (i : {x // x ≠ i₀}), p i -ᵥ p i₀)) :=
+begin
+  rw [←set.image_univ, vector_span_image_eq_span_vsub_set_right_ne k _ (set.mem_univ i₀)],
+  congr' with v,
+  simp only [set.mem_range, set.mem_image, set.mem_diff, set.mem_singleton_iff, subtype.exists,
+             subtype.coe_mk],
+  split,
+  { rintros ⟨x, ⟨i₁, ⟨⟨hi₁u, hi₁⟩, rfl⟩⟩, hv⟩,
+    exact ⟨i₁, hi₁, hv⟩ },
+  { exact λ ⟨i₁, hi₁, hv⟩, ⟨p i₁, ⟨i₁, ⟨set.mem_univ _, hi₁⟩, rfl⟩, hv⟩ }
+end
+
 /-- The affine span of a set is nonempty if and only if that set
 is. -/
 lemma affine_span_nonempty (s : set P) :

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -172,4 +172,86 @@ begin
   exact affine_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one hi le_top hc
 end
 
+variables (k)
+
+/-- The `vector_span` of `n + 1` points in an indexed family has
+dimension at most `n`. -/
+lemma findim_vector_span_image_finset_le (p : ι → P) (s : finset ι) {n : ℕ}
+  (hc : finset.card s = n + 1) : findim k (vector_span k (p '' ↑s)) ≤ n :=
+begin
+  have hn : (p '' ↑s).nonempty,
+  { simp [hc, ←finset.card_pos] },
+  rcases hn with ⟨p₁, hp₁⟩,
+  rw [vector_span_eq_span_vsub_set_right_ne k hp₁],
+  have hfp₁ : (p '' ↑s \ {p₁}).finite :=
+    ((finset.finite_to_set _).image _).subset (set.diff_subset _ _),
+  haveI := hfp₁.fintype,
+  have hf : ((λ p, p -ᵥ p₁) '' (p '' ↑s \ {p₁})).finite := hfp₁.image _,
+  haveI := hf.fintype,
+  convert le_trans (findim_span_le_card ((λ p, p -ᵥ p₁) '' (p '' ↑s \ {p₁}))) _,
+  have hm : p₁ ∉ p '' ↑s \ {p₁}, by simp,
+  haveI := set.fintype_insert' (p '' ↑s \ {p₁}) hm,
+  rw [set.to_finset_card, set.card_image_of_injective (p '' ↑s \ {p₁}) (vsub_left_injective p₁),
+      ←add_le_add_iff_right 1, ←set.card_fintype_insert' _ hm],
+  have h : fintype.card (↑(s.image p) : set P) ≤ n + 1,
+  { rw [fintype.card_coe, ←hc],
+    exact finset.card_image_le },
+  convert h,
+  simp [hp₁]
+end
+
+/-- The `vector_span` of an indexed family of `n + 1` points has
+dimension at most `n`. -/
+lemma findim_vector_span_range_le [fintype ι] (p : ι → P) {n : ℕ}
+  (hc : fintype.card ι = n + 1) : findim k (vector_span k (set.range p)) ≤ n :=
+begin
+  rw [←set.image_univ, ←finset.coe_univ],
+  rw ←finset.card_univ at hc,
+  exact findim_vector_span_image_finset_le _ _ _ hc
+end
+
+/-- `n + 1` points are affinely independent if and only if their
+`vector_span` has dimension `n`. -/
+lemma affine_independent_iff_findim_vector_span_eq [fintype ι] (p : ι → P) {n : ℕ}
+  (hc : fintype.card ι = n + 1) :
+  affine_independent k p ↔ findim k (vector_span k (set.range p)) = n :=
+begin
+  have hn : nonempty ι, by simp [←fintype.card_pos_iff, hc],
+  cases hn with i₁,
+  rw [affine_independent_iff_linear_independent_vsub _ _ i₁,
+      linear_independent_iff_card_eq_findim_span, eq_comm,
+      vector_span_range_eq_span_range_vsub_right_ne k p i₁],
+  congr',
+  rw ←finset.card_univ at hc,
+  rw fintype.subtype_card,
+  simp [finset.filter_ne', finset.card_erase_of_mem, hc]
+end
+
+/-- `n + 1` points are affinely independent if and only if their
+`vector_span` has dimension at least `n`. -/
+lemma affine_independent_iff_le_findim_vector_span [fintype ι] (p : ι → P) {n : ℕ}
+  (hc : fintype.card ι = n + 1) :
+  affine_independent k p ↔ n ≤ findim k (vector_span k (set.range p)) :=
+begin
+  rw affine_independent_iff_findim_vector_span_eq k p hc,
+  split,
+  { rintro rfl,
+    refl },
+  { exact λ hle, le_antisymm (findim_vector_span_range_le k p hc) hle }
+end
+
+/-- `n + 2` points are affinely independent if and only if their
+`vector_span` does not have dimension at most `n`. -/
+lemma affine_independent_iff_not_findim_vector_span_le [fintype ι] (p : ι → P) {n : ℕ}
+  (hc : fintype.card ι = n + 2) :
+  affine_independent k p ↔ ¬ findim k (vector_span k (set.range p)) ≤ n :=
+by rw [affine_independent_iff_le_findim_vector_span k p hc, ←nat.lt_iff_add_one_le, lt_iff_not_ge]
+
+/-- `n + 2` points have a `vector_span` with dimension at most `n` if
+and only if they are not affinely independent. -/
+lemma findim_vector_span_le_iff_not_affine_independent [fintype ι] (p : ι → P) {n : ℕ}
+  (hc : fintype.card ι = n + 2) :
+  findim k (vector_span k (set.range p)) ≤ n ↔ ¬ affine_independent k p :=
+(not_iff_comm.1 (affine_independent_iff_not_findim_vector_span_le k p hc).symm).symm
+
 end affine_space'