refactor(algebra/add_torsor): define pointwise -ᵥ and +ᵥ on sets (#4710)

This seems more natural than `vsub_set` to me.

Author: urkud

src/algebra/add_torsor.lean

@@ -6,6 +6,7 @@ Authors: Joseph Myers, Yury Kudryashov.
 import algebra.group.prod
 import algebra.group.type_tags
 import algebra.group.pi
+import algebra.pointwise
 import data.equiv.basic
 import data.set.finite
 
@@ -229,29 +230,68 @@ element. -/
 lemma eq_vadd_iff_vsub_eq (p1 : P) (g : G) (p2 : P) : p1 = g +ᵥ p2 ↔ p1 -ᵥ p2 = g :=
 ⟨λ h, h.symm ▸ vadd_vsub _ _, λ h, h ▸ (vsub_vadd _ _).symm⟩
 
-/-- The pairwise differences of a set of points. -/
-def vsub_set (s : set P) : set G := set.image2 (-ᵥ) s s
+namespace set
 
-/-- `vsub_set` of an empty set. -/
-@[simp] lemma vsub_set_empty : vsub_set (∅ : set P) = ∅ :=
-set.image2_empty_left
+instance has_vsub : has_vsub (set G) (set P) := ⟨set.image2 (-ᵥ)⟩
 
-/-- `vsub_set` of a single point. -/
-@[simp] lemma vsub_set_singleton (p : P) : vsub_set ({p} : set P) = {(0:G)} :=
-by simp [vsub_set]
+section vsub
 
-/-- `vsub_set` of a finite set is finite. -/
-lemma vsub_set_finite_of_finite {s : set P} (h : set.finite s) : set.finite (vsub_set s) :=
-h.image2 _ h
+variables (s t : set P)
 
-/-- Each pairwise difference is in the `vsub_set`. -/
-lemma vsub_mem_vsub_set {p1 p2 : P} {s : set P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) :
-  (p1 -ᵥ p2) ∈ vsub_set s :=
-set.mem_image2_of_mem hp1 hp2
+@[simp] lemma vsub_empty : s -ᵥ ∅ = ∅ := set.image2_empty_right
 
-/-- `vsub_set` is contained in `vsub_set` of a larger set. -/
-lemma vsub_set_mono {s1 s2 : set P} (h : s1 ⊆ s2) : vsub_set s1 ⊆ vsub_set s2 :=
-set.image2_subset h h
+@[simp] lemma empty_vsub : ∅ -ᵥ s = ∅ := set.image2_empty_left
+
+@[simp] lemma singleton_vsub (p : P) : {p} -ᵥ s = ((-ᵥ) p) '' s :=
+image2_singleton_left
+
+@[simp] lemma vsub_singleton (p : P) : s -ᵥ {p} = (-ᵥ p) '' s :=
+image2_singleton_right
+
+@[simp] lemma singleton_vsub_self (p : P) : ({p} : set P) -ᵥ {p} = {(0:G)} :=
+by simp
+
+variables {s t}
+
+/-- `vsub` of a finite set is finite. -/
+lemma finite.vsub (hs : finite s) (ht : finite t) : finite (s -ᵥ t) :=
+hs.image2 _ ht
+
+/-- Each pairwise difference is in the `vsub` set. -/
+lemma vsub_mem_vsub {ps pt : P} (hs : ps ∈ s) (ht : pt ∈ t) :
+  (ps -ᵥ pt) ∈ s -ᵥ t :=
+mem_image2_of_mem hs ht
+
+/-- `s -ᵥ t` is monotone in both arguments. -/
+@[mono] lemma vsub_subset_vsub {s' t' : set P} (hs : s ⊆ s') (ht : t ⊆ t') :
+  s -ᵥ t ⊆ s' -ᵥ t' :=
+image2_subset hs ht
+
+lemma vsub_self_mono (h : s ⊆ t) : s -ᵥ s ⊆ t -ᵥ t := vsub_subset_vsub h h
+
+lemma vsub_subset_iff {u : set G} : s -ᵥ t ⊆ u ↔ ∀ (x ∈ s) (y ∈ t), x -ᵥ y ∈ u :=
+image2_subset_iff
+
+end vsub
+
+instance add_action : add_action (set G) (set P) :=
+{ vadd := set.image2 (+ᵥ),
+  zero_vadd' := λ s, by simp [← singleton_zero],
+  vadd_assoc' := λ s t p, by { symmetry, apply image2_assoc, intros, symmetry, apply vadd_assoc } }
+
+variables {s s' : set G} {t t' : set P}
+
+@[mono] lemma vadd_subset_vadd (hs : s ⊆ s') (ht : t ⊆ t') : s +ᵥ t ⊆ s' +ᵥ t' :=
+image2_subset hs ht
+
+@[simp] lemma vadd_singleton (s : set G) (p : P) : s +ᵥ {p} = (+ᵥ p) '' s := image2_singleton_right
+
+@[simp] lemma singleton_vadd (v : G) (s : set P) : ({v} : set G) +ᵥ s = ((+ᵥ) v) '' s :=
+image2_singleton_left
+
+lemma finite.vadd (hs : finite s) (ht : finite t) : finite (s +ᵥ t) := hs.image2 _ ht
+
+end set
 
 @[simp] lemma vadd_vsub_vadd_cancel_right (v₁ v₂ : G) (p : P) :
   (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂ :=

src/geometry/euclidean/monge_point.lean

@@ -252,8 +252,9 @@ opposite edge (in 2 dimensions, this is the same as an altitude).
 This definition is only intended to be used when `i₁ ≠ i₂`. -/
 def monge_plane {n : ℕ} (s : simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :
   affine_subspace ℝ P :=
-mk' (({i₁, i₂}ᶜ : finset (fin (n + 3))).centroid ℝ s.points) (submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}).orthogonal ⊓
-  affine_span ℝ (set.range s.points)
+mk' (({i₁, i₂}ᶜ : finset (fin (n + 3))).centroid ℝ s.points)
+  (submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}).orthogonal ⊓
+    affine_span ℝ (set.range s.points)
 
 /-- The definition of a Monge plane. -/
 lemma monge_plane_def {n : ℕ} (s : simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

src/linear_algebra/affine_space/basic.lean

@@ -102,6 +102,8 @@ space, or more generally a module. We omit the arguments `(k : Type*) [ring k] [
 in the type synonym itself to simplify type class search. -/
 notation `affine_space` := add_torsor
 
+open set
+
 section
 
 variables (k : Type*) {V : Type*} {P : Type*} [ring k] [add_comm_group V] [module k V]
@@ -110,36 +112,36 @@ include V
 
 /-- The submodule spanning the differences of a (possibly empty) set
 of points. -/
-def vector_span (s : set P) : submodule k V := submodule.span k (vsub_set s)
+def vector_span (s : set P) : submodule k V := submodule.span k (s -ᵥ s)
 
 /-- The definition of `vector_span`, for rewriting. -/
-lemma vector_span_def (s : set P) : vector_span k s = submodule.span k (vsub_set s) :=
+lemma vector_span_def (s : set P) : vector_span k s = submodule.span k (s -ᵥ 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)
+submodule.span_mono (vsub_self_mono h)
 
 variables (P)
 
 /-- The `vector_span` of the empty set is `⊥`. -/
 @[simp] lemma vector_span_empty : vector_span k (∅ : set P) = (⊥ : submodule k V) :=
-by rw [vector_span_def, vsub_set_empty, submodule.span_empty]
+by rw [vector_span_def, vsub_empty, submodule.span_empty]
 
 variables {P}
 
 /-- The `vector_span` of a single point is `⊥`. -/
 @[simp] lemma vector_span_singleton (p : P) : vector_span k ({p} : set P) = ⊥ :=
 by simp [vector_span_def]
 
-/-- The `vsub_set` lies within the `vector_span`. -/
-lemma vsub_set_subset_vector_span (s : set P) : vsub_set s ⊆ vector_span k s :=
+/-- The `s -ᵥ s` lies within the `vector_span k s`. -/
+lemma vsub_set_subset_vector_span (s : set P) : s -ᵥ s ⊆ ↑(vector_span k s) :=
 submodule.subset_span
 
 /-- Each pairwise difference is in the `vector_span`. -/
 lemma vsub_mem_vector_span {s : set P} {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) :
   p1 -ᵥ p2 ∈ vector_span k s :=
-vsub_set_subset_vector_span k s (vsub_mem_vsub_set hp1 hp2)
+vsub_set_subset_vector_span k s (vsub_mem_vsub hp1 hp2)
 
 /-- The points in the affine span of a (possibly empty) set of
 points. Use `affine_span` instead to get an `affine_subspace k P`. -/
@@ -252,25 +254,25 @@ in the definition of `submodule.span`) can be used in the proof of
 that proof. -/
 def direction_of_nonempty {s : affine_subspace k P} (h : (s : set P).nonempty) :
   submodule k V :=
-{ carrier := vsub_set (s : set P),
+{ carrier := (s : set P) -ᵥ s,
   zero_mem' := begin
     cases h with p hp,
-    exact (vsub_self p) ▸ vsub_mem_vsub_set hp hp
+    exact (vsub_self p) ▸ vsub_mem_vsub hp hp
   end,
   add_mem' := begin
     intros a b ha hb,
     rcases ha with ⟨p1, p2, hp1, hp2, rfl⟩,
     rcases hb with ⟨p3, p4, hp3, hp4, rfl⟩,
     rw [←vadd_vsub_assoc],
-    refine vsub_mem_vsub_set _ hp4,
+    refine vsub_mem_vsub _ hp4,
     convert s.smul_vsub_vadd_mem 1 hp1 hp2 hp3,
     rw one_smul
   end,
   smul_mem' := begin
     intros c v hv,
     rcases hv with ⟨p1, p2, hp1, hp2, rfl⟩,
     rw [←vadd_vsub (c • (p1 -ᵥ p2)) p2],
-    refine vsub_mem_vsub_set _ hp2,
+    refine vsub_mem_vsub _ hp2,
     exact s.smul_vsub_vadd_mem c hp1 hp2 hp2
   end }
 
@@ -283,7 +285,7 @@ le_antisymm (vsub_set_subset_vector_span k s) (submodule.span_le.2 set.subset.rf
 /-- The set of vectors in the direction of a nonempty affine subspace
 is given by `vsub_set`. -/
 lemma coe_direction_eq_vsub_set {s : affine_subspace k P} (h : (s : set P).nonempty) :
-  (s.direction : set V) = vsub_set (s : set P) :=
+  (s.direction : set V) = (s : set P) -ᵥ s :=
 direction_of_nonempty_eq_direction h ▸ rfl
 
 /-- A vector is in the direction of a nonempty affine subspace if and
@@ -704,7 +706,7 @@ variables (P)
 
 /-- The direction of `⊥` is the submodule `⊥`. -/
 @[simp] lemma direction_bot : (⊥ : affine_subspace k P).direction = ⊥ :=
-by rw [direction_eq_vector_span, bot_coe, vector_span_def, vsub_set_empty, submodule.span_empty]
+by rw [direction_eq_vector_span, bot_coe, vector_span_def, vsub_empty, submodule.span_empty]
 
 variables {k V P}
 
@@ -739,8 +741,8 @@ lemma direction_inf (s1 s2 : affine_subspace k P) :
 begin
   repeat { rw [direction_eq_vector_span, vector_span_def] },
   exact le_inf
-    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_set_mono (set.inter_subset_left _ _)) hp))
-    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_set_mono (set.inter_subset_right _ _)) hp))
+    (Inf_le_Inf (λ p hp, trans (vsub_self_mono (inter_subset_left _ _)) hp))
+    (Inf_le_Inf (λ p hp, trans (vsub_self_mono (inter_subset_right _ _)) hp))
 end
 
 /-- If two affine subspaces have a point in common, the direction of
@@ -789,8 +791,8 @@ lemma sup_direction_le (s1 s2 : affine_subspace k P) :
 begin
   repeat { rw [direction_eq_vector_span, vector_span_def] },
   exact sup_le
-    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_set_mono (le_sup_left : s1 ≤ s1 ⊔ s2)) hp))
-    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_set_mono (le_sup_right : s2 ≤ s1 ⊔ s2)) hp))
+    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_self_mono (le_sup_left : s1 ≤ s1 ⊔ s2)) hp))
+    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_self_mono (le_sup_right : s2 ≤ s1 ⊔ s2)) hp))
 end
 
 /-- The sup of the directions of two nonempty affine subspaces with
@@ -865,7 +867,7 @@ variables (k : Type*) {V : Type*} {P : Type*} [ring k] [add_comm_group V] [modul
 variables {ι : Type*}
 include V
 
-open affine_subspace
+open affine_subspace set
 
 /-- The `vector_span` is the span of the pairwise subtractions with a
 given point on the left. -/
@@ -1073,8 +1075,8 @@ begin
     rw [direction_eq_vector_span, vector_span_def],
     exact Inf_le_Inf (λ p hp, set.subset.trans
       (set.singleton_subset_iff.2
-        (vsub_mem_vsub_set (mem_span_points k p2 _ (set.mem_union_right _ hp2))
-                           (mem_span_points k p1 _ (set.mem_union_left _ hp1))))
+        (vsub_mem_vsub (mem_span_points k p2 _ (set.mem_union_right _ hp2))
+                       (mem_span_points k p1 _ (set.mem_union_left _ hp1))))
       hp) }
 end
 

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -35,7 +35,7 @@ open affine_subspace finite_dimensional vector_space
 /-- 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
+span_of_finite k $ h.vsub h
 
 /-- The `vector_span` of a family indexed by a `fintype` is
 finite-dimensional. -/