feat(*): define equiv.reflection and isometry.reflection (#2609)

Define reflection in a point and prove basic properties.
It is defined both as an `equiv.perm` of an `add_comm_group` and
as an `isometric` of a `normed_group`.

Other changes:

* rename `two_smul` to `two_smul'`, add `two_smul` using `semimodule`
  instead of `add_monoid.smul`;
* minor review of `algebra.midpoint`;
* arguments of `isometry.dist_eq` and `isometry.edist_eq` are now explicit;
* rename `isometry.inv` to `isometry.right_inv`; now it takes `right_inverse`
  instead of `equiv`;
* drop `isometry_inv_fun`: use `h.symm.isometry` instead;
* pull a few more lemmas about `equiv` and `isometry` to the `isometric` namespace.

src/algebra/group_power.lean

@@ -83,7 +83,7 @@ by rw [succ_smul, smul_add_comm']
 
 theorem pow_two (a : M) : a^2 = a * a :=
 show a*(a*1)=a*a, by rw mul_one
-theorem two_smul (a : A) : 2•a = a + a :=
+theorem two_smul' (a : A) : 2•a = a + a :=
 show a+(a+0)=a+a, by rw add_zero
 
 theorem pow_add (a : M) (m n : ℕ) : a^(m + n) = a^m * a^n :=

src/algebra/midpoint.lean

@@ -9,19 +9,26 @@ import algebra.invertible
 /-!
 # Midpoint of a segment
 
-Given two points `x` and `y` in a vector space over a ring `R` with invertible `2`,
-we define `midpoint R x y` to be `(⅟2:R) • (x + y)`, where `(⅟2:R)` is the inverse of `(2:R)`
-provided by `[invertible (2:R)]`.
+## Main definitions
 
-We prove that `z` is the midpoint of `[x, y]` if and only if `x + y = z + z`, hence `midpoint R x y`
-does not depend on `R`. We also prove that `midpoint x y` is linear both in `x` and `y`.
+* `midpoint R x y`: midpoint of the segment `[x, y]`. We define it for `x` and `y`
+  in a module over a ring `R` with invertible `2`.
+* `add_monoid_hom.of_map_midpoint`: construct an `add_monoid_hom` given a map `f` such that
+  `f` sends zero to zero and midpoints to midpoints.
 
-We do not mark lemmas other than `midpoint_self` as `@[simp]` because it is hard to tell which side
-is simpler.
+## Main theorems
+
+* `midpoint_eq_iff`: `z` is the midpoint of `[x, y]` if and only if `x + y = z + z`,
+* `midpoint_unique`: `midpoint R x y` does not depend on `R`;
+* `midpoint x y` is linear both in `x` and `y`;
+* `reflection_midpoint_left`, `reflection_midpoint_right`: `equiv.reflection (midpoint R x y)`
+  swaps `x` and `y`.
+
+We do not mark most lemmas as `@[simp]` because it is hard to tell which side is simpler.
 
 ## Tags
 
-midpoint
+midpoint, add_monoid_hom
 -/
 
 variables (R : Type*) {E : Type*}
@@ -36,23 +43,29 @@ def midpoint (x y : E) : E := (⅟2:R) • (x + y)
 lemma midpoint_eq_iff {x y z : E} : midpoint R x y = z ↔ x + y = z + z :=
 ⟨λ h, h ▸ calc x + y = (2 * ⅟2:R) • (x + y) : by rw [mul_inv_of_self, one_smul]
  ... = midpoint R x y + midpoint R x y : by rw [two_mul, add_smul, midpoint],
- λ h, by rw [midpoint, h, ← one_smul R z, ← add_smul, smul_smul, ← bit0, inv_of_mul_self]⟩
-
-variable {R}
+ λ h, by rw [midpoint, h, ← two_smul R z, smul_smul, inv_of_mul_self, one_smul]⟩
 
-lemma midpoint_def (x y : E) : midpoint R x y = (⅟2:R) • (x + y) := rfl
+@[simp] lemma midpoint_add_self (x y : E) : midpoint R x y + midpoint R x y = x + y :=
+((midpoint_eq_iff R).1 rfl).symm
 
 /-- `midpoint` does not depend on the ring `R`. -/
 lemma midpoint_unique (R' : Type*) [semiring R'] [invertible (2:R')] [semimodule R' E] (x y : E) :
   midpoint R x y = midpoint R' x y :=
 (midpoint_eq_iff R).2 $ (midpoint_eq_iff R').1 rfl
 
 @[simp] lemma midpoint_self (x : E) : midpoint R x x = x :=
-by rw [midpoint_def, smul_add, ← add_smul, ← mul_two, inv_of_mul_self, one_smul]
+by rw [midpoint, smul_add, ← two_smul R, smul_smul, mul_inv_of_self, one_smul]
+
+variable {R}
+
+lemma midpoint_def (x y : E) : midpoint R x y = (⅟2:R) • (x + y) := rfl
 
 lemma midpoint_comm (x y : E) : midpoint R x y = midpoint R y x :=
 by simp only [midpoint_def, add_comm]
 
+lemma midpoint_zero_add (x y : E) : midpoint R 0 (x + y) = midpoint R x y :=
+(midpoint_eq_iff R).2 $ (zero_add (x + y)).symm ▸ (midpoint_eq_iff R).1 rfl
+
 lemma midpoint_add_add (x y x' y' : E) :
   midpoint R (x + x') (y + y') = midpoint R x y + midpoint R x' y' :=
 by { simp only [midpoint_def, ← smul_add, add_assoc, add_left_comm x'] }
@@ -68,6 +81,8 @@ lemma midpoint_smul_smul (c : R) (x y : E) : midpoint R (c • x) (c • y) = c
 
 end monoid
 
+section group
+
 variables [ring R] [invertible (2:R)] [add_comm_group E] [module R E]
 
 lemma midpoint_neg_neg (x y : E) : midpoint R (-x) (-y) = -midpoint R x y :=
@@ -82,3 +97,42 @@ by rw [midpoint_sub_sub, midpoint_self]
 
 lemma midpoint_sub_left (x y z : E) : midpoint R (x - y) (x - z) = x - midpoint R y z :=
 by rw [midpoint_sub_sub, midpoint_self]
+
+end group
+
+namespace add_monoid_hom
+
+variables (R) (R' : Type*) {F : Type*}
+  [semiring R] [invertible (2:R)] [add_comm_monoid E] [semimodule R E]
+  [semiring R'] [invertible (2:R')] [add_comm_monoid F] [semimodule R' F]
+
+/-- A map `f : E → F` sending zero to zero and midpoints to midpoints is an `add_monoid_hom`. -/
+def of_map_midpoint (f : E → F) (h0 : f 0 = 0)
+  (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) :
+  E →+ F :=
+{ to_fun := f,
+  map_zero' := h0,
+  map_add' := λ x y, -- by rw [← midpoint_self R (x + y), ← midpoint_zero_add, hm, h0]
+    calc f (x + y) = f 0 + f (x + y) : by rw [h0, zero_add]
+    ... = midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) :
+      (midpoint_add_self _ _ _).symm
+    ... = f (midpoint R x y) + f (midpoint R x y) : by rw [← hm, midpoint_zero_add]
+    ... = f x + f y : by rw [hm, midpoint_add_self] }
+
+@[simp] lemma coe_of_map_midpoint (f : E → F) (h0 : f 0 = 0)
+  (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) :
+  ⇑(of_map_midpoint R R' f h0 hm) = f := rfl
+
+end add_monoid_hom
+
+namespace equiv
+
+variables [ring R] [invertible (2:R)] [add_comm_group E] [module R E]
+
+@[simp] lemma reflection_midpoint_left (x y : E) : (reflection (midpoint R x y) : E → E) x = y :=
+by rw [reflection_apply, midpoint_add_self, add_sub_cancel']
+
+@[simp] lemma reflection_midpoint_right (x y : E) : (reflection (midpoint R x y) : E → E) y = x :=
+by rw [reflection_apply, midpoint_add_self, add_sub_cancel]
+
+end equiv

src/algebra/module.lean

@@ -71,6 +71,8 @@ theorem add_smul : (r + s) • x = r • x + s • x := semimodule.add_smul r s
 variables (R)
 @[simp] theorem zero_smul : (0 : R) • x = 0 := semimodule.zero_smul x
 
+theorem two_smul : (2 : R) • x = x + x := by rw [bit0, add_smul, one_smul]
+
 variable (M)
 
 /-- `(•)` as an `add_monoid_hom`. -/

src/analysis/normed_space/basic.lean

@@ -633,6 +633,8 @@ hf.div hg hnz
 
 lemma real.norm_eq_abs (r : ℝ) : norm r = abs r := rfl
 
+@[simp] lemma real.norm_two : ∥(2:ℝ)∥ = 2 := abs_of_pos (@two_pos ℝ _)
+
 @[simp] lemma norm_norm [normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
 by rw [real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]
 

src/analysis/normed_space/reflection.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury Kudryashov
+-/
+import algebra.midpoint
+import topology.metric_space.isometry
+
+/-!
+# Reflection in a point as an `isometric` homeomorphism
+
+Given a `normed_group E` and `x : E`, we define `isometric.reflection x` to be
+the reflection in `x` interpreted as an `isometric` homeomorphism.
+
+Reflection is defined as an `equiv.perm` in `data.equiv.mul_add`. In this file
+we restate results about `equiv.reflection` for an `isometric.reflection`, and
+add a few results about `dist`.
+
+## Tags
+
+reflection, isometric
+-/
+
+variables (R : Type*) {E : Type*}
+
+lemma equiv.reflection_fixed_iff_of_module [ring R] [invertible (2:R)]
+  [add_comm_group E] [module R E] {x y : E} :
+  (equiv.reflection x : E → E) y = y ↔ y = x :=
+equiv.reflection_fixed_iff_of_bit0_inj $ λ x y h,
+by rw [← one_smul R x, ← one_smul R y, ← inv_of_mul_self (2:R), mul_smul, mul_smul, two_smul,
+  two_smul, ← bit0, ← bit0, h]
+
+namespace isometric
+
+section normed_group
+
+variables [normed_group E]
+
+/-- Reflection in `x` as an `isometric` homeomorphism. -/
+def reflection (x : E) : E ≃ᵢ E :=
+(isometric.neg E).trans (isometric.add_left (x + x))
+
+lemma reflection_apply (x y : E) : (reflection x : E → E) y = x + x - y := rfl
+
+@[simp] lemma reflection_to_equiv (x : E) : (reflection x).to_equiv = equiv.reflection x := rfl
+
+@[simp] lemma reflection_self (x : E) : (reflection x : E → E) x = x := add_sub_cancel _ _
+
+lemma reflection_involutive (x : E) : function.involutive (reflection x : E → E) :=
+equiv.reflection_involutive x
+
+@[simp] lemma reflection_symm (x : E) : (reflection x).symm = reflection x :=
+to_equiv_inj $ equiv.reflection_symm x
+
+@[simp] lemma reflection_dist_fixed (x y : E) :
+  dist ((reflection x : E → E) y) x = dist y x :=
+by rw [← (reflection x).dist_eq y x, reflection_self]
+
+lemma reflection_dist_self' (x y : E) :
+  dist ((reflection x : E → E) y) y = dist (x + x) (y + y) :=
+by { simp only [reflection_apply, dist_eq_norm], congr' 1, abel }
+
+end normed_group
+
+section module
+
+variables [ring R] [invertible (2:R)] [normed_group E] [module R E]
+
+@[simp] lemma reflection_midpoint_left (x y : E) : (reflection (midpoint R x y) : E → E) x = y :=
+equiv.reflection_midpoint_left R x y
+
+@[simp] lemma reflection_midpoint_right (x y : E) : (reflection (midpoint R x y) : E → E) y = x :=
+equiv.reflection_midpoint_right R x y
+
+variable (R)
+
+include R
+
+lemma reflection_fixed_iff {x y : E} : (reflection x : E → E) y = y ↔ y = x :=
+equiv.reflection_fixed_iff_of_module R
+
+end module
+
+section normed_space
+
+variables (R) [normed_field R] [normed_group E] [normed_space R E]
+
+lemma reflection_dist_self (x y : E) :
+  dist ((reflection x : E → E) y) y = ∥(2:R)∥ * dist x y :=
+by simp only [reflection_dist_self', ← two_smul R x, ← two_smul R y, dist_smul]
+
+end normed_space
+
+lemma reflection_dist_self_real [normed_group E] [normed_space ℝ E] (x y : E) :
+  dist ((reflection x : E → E) y) y = 2 * dist x y :=
+by simp [reflection_dist_self ℝ x y, real.norm_two]
+
+end isometric

src/data/equiv/mul_add.lean

@@ -283,4 +283,30 @@ protected def inv : perm G :=
 
 end group
 
+section reflection
+
+variables [add_comm_group A] (x y : A)
+
+/-- Reflection in `x` as a permutation. -/
+def reflection (x : A) : perm A :=
+(equiv.neg A).trans (equiv.add_left (x + x))
+
+lemma reflection_apply : reflection x y = x + x - y := rfl
+
+@[simp] lemma reflection_self : reflection x x = x := add_sub_cancel _ _
+
+lemma reflection_involutive : function.involutive (reflection x : A → A) :=
+λ y, by simp only [reflection_apply, sub_sub_cancel]
+
+@[simp] lemma reflection_symm : (reflection x).symm = reflection x :=
+by { ext y, rw [symm_apply_eq, reflection_involutive x y] }
+
+/-- `x` is the only fixed point of `reflection x`. This lemma requires `x + x = y + y ↔ x = y`.
+There is no typeclass to use here, so we add it as an explicit argument. -/
+lemma reflection_fixed_iff_of_bit0_inj {x y : A} (h : function.injective (bit0 : A → A)) :
+  reflection x y = y ↔ y = x :=
+sub_eq_iff_eq_add.trans $ h.eq_iff.trans eq_comm
+
+end reflection
+
 end equiv

src/topology/metric_space/gromov_hausdorff.lean

@@ -275,10 +275,10 @@ begin
       repeat {split},
       { exact λx y, calc
         F (inl x, inl y) = dist (Φ x) (Φ y) : rfl
-        ... = dist x y : Φisom.dist_eq },
+        ... = dist x y : Φisom.dist_eq x y },
       { exact λx y, calc
         F (inr x, inr y) = dist (Ψ x) (Ψ y) : rfl
-        ... = dist x y : Ψisom.dist_eq },
+        ... = dist x y : Ψisom.dist_eq x y },
       { exact λx y, dist_comm _ _ },
       { exact λx y z, dist_triangle _ _ _ },
       { exact λx y, calc