feat(linear_algebra/affine_space): more lemmas (#3990)

Add another batch of lemmas about affine spaces.  These lemmas mostly
relate to manipulating centroids and the relations between centroids
of points given by different subsets of the index type.

src/linear_algebra/affine_space/combination.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Joseph Myers.
 -/
+import algebra.invertible
 import data.indicator_function
 import linear_algebra.affine_space.basic
 import linear_algebra.finsupp
@@ -47,6 +48,7 @@ variables [S : affine_space V P]
 include S
 
 variables {ι : Type*} (s : finset ι)
+variables {ι₂ : Type*} (s₂ : finset ι₂)
 
 /-- A weighted sum of the results of subtracting a base point from the
 given points, as a linear map on the weights.  The main cases of
@@ -127,6 +129,16 @@ begin
   exact set.sum_indicator_subset_of_eq_zero w (λ i wi, wi • (p i -ᵥ b : V)) h (λ i, zero_smul k _)
 end
 
+/-- A weighted sum, over the image of an embedding, equals a weighted
+sum with the same points and weights over the original
+`finset`. -/
+lemma weighted_vsub_of_point_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P) :
+  (s₂.map e).weighted_vsub_of_point p b w = s₂.weighted_vsub_of_point (p ∘ e) b (w ∘ e) :=
+begin
+  simp_rw [weighted_vsub_of_point_apply],
+  exact finset.sum_map _ _ _
+end
+
 /-- A weighted sum of the results of subtracting a default base point
 from the given points, as a linear map on the weights.  This is
 intended to be used when the sum of the weights is 0; that condition
@@ -161,6 +173,13 @@ lemma weighted_vsub_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ :
   s₁.weighted_vsub p w = s₂.weighted_vsub p (set.indicator ↑s₁ w) :=
 weighted_vsub_of_point_indicator_subset _ _ _ h
 
+/-- A weighted subtraction, over the image of an embedding, equals a
+weighted subtraction with the same points and weights over the
+original `finset`. -/
+lemma weighted_vsub_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
+  (s₂.map e).weighted_vsub p w = s₂.weighted_vsub (p ∘ e) (w ∘ e) :=
+s₂.weighted_vsub_of_point_map _ _ _ _
+
 /-- A weighted sum of the results of subtracting a default base point
 from the given points, added to that base point, as an affine map on
 the weights.  This is intended to be used when the sum of the weights
@@ -233,6 +252,13 @@ lemma affine_combination_indicator_subset (w : ι → k) (p : ι → P) {s₁ s
 by rw [affine_combination_apply, affine_combination_apply,
        weighted_vsub_of_point_indicator_subset _ _ _ h]
 
+/-- An affine combination, over the image of an embedding, equals an
+affine combination with the same points and weights over the original
+`finset`. -/
+lemma affine_combination_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
+  (s₂.map e).affine_combination p w = s₂.affine_combination (p ∘ e) (w ∘ e) :=
+by simp_rw [affine_combination_apply, weighted_vsub_of_point_map]
+
 variables {V}
 
 /-- Suppose an indexed family of points is given, along with a subset
@@ -299,7 +325,7 @@ end finset
 namespace finset
 
 variables (k : Type*) {V : Type*} {P : Type*} [division_ring k] [add_comm_group V] [module k V]
-variables [affine_space V P] {ι : Type*} (s : finset ι)
+variables [affine_space V P] {ι : Type*} (s : finset ι) {ι₂ : Type*} (s₂ : finset ι₂)
 
 /-- The weights for the centroid of some points. -/
 def centroid_weights : ι → k := function.const ι (card s : k) ⁻¹
@@ -359,6 +385,94 @@ rfl
   ({i} : finset ι).centroid k p = p i :=
 by simp [centroid_def, affine_combination_apply]
 
+/-- The centroid of two points, expressed directly as adding a vector
+to a point. -/
+lemma centroid_insert_singleton [invertible (2 : k)] (p : ι → P) (i₁ i₂ : ι) :
+  ({i₁, i₂} : finset ι).centroid k p = (2 ⁻¹ : k) • (p i₂ -ᵥ p i₁) +ᵥ p i₁ :=
+begin
+  by_cases h : i₁ = i₂,
+  { simp [h] },
+  { have hc : (card ({i₁, i₂} : finset ι) : k) ≠ 0,
+    { rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton],
+      norm_num,
+      exact nonzero_of_invertible _ },
+    rw [centroid_def,
+        affine_combination_eq_weighted_vsub_of_point_vadd_of_sum_eq_one _ _ _
+          (sum_centroid_weights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)],
+    simp [h],
+    norm_num }
+end
+
+/-- The centroid of two points indexed by `fin 2`, expressed directly
+as adding a vector to the first point. -/
+lemma centroid_insert_singleton_fin [invertible (2 : k)] (p : fin 2 → P) :
+  univ.centroid k p = (2 ⁻¹ : k) • (p 1 -ᵥ p 0) +ᵥ p 0 :=
+begin
+  have hu : (finset.univ : finset (fin 2)) = {0, 1}, by dec_trivial,
+  rw hu,
+  convert centroid_insert_singleton k p 0 1
+end
+
+/-- A centroid, over the image of an embedding, equals a centroid with
+the same points and weights over the original `finset`. -/
+lemma centroid_map (e : ι₂ ↪ ι) (p : ι → P) : (s₂.map e).centroid k p = s₂.centroid k (p ∘ e) :=
+by simp [centroid_def, affine_combination_map, centroid_weights]
+
+omit V
+
+/-- `centroid_weights` gives the weights for the centroid as a
+constant function, which is suitable when summing over the points
+whose centroid is being taken.  This function gives the weights in a
+form suitable for summing over a larger set of points, as an indicator
+function that is zero outside the set whose centroid is being taken.
+In the case of a `fintype`, the sum may be over `univ`. -/
+def centroid_weights_indicator : ι → k := set.indicator ↑s (s.centroid_weights k)
+
+/-- The definition of `centroid_weights_indicator`. -/
+lemma centroid_weights_indicator_def :
+  s.centroid_weights_indicator k = set.indicator ↑s (s.centroid_weights k) :=
+rfl
+
+/-- The sum of the weights for the centroid indexed by a `fintype`. -/
+lemma sum_centroid_weights_indicator [fintype ι] :
+  ∑ i, s.centroid_weights_indicator k i = ∑ i in s, s.centroid_weights k i :=
+(set.sum_indicator_subset _ (subset_univ _)).symm
+
+/-- In the characteristic zero case, the weights in the centroid
+indexed by a `fintype` sum to 1 if the number of points is not
+zero. -/
+lemma sum_centroid_weights_indicator_eq_one_of_card_ne_zero [char_zero k] [fintype ι]
+  (h : card s ≠ 0) : ∑ i, s.centroid_weights_indicator k i = 1 :=
+begin
+  rw sum_centroid_weights_indicator,
+  exact s.sum_centroid_weights_eq_one_of_card_ne_zero k h
+end
+
+/-- In the characteristic zero case, the weights in the centroid
+indexed by a `fintype` sum to 1 if the set is nonempty. -/
+lemma sum_centroid_weights_indicator_eq_one_of_nonempty [char_zero k] [fintype ι]
+  (h : s.nonempty) : ∑ i, s.centroid_weights_indicator k i = 1 :=
+begin
+  rw sum_centroid_weights_indicator,
+  exact s.sum_centroid_weights_eq_one_of_nonempty k h
+end
+
+/-- In the characteristic zero case, the weights in the centroid
+indexed by a `fintype` sum to 1 if the number of points is `n + 1`. -/
+lemma sum_centroid_weights_indicator_eq_one_of_card_eq_add_one [char_zero k] [fintype ι] {n : ℕ}
+  (h : card s = n + 1) : ∑ i, s.centroid_weights_indicator k i = 1 :=
+begin
+  rw sum_centroid_weights_indicator,
+  exact s.sum_centroid_weights_eq_one_of_card_eq_add_one k h
+end
+
+include V
+
+/-- The centroid as an affine combination over a `fintype`. -/
+lemma centroid_eq_affine_combination_fintype [fintype ι] (p : ι → P) :
+  s.centroid k p = univ.affine_combination p (s.centroid_weights_indicator k) :=
+affine_combination_indicator_subset _ _ (subset_univ _)
+
 end finset
 
 section affine_space'

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -44,6 +44,12 @@ instance finite_dimensional_direction_affine_span_of_fintype [fintype ι] (p : 
   finite_dimensional k (affine_span k (set.range p)).direction :=
 finite_dimensional_direction_affine_span_of_finite k (set.finite_range _)
 
+/-- The direction of the affine span of a subset of a family indexed
+by a `fintype` is finite-dimensional. -/
+instance finite_dimensional_direction_affine_span_image_of_fintype [fintype ι] (p : ι → P)
+  (s : set ι) : finite_dimensional k (affine_span k (p '' s)).direction :=
+finite_dimensional_direction_affine_span_of_finite k ((set.finite.of_fintype _).image _)
+
 variables {k}
 
 /-- The `vector_span` of a finite affinely independent family has

src/linear_algebra/affine_space/independent.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Joseph Myers.
 -/
 import data.finset.sort
+import data.matrix.notation
 import linear_algebra.affine_space.combination
 import linear_algebra.basis
 
@@ -219,7 +220,8 @@ begin
   { rw [←hw, finset.sum_map],
     simp [hw'] },
   have hs' : fs'.weighted_vsub p w' = (0:V),
-  { rw [←hs, finset.weighted_vsub_apply, finset.weighted_vsub_apply, finset.sum_map],
+  { rw [←hs, finset.weighted_vsub_map],
+    congr' with i,
     simp [hw'] },
   rw [←ha fs' w' hw's hs' (f i0) ((finset.mem_map' _).2 hi0), hw']
 end
@@ -310,7 +312,7 @@ 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]
+variables [affine_space V P] {ι : Type*}
 include V
 
 /-- An affinely independent set of points can be extended to such a
@@ -343,6 +345,27 @@ begin
     { use [hsvi, affine_span_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt] } }
 end
 
+variables (k)
+
+/-- Two different points are affinely independent. -/
+lemma affine_independent_of_ne {p₁ p₂ : P} (h : p₁ ≠ p₂) : affine_independent k ![p₁, p₂] :=
+begin
+  rw affine_independent_iff_linear_independent_vsub k ![p₁, p₂] 0,
+  let i₁ : {x // x ≠ (0 : fin 2)} := ⟨1, dec_trivial⟩,
+  have he' : ∀ i, i = i₁,
+  { rintro ⟨i, hi⟩,
+    ext,
+    fin_cases i,
+    { simpa using hi } },
+  haveI : unique {x // x ≠ (0 : fin 2)} := ⟨⟨i₁⟩, he'⟩,
+  have hz : (![p₁, p₂] ↑(default {x // x ≠ (0 : fin 2)}) -ᵥ ![p₁, p₂] 0 : V) ≠ 0,
+  { rw he' (default _),
+    intro he,
+    rw vsub_eq_zero_iff_eq at he,
+    exact h he.symm },
+  exact linear_independent_unique hz
+end
+
 end field
 
 namespace affine
@@ -413,6 +436,80 @@ rfl
   s.face (finset.card_singleton i) = mk_of_point k (s.points i) :=
 by { ext, simp [face_points] }
 
+/-- The set of points of a face. -/
+@[simp] lemma range_face_points {n : ℕ} (s : simplex k P n) {fs : finset (fin (n + 1))}
+  {m : ℕ} (h : fs.card = m + 1) : set.range (s.face h).points = s.points '' ↑fs :=
+begin
+  rw [face, set.range_comp],
+  simp
+end
+
 end simplex
 
 end affine
+
+namespace affine
+namespace simplex
+
+variables {k : Type*} {V : Type*} {P : Type*} [division_ring k]
+          [add_comm_group V] [module k V] [affine_space V P]
+include V
+
+/-- The centroid of a face of a simplex as the centroid of a subset of
+the points. -/
+@[simp] lemma face_centroid_eq_centroid {n : ℕ} (s : simplex k P n) {fs : finset (fin (n + 1))}
+  {m : ℕ} (h : fs.card = m + 1) :
+  finset.univ.centroid k (s.face h).points = fs.centroid k s.points :=
+begin
+  convert (finset.univ.centroid_map k ⟨fs.mono_of_fin h, fs.mono_of_fin_injective h⟩ s.points).symm,
+  rw [←finset.coe_inj, finset.coe_map, function.embedding.coe_fn_mk],
+  simp
+end
+
+/-- Over a characteristic-zero division ring, the centroids given by
+two subsets of the points of a simplex are equal if and only if those
+faces are given by the same subset of points. -/
+@[simp] lemma centroid_eq_iff [char_zero k] {n : ℕ} (s : simplex k P n)
+  {fs₁ fs₂ : finset (fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) :
+  fs₁.centroid k s.points = fs₂.centroid k s.points ↔ fs₁ = fs₂ :=
+begin
+  split,
+  { intro h,
+    rw [finset.centroid_eq_affine_combination_fintype,
+        finset.centroid_eq_affine_combination_fintype] at h,
+    have ha := (affine_independent_iff_indicator_eq_of_affine_combination_eq k s.points).1
+      s.independent _ _ _ _ (fs₁.sum_centroid_weights_indicator_eq_one_of_card_eq_add_one k h₁)
+      (fs₂.sum_centroid_weights_indicator_eq_one_of_card_eq_add_one k h₂) h,
+    simp_rw [finset.coe_univ, set.indicator_univ, function.funext_iff,
+             finset.centroid_weights_indicator_def, finset.centroid_weights, h₁, h₂] at ha,
+    ext i,
+    replace ha := ha i,
+    split,
+    all_goals
+    { intro hi,
+      by_contradiction hni,
+      simp [hi, hni] at ha,
+      norm_cast at ha } },
+  { intro h,
+    have hm : m₁ = m₂,
+    { subst h,
+      simpa [h₁] using h₂ },
+    subst hm,
+    congr,
+    exact h }
+end
+
+/-- Over a characteristic-zero division ring, the centroids of two
+faces of a simplex are equal if and only if those faces are given by
+the same subset of points. -/
+lemma face_centroid_eq_iff [char_zero k] {n : ℕ} (s : simplex k P n)
+  {fs₁ fs₂ : finset (fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) :
+  finset.univ.centroid k (s.face h₁).points = finset.univ.centroid k (s.face h₂).points ↔
+    fs₁ = fs₂ :=
+begin
+  rw [face_centroid_eq_centroid, face_centroid_eq_centroid],
+  exact s.centroid_eq_iff h₁ h₂
+end
+
+end simplex
+end affine