feat(algebra/add_torsor): add equiv.const_vadd and `equiv.vadd_cons…

…t` (#2907)

Also define their `isometric.*` versions in `analysis/normed_space/add_torsor`.

src/algebra/add_torsor.lean

@@ -3,7 +3,9 @@ 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.group.basic
+import algebra.group.hom
+import algebra.group.type_tags
+import data.equiv.basic
 
 /-!
 # Torsors of additive group actions
@@ -200,25 +202,78 @@ by rw [←add_right_inj (p2 -ᵥ p1 : G), vsub_add_vsub_cancel, ←neg_vsub_eq_v
        ←add_sub_assoc, ←neg_vsub_eq_vsub_rev, neg_add_self, zero_sub]
 
 /-- Cancellation subtracting the results of two subtractions. -/
-@[simp] lemma vsub_sub_vsub_right_cancel (p1 p2 p3 : P) :
+@[simp] lemma vsub_sub_vsub_cancel_right (p1 p2 p3 : P) :
   (p1 -ᵥ p3 : G) - (p2 -ᵥ p3) = (p1 -ᵥ p2) :=
 by rw [←vsub_vadd_eq_vsub_sub, vsub_vadd]
 
 /-- The pairwise differences of a set of points. -/
 def vsub_set (s : set P) : set G := {g | ∃ x ∈ s, ∃ y ∈ s, g = x -ᵥ y}
 
+@[simp] lemma vadd_vsub_vadd_cancel_right (v₁ v₂ : G) (p : P) :
+  ((v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) : G) = v₁ - v₂ :=
+by rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
+
 end general
 
 section comm
 
-variables (G : Type*) {P : Type*} [add_comm_group G] [S : add_torsor G P]
-include S
+variables (G : Type*) {P : Type*} [add_comm_group G] [add_torsor G P]
 
 /-- Cancellation subtracting the results of two subtractions. -/
-@[simp] lemma vsub_sub_vsub_left_cancel (p1 p2 p3 : P) :
+@[simp] lemma vsub_sub_vsub_cancel_left (p1 p2 p3 : P) :
   (p3 -ᵥ p2 : G) - (p3 -ᵥ p1) = (p1 -ᵥ p2) :=
 by rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
 
+@[simp] lemma vadd_vsub_vadd_cancel_left (v : G) (p1 p2 : P) :
+  ((v +ᵥ p1) -ᵥ (v +ᵥ p2) : G) = p1 -ᵥ p2 :=
+by rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel']
+
 end comm
 
 end add_torsor
+
+namespace equiv
+
+variables (G : Type*) {P : Type*} [add_group G] [add_torsor G P]
+
+open add_action add_torsor
+
+/-- `v ↦ v +ᵥ p` as an equivalence. -/
+def vadd_const (p : P) : G ≃ P :=
+{ to_fun := λ v, v +ᵥ p,
+  inv_fun := λ p', p' -ᵥ p,
+  left_inv := λ v, vadd_vsub _ _ _,
+  right_inv := λ p', vsub_vadd _ _ _ }
+
+@[simp] lemma coe_vadd_const (p : P) : ⇑(vadd_const G p) = λ v, v+ᵥ p := rfl
+
+@[simp] lemma coe_vadd_const_symm (p : P) : ⇑(vadd_const G p).symm = λ p', p' -ᵥ p := rfl
+
+variables {G} (P)
+
+/-- The permutation given by `p ↦ v +ᵥ p`. -/
+def const_vadd (v : G) : equiv.perm P :=
+{ to_fun := (+ᵥ) v,
+  inv_fun := (+ᵥ) (-v),
+  left_inv := λ p, by simp [vadd_assoc],
+  right_inv := λ p, by simp [vadd_assoc] }
+
+@[simp] lemma coe_const_vadd (v : G) : ⇑(const_vadd P v) = (+ᵥ) v := rfl
+
+variable (G)
+
+@[simp] lemma const_vadd_zero : const_vadd P (0:G) = 1 := ext $ zero_vadd G
+
+variable {G}
+
+@[simp] lemma const_vadd_add (v₁ v₂ : G) :
+  const_vadd P (v₁ + v₂) = const_vadd P v₁ * const_vadd P v₂ :=
+ext $ λ p, (vadd_assoc G v₁ v₂ p).symm
+
+/-- `equiv.const_vadd` as a homomorphism from `multiplicative G` to `equiv.perm P` -/
+def const_vadd_hom : multiplicative G →* equiv.perm P :=
+{ to_fun := λ v, const_vadd P v.to_add,
+  map_one' := const_vadd_zero G P,
+  map_mul' := const_vadd_add P }
+
+end equiv

src/analysis/normed_space/add_torsor.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Joseph Myers.
 -/
 import algebra.add_torsor
-import analysis.normed_space.basic
+import topology.metric_space.isometry
 
 noncomputable theory
 
@@ -39,6 +39,16 @@ lemma add_torsor.dist_eq_norm (V : Type u) {P : Type v} [normed_group V] [metric
   dist x y = ∥(x -ᵥ y : V)∥ :=
 normed_add_torsor.dist_eq_norm' x y
 
+lemma dist_vadd_cancel_left {V : Type u} {P : Type v} [normed_group V] [metric_space P]
+    [normed_add_torsor V P] (v : V) (x y : P) :
+  dist (v +ᵥ x) (v +ᵥ y) = dist x y :=
+by rw [add_torsor.dist_eq_norm V, add_torsor.dist_eq_norm V, add_torsor.vadd_vsub_vadd_cancel_left]
+
+lemma dist_vadd_cancel_right {V : Type u} {P : Type v} [normed_group V] [metric_space P]
+    [normed_add_torsor V P] (v₁ v₂ : V) (x : P) :
+  dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂ :=
+by rw [add_torsor.dist_eq_norm V, dist_eq_norm, add_torsor.vadd_vsub_vadd_cancel_right]
+
 /-- A `normed_group` is a `normed_add_torsor` over itself. -/
 instance normed_group.normed_add_torsor (V : Type u) [normed_group V] :
   normed_add_torsor V V :=
@@ -61,3 +71,32 @@ def metric_space_of_normed_group_of_add_torsor (V : Type u) (P : Type v) [normed
     rw ←vsub_add_vsub_cancel,
     apply norm_add_le
   end }
+
+namespace isometric
+
+variables (V : Type u) {P : Type v} [normed_group V] [metric_space P] [normed_add_torsor V P]
+
+/-- The map `v ↦ v +ᵥ p` as an isometric equivalence between `V` and `P`. -/
+def vadd_const (p : P) : V ≃ᵢ P :=
+⟨equiv.vadd_const V p, isometry_emetric_iff_metric.2 $ λ x₁ x₂, dist_vadd_cancel_right x₁ x₂ p⟩
+
+@[simp] lemma coe_vadd_const (p : P) : ⇑(vadd_const V p) = λ v, v +ᵥ p := rfl
+
+@[simp] lemma coe_vadd_const_symm (p : P) : ⇑(vadd_const V p).symm = λ p', p' -ᵥ p := rfl
+
+@[simp] lemma vadd_const_to_equiv (p : P) : (vadd_const V p).to_equiv = equiv.vadd_const V p := rfl
+
+variables {V} (P)
+
+/-- The map `p ↦ v +ᵥ p` as an isometric automorphism of `P`. -/
+def const_vadd (v : V) : P ≃ᵢ P :=
+⟨equiv.const_vadd P v, isometry_emetric_iff_metric.2 $ dist_vadd_cancel_left v⟩
+
+@[simp] lemma coe_const_vadd (v : V) : ⇑(const_vadd P v) = (+ᵥ) v := rfl
+
+variable (V)
+
+@[simp] lemma const_vadd_zero : const_vadd P (0:V) = isometric.refl P :=
+isometric.to_equiv_inj $ equiv.const_vadd_zero V P
+
+end isometric