feat(linear_algebra/affine_space/independent): affinely independent s…

…ets (#3794)

Prove variants of `affine_independent_iff_linear_independent_vsub`
that relate affine independence for a set of points (as opposed to an
indexed family of points) to linear independence for a set of vectors,
so facilitating linking to results such as `exists_subset_is_basis`
expressed in terms of linearly independent sets of vectors.  There are
two variants, depending on which of the set of points or the set of
vectors is given as a hypothesis.

Thus, applying `exists_subset_is_basis`, deduce that if `k` is a
field, any affinely independent set of points can be extended to such
a set that spans the whole space.

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear.20suffering

src/linear_algebra/affine_space/basic.lean

@@ -846,6 +846,27 @@ lemma affine_span_nonempty (s : set P) :
   (affine_span k s : set P).nonempty ↔ s.nonempty :=
 span_points_nonempty k s
 
+variables {k}
+
+/-- Suppose a set of vectors spans `V`.  Then a point `p`, together
+with those vectors added to `p`, spans `P`. -/
+lemma affine_span_singleton_union_vadd_eq_top_of_span_eq_top {s : set V} (p : P)
+    (h : submodule.span k (set.range (coe : s → V)) = ⊤) :
+  affine_span k ({p} ∪ (λ v, v +ᵥ p) '' s) = ⊤ :=
+begin
+  convert affine_subspace.ext_of_direction_eq _
+    ⟨p,
+     mem_affine_span k (set.mem_union_left _ (set.mem_singleton _)),
+     affine_subspace.mem_top k V p⟩,
+  rw [direction_affine_span, affine_subspace.direction_top,
+      vector_span_eq_span_vsub_set_right k
+        ((set.mem_union_left _ (set.mem_singleton _)) : p ∈ _), eq_top_iff, ←h],
+  apply submodule.span_mono,
+  rintros v ⟨v', rfl⟩,
+  use (v' : V) +ᵥ p,
+  simp
+end
+
 end affine_space'
 
 namespace affine_subspace

src/linear_algebra/affine_space/independent.lean

@@ -102,6 +102,48 @@ begin
     exact finset.eq_zero_of_sum_eq_zero hw h2b i hi }
 end
 
+/-- A set is affinely independent if and only if the differences from
+a base point in that set are linearly independent. -/
+lemma affine_independent_set_iff_linear_independent_vsub {s : set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
+  affine_independent k (λ p, p : s → P) ↔
+  linear_independent k (λ v, v : (λ p, (p -ᵥ p₁ : V)) '' (s \ {p₁}) → V) :=
+begin
+  rw affine_independent_iff_linear_independent_vsub k (λ p, p : s → P) ⟨p₁, hp₁⟩,
+  split,
+  { intro h,
+    have hv : ∀ v : (λ p, (p -ᵥ p₁ : V)) '' (s \ {p₁}), (v : V) +ᵥ p₁ ∈ s \ {p₁} :=
+      λ v, (set.mem_image_of_injective (vsub_left_injective p₁)).1
+             ((vadd_vsub (v : V) p₁).symm ▸ v.property),
+    let f : (λ p : P, (p -ᵥ p₁ : V)) '' (s \ {p₁}) → {x : s // x ≠ ⟨p₁, hp₁⟩} :=
+      λ x, ⟨⟨(x : V) +ᵥ p₁, set.mem_of_mem_diff (hv x)⟩,
+            λ hx, set.not_mem_of_mem_diff (hv x) (subtype.ext_iff.1 hx)⟩,
+    convert h.comp f
+      (λ x1 x2 hx, (subtype.ext (vadd_right_cancel p₁ (subtype.ext_iff.1 (subtype.ext_iff.1 hx))))),
+    ext v,
+    exact (vadd_vsub (v : V) p₁).symm },
+  { intro h,
+    let f : {x : s // x ≠ ⟨p₁, hp₁⟩} → (λ p : P, (p -ᵥ p₁ : V)) '' (s \ {p₁}) :=
+      λ x, ⟨((x : s) : P) -ᵥ p₁, ⟨x, ⟨⟨(x : s).property, λ hx, x.property (subtype.ext hx)⟩, rfl⟩⟩⟩,
+    convert h.comp f
+      (λ x1 x2 hx, subtype.ext (subtype.ext (vsub_left_cancel (subtype.ext_iff.1 hx)))) }
+end
+
+/-- A set of nonzero vectors is linearly independent if and only if,
+given a point `p₁`, the vectors added to `p₁` and `p₁` itself are
+affinely independent. -/
+lemma linear_independent_set_iff_affine_independent_vadd_union_singleton {s : set V}
+  (hs : ∀ v ∈ s, v ≠ (0 : V)) (p₁ : P) : linear_independent k (λ v, v : s → V) ↔
+  affine_independent k (λ p, p : {p₁} ∪ ((λ v, v +ᵥ p₁) '' s) → P) :=
+begin
+  rw affine_independent_set_iff_linear_independent_vsub k
+    (set.mem_union_left _ (set.mem_singleton p₁)),
+  have h : (λ p, (p -ᵥ p₁ : V)) '' (({p₁} ∪ (λ v, v +ᵥ p₁) '' s) \ {p₁}) = s,
+  { simp_rw [set.union_diff_left, set.image_diff (vsub_left_injective p₁), set.image_image,
+             set.image_singleton, vsub_self, vadd_vsub, set.image_id'],
+    exact set.diff_singleton_eq_self (λ h, hs 0 h rfl) },
+  rw h
+end
+
 /-- A family is affinely independent if and only if any affine
 combinations (with sum of weights 1) that evaluate to the same point
 have equal `set.indicator`. -/
@@ -239,6 +281,44 @@ by simp [ha]
 
 end affine_independent
 
+section field
+
+variables {k : Type*} {V : Type*} {P : Type*} [field k] [add_comm_group V] [module k V]
+variables [affine_space V P]
+include V
+
+/-- An affinely independent set of points can be extended to such a
+set that spans the whole space. -/
+lemma exists_subset_affine_independent_affine_span_eq_top {s : set P}
+  (h : affine_independent k (λ p, p : s → P)) :
+  ∃ t : set P, s ⊆ t ∧ affine_independent k (λ p, p : t → P) ∧ affine_span k t = ⊤ :=
+begin
+  rcases s.eq_empty_or_nonempty with rfl | ⟨p₁, hp₁⟩,
+  { have p₁ : P := add_torsor.nonempty.some,
+    rcases exists_is_basis k V with ⟨sv, hsvi, hsvt⟩,
+    have h0 : ∀ v : V, v ∈ sv → v ≠ 0,
+    { intros v hv,
+      change ((⟨v, hv⟩ : sv) : V) ≠ 0,
+      exact hsvi.ne_zero },
+    rw linear_independent_set_iff_affine_independent_vadd_union_singleton k h0 p₁ at hsvi,
+    use [{p₁} ∪ (λ v, v +ᵥ p₁) '' sv, set.empty_subset _, hsvi,
+         affine_span_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt] },
+  { rw affine_independent_set_iff_linear_independent_vsub k hp₁ at h,
+    rcases exists_subset_is_basis h with ⟨sv, hsv, hsvi, hsvt⟩,
+    have h0 : ∀ v : V, v ∈ sv → v ≠ 0,
+    { intros v hv,
+      change ((⟨v, hv⟩ : sv) : V) ≠ 0,
+      exact hsvi.ne_zero },
+    rw linear_independent_set_iff_affine_independent_vadd_union_singleton k h0 p₁ at hsvi,
+    use {p₁} ∪ (λ v, v +ᵥ p₁) '' sv,
+    split,
+    { refine set.subset.trans _ (set.union_subset_union_right _ (set.image_subset _ hsv)),
+      simp [set.image_image] },
+    { use [hsvi, affine_span_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt] } }
+end
+
+end field
+
 namespace affine
 
 variables (k : Type*) {V : Type*} (P : Type*) [ring k] [add_comm_group V] [module k V]