[Merged by Bors] - feat(linear_algebra/affine_space): more lemmas

src/linear_algebra/affine_space/basic.lean

@@ -111,6 +111,10 @@ def vector_span (s : set P) : submodule k V := submodule.span k (vsub_set s)
 lemma vector_span_def (s : set P) : vector_span k s = submodule.span k (vsub_set s) :=
 rfl
 
+/-- `vector_span` is monotone. -/
+lemma vector_span_mono {s₁ s₂ : set P} (h : s₁ ⊆ s₂) : vector_span k s₁ ≤ vector_span k s₂ :=
+submodule.span_mono (vsub_set_mono h)
+
 variables (P)
 
 /-- The `vector_span` of the empty set is `⊥`. -/
@@ -396,6 +400,12 @@ begin
     exact vsub_mem_direction hp hq2 }
 end
 
+/-- Two affine subspaces with nonempty intersection are equal if and
+only if their directions are equal. -/
+lemma eq_iff_direction_eq_of_mem {s₁ s₂ : affine_subspace k P} {p : P} (h₁ : p ∈ s₁)
+  (h₂ : p ∈ s₂) : s₁ = s₂ ↔ s₁.direction = s₂.direction :=
+⟨λ h, h ▸ rfl, λ h, ext_of_direction_eq h ⟨p, h₁, h₂⟩⟩
+
 /-- Construct an affine subspace from a point and a direction. -/
 def mk' (p : P) (direction : submodule k V) : affine_subspace k P :=
 { carrier := {q | ∃ v ∈ direction, q = v +ᵥ p},
@@ -455,7 +465,7 @@ begin
   rw hp,
   have hp1s1 : p1 ∈ (s1 : set P) := set.mem_of_mem_of_subset hp1 h,
   refine vadd_mem_of_mem_direction _ hp1s1,
-  have hs : vector_span k s ≤ s1.direction := submodule.span_mono (vsub_set_mono h),
+  have hs : vector_span k s ≤ s1.direction := vector_span_mono k h,
   rw submodule.le_def at hs,
   rw ←submodule.mem_coe,
   exact set.mem_of_mem_of_subset hv hs
@@ -497,7 +507,7 @@ begin
     rw [hp1, hp3, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, submodule.mem_coe],
     exact (vector_span k s).sub_mem ((vector_span k s).add_mem hv1
       (vsub_mem_vector_span k hp2 hp4)) hv2 },
-  { exact submodule.span_mono (vsub_set_mono (subset_span_points k s)) }
+  { exact vector_span_mono k (subset_span_points k s) }
 end
 
 /-- A point in a set is in its affine span. -/
@@ -577,6 +587,13 @@ second. -/
 lemma lt_iff_le_and_exists (s1 s2 : affine_subspace k P) : s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p ∈ s2, p ∉ s1 :=
 by rw [lt_iff_le_not_le, not_le_iff_exists]
 
+/-- If an affine subspace is nonempty and contained in another with
+the same direction, they are equal. -/
+lemma eq_of_direction_eq_of_nonempty_of_le {s₁ s₂ : affine_subspace k P}
+  (hd : s₁.direction = s₂.direction) (hn : (s₁ : set P).nonempty) (hle : s₁ ≤ s₂) :
+  s₁ = s₂ :=
+let ⟨p, hp⟩ := hn in ext_of_direction_eq hd ⟨p, hp, hle hp⟩
+
 variables (k V)
 
 /-- The affine span is the `Inf` of subspaces containing the given
@@ -731,7 +748,7 @@ applies to their directions. -/
 lemma direction_le {s1 s2 : affine_subspace k P} (h : s1 ≤ s2) : s1.direction ≤ s2.direction :=
 begin
   repeat { rw [direction_eq_vector_span, vector_span_def] },
-  exact submodule.span_mono (vsub_set_mono h)
+  exact vector_span_mono k h
 end
 
 /-- If one nonempty affine subspace is less than another, the same

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -25,13 +25,25 @@ variables (k : Type*) {V : Type*} {P : Type*} [field k] [add_comm_group V] [modu
 variables {ι : Type*}
 include V
 
-open finite_dimensional
+open affine_subspace finite_dimensional
 
 /-- The `vector_span` of a finite set is finite-dimensional. -/
 lemma finite_dimensional_vector_span_of_finite {s : set P} (h : set.finite s) :
   finite_dimensional k (vector_span k s) :=
 span_of_finite k $ vsub_set_finite_of_finite h
 
+/-- The `vector_span` of a family indexed by a `fintype` is
+finite-dimensional. -/
+instance finite_dimensional_direction_vector_span_of_fintype [fintype ι] (p : ι → P) :
+  finite_dimensional k (vector_span k (set.range p)) :=
+finite_dimensional_vector_span_of_finite k (set.finite_range _)
+
+/-- The `vector_span` of a subset of a family indexed by a `fintype`
+is finite-dimensional. -/
+instance finite_dimensional_vector_span_image_of_fintype [fintype ι] (p : ι → P)
+  (s : set ι) : finite_dimensional k (vector_span k (p '' s)) :=
+finite_dimensional_vector_span_of_finite k ((set.finite.of_fintype _).image _)
+
 /-- The direction of the affine span of a finite set is
 finite-dimensional. -/
 lemma finite_dimensional_direction_affine_span_of_finite {s : set P} (h : set.finite s) :
@@ -52,37 +64,95 @@ finite_dimensional_direction_affine_span_of_finite k ((set.finite.of_fintype _).
 
 variables {k}
 
-/-- The `vector_span` of a finite affinely independent family has
-dimension one less than its cardinality. -/
-lemma findim_vector_span_of_affine_independent [fintype ι] {p : ι → P}
-  (hi : affine_independent k p) {n : ℕ} (hc : fintype.card ι = n + 1) :
-  findim k (vector_span k (set.range p)) = n :=
+/-- The `vector_span` of a finite subset of an affinely independent
+family has dimension one less than its cardinality. -/
+lemma findim_vector_span_image_finset_of_affine_independent {p : ι → P}
+  (hi : affine_independent k p) {s : finset ι} {n : ℕ} (hc : finset.card s = n + 1) :
+  findim k (vector_span k (p '' ↑s)) = n :=
 begin
-  have hi' := affine_independent_set_of_affine_independent hi,
-  have hc' : fintype.card (set.range p) = n + 1,
-  by rwa set.card_range_of_injective (injective_of_affine_independent hi),
-  have hn : (set.range p).nonempty,
-  { refine set.range_nonempty_iff_nonempty.2 (fintype.card_pos_iff.1 _),
-    simp [hc] },
+  have hi' := affine_independent_of_subset_affine_independent
+    (affine_independent_set_of_affine_independent hi) (set.image_subset_range p ↑s),
+  have hc' : fintype.card (p '' ↑s) = n + 1,
+  { rwa [set.card_image_of_injective ↑s (injective_of_affine_independent hi), fintype.card_coe] },
+  have hn : (p '' ↑s).nonempty,
+  { simp [hc, ←finset.card_pos] },
   rcases hn with ⟨p₁, hp₁⟩,
   rw affine_independent_set_iff_linear_independent_vsub k hp₁ at hi',
-  have hfr : (set.range p \ {p₁}).finite := (set.finite_range _).subset (set.diff_subset _ _),
+  have hfr : (p '' ↑s \ {p₁}).finite := ((set.finite_mem_finset _).image _).subset
+    (set.diff_subset _ _),
   haveI := hfr.fintype,
-  have hf : set.finite ((λ (p : P), p -ᵥ p₁) '' (set.range p \ {p₁})) := hfr.image _,
+  have hf : set.finite ((λ (p : P), p -ᵥ p₁) '' (p '' ↑s \ {p₁})) := hfr.image _,
   haveI := hf.fintype,
   have hc : hf.to_finset.card = n,
   { rw [hf.card_to_finset,
-        set.card_image_of_injective (set.range p \ {p₁}) (vsub_left_injective _)],
-    have hd : insert p₁ (set.range p \ {p₁}) = set.range p,
+        set.card_image_of_injective (p '' ↑s \ {p₁}) (vsub_left_injective _)],
+    have hd : insert p₁ (p '' ↑s \ {p₁}) = p '' ↑s,
     { rw [set.insert_diff_singleton, set.insert_eq_of_mem hp₁] },
-    have hc'' : fintype.card ↥(insert p₁ (set.range p \ {p₁})) = n + 1,
+    have hc'' : fintype.card ↥(insert p₁ (p '' ↑s \ {p₁})) = n + 1,
     { convert hc' },
-    rw set.card_insert (set.range p \ {p₁}) (λ h, ((set.mem_diff p₁).2 h).2 rfl) at hc'',
+    rw set.card_insert (p '' ↑s \ {p₁}) (λ h, ((set.mem_diff p₁).2 h).2 rfl) at hc'',
     simpa using hc'' },
   rw [vector_span_eq_span_vsub_set_right_ne k hp₁, findim_span_set_eq_card _ hi', ←hc],
   congr
 end
 
+/-- The `vector_span` of a finite affinely independent family has
+dimension one less than its cardinality. -/
+lemma findim_vector_span_of_affine_independent [fintype ι] {p : ι → P}
+  (hi : affine_independent k p) {n : ℕ} (hc : fintype.card ι = n + 1) :
+  findim k (vector_span k (set.range p)) = n :=
+begin
+  rw ←finset.card_univ at hc,
+  rw [←set.image_univ, ←finset.coe_univ],
+  exact findim_vector_span_image_finset_of_affine_independent hi hc
+end
+
+/-- If the `vector_span` of a finite subset of an affinely independent
+family lies in a submodule with dimension one less than its
+cardinality, it equals that submodule. -/
+lemma vector_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one
+  {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sm : submodule k V}
+  [finite_dimensional k sm] (hle : vector_span k (p '' ↑s) ≤ sm)
+  (hc : finset.card s = findim k sm + 1) : vector_span k (p '' ↑s) = sm :=
+eq_of_le_of_findim_eq hle $ findim_vector_span_image_finset_of_affine_independent hi hc
+
+/-- If the `vector_span` of a finite affinely independent
+family lies in a submodule with dimension one less than its
+cardinality, it equals that submodule. -/
+lemma vector_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one [fintype ι]
+  {p : ι → P} (hi : affine_independent k p) {sm : submodule k V} [finite_dimensional k sm]
+  (hle : vector_span k (set.range p) ≤ sm) (hc : fintype.card ι = findim k sm + 1) :
+  vector_span k (set.range p) = sm :=
+eq_of_le_of_findim_eq hle $ findim_vector_span_of_affine_independent hi hc
+
+/-- If the `affine_span` of a finite subset of an affinely independent
+family lies in an affine subspace whose direction has dimension one
+less than its cardinality, it equals that subspace. -/
+lemma affine_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one
+  {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sp : affine_subspace k P}
+  [finite_dimensional k sp.direction] (hle : affine_span k (p '' ↑s) ≤ sp)
+  (hc : finset.card s = findim k sp.direction + 1) : affine_span k (p '' ↑s) = sp :=
+begin
+  have hn : (p '' ↑s).nonempty, { simp [hc, ←finset.card_pos] },
+  refine eq_of_direction_eq_of_nonempty_of_le _ ((affine_span_nonempty k _).2 hn) hle,
+  have hd := direction_le hle,
+  rw direction_affine_span at ⊢ hd,
+  exact vector_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one hi hd hc
+end
+
+/-- If the `affine_span` of a finite affinely independent family lies
+in an affine subspace whose direction has dimension one less than its
+cardinality, it equals that subspace. -/
+lemma affine_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one [fintype ι]
+  {p : ι → P} (hi : affine_independent k p) {sp : affine_subspace k P}
+  [finite_dimensional k sp.direction] (hle : affine_span k (set.range p) ≤ sp)
+  (hc : fintype.card ι = findim k sp.direction + 1) : affine_span k (set.range p) = sp :=
+begin
+  rw ←finset.card_univ at hc,
+  rw [←set.image_univ, ←finset.coe_univ] at ⊢ hle,
+  exact affine_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one hi hle hc
+end
+
 /-- The `vector_span` of a finite affinely independent family whose
 cardinality is one more than that of the finite-dimensional space is
 `⊤`. -/
@@ -98,12 +168,8 @@ lemma affine_span_eq_top_of_affine_independent_of_card_eq_findim_add_one [finite
   [fintype ι] {p : ι → P} (hi : affine_independent k p) (hc : fintype.card ι = findim k V + 1) :
   affine_span k (set.range p) = ⊤ :=
 begin
-  have hn : (set.range p).nonempty,
-  { refine set.range_nonempty_iff_nonempty.2 (fintype.card_pos_iff.1 _),
-    simp [hc] },
-  rw [←affine_subspace.direction_eq_top_iff_of_nonempty ((affine_span_nonempty k _).2 hn),
-      direction_affine_span],
-  exact vector_span_eq_top_of_affine_independent_of_card_eq_findim_add_one hi hc
+  rw [←findim_top, ←direction_top k V P] at hc,
+  exact affine_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one hi le_top hc
 end
 
 end affine_space'