feat(analysis/normed*): add instances about balls and spheres (#14808)

urkud · urkud · commit f9571f0fcba0 · 2022-06-25T20:02:11.000Z
Non-bc change: `has_inv.inv` on the unit circle is now defined using `has_inv.inv` instead of complex conjugation.
diff --git a/src/analysis/complex/circle.lean b/src/analysis/complex/circle.lean
@@ -5,6 +5,7 @@ Authors: Heather Macbeth
 -/
 import analysis.special_functions.exp
 import topology.continuous_function.basic
+import analysis.normed.field.unit_ball
 
 /-!
 # The circle
@@ -36,14 +37,7 @@ open complex metric
 open_locale complex_conjugate
 
 /-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`. -/
-def circle : submonoid ℂ :=
-{ carrier := sphere (0:ℂ) 1,
-  one_mem' := by simp,
-  mul_mem' := λ a b, begin
-    simp only [norm_eq_abs, mem_sphere_zero_iff_norm],
-    intros ha hb,
-    simp [ha, hb],
-  end }
+def circle : submonoid ℂ := submonoid.unit_sphere ℂ
 
 @[simp] lemma mem_circle_iff_abs {z : ℂ} : z ∈ circle ↔ abs z = 1 := mem_sphere_zero_iff_norm
 
@@ -59,42 +53,26 @@ by rw [mem_circle_iff_abs, complex.abs, real.sqrt_eq_one]
 
 lemma ne_zero_of_mem_circle (z : circle) : (z:ℂ) ≠ 0 := ne_zero_of_mem_unit_sphere z
 
-instance : comm_group circle :=
-{ inv := λ z, ⟨conj (z : ℂ), by simp⟩,
-  mul_left_inv := λ z, subtype.ext $ by { simp [has_inv.inv, ← norm_sq_eq_conj_mul_self,
-    ← mul_self_abs] },
-  .. circle.to_comm_monoid }
+instance : comm_group circle := metric.sphere.comm_group
 
-lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = conj (z : ℂ) := rfl
+@[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = (z : ℂ)⁻¹ := rfl
 
-@[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = (z : ℂ)⁻¹ :=
-begin
-  rw coe_inv_circle_eq_conj,
-  apply eq_inv_of_mul_eq_one_right,
-  rw [mul_comm, ← complex.norm_sq_eq_conj_mul_self],
-  simp,
-end
+lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = conj (z : ℂ) :=
+by rw [coe_inv_circle, inv_def, norm_sq_eq_of_mem_circle, inv_one, of_real_one, mul_one]
 
 @[simp] lemma coe_div_circle (z w : circle) : ↑(z / w) = (z:ℂ) / w :=
-show ↑(z * w⁻¹) = (z:ℂ) * w⁻¹, by simp
+circle.subtype.map_div z w
 
 /-- The elements of the circle embed into the units. -/
-@[simps]
-def circle.to_units : circle →* units ℂ :=
-{ to_fun := λ x, units.mk0 x $ ne_zero_of_mem_circle _,
-  map_one' := units.ext rfl,
-  map_mul' := λ x y, units.ext rfl }
+@[simps apply] def circle.to_units : circle →* units ℂ := unit_sphere_to_units ℂ
 
 instance : compact_space circle := metric.sphere.compact_space _ _
 
--- the following result could instead be deduced from the Lie group structure on the circle using
--- `topological_group_of_lie_group`, but that seems a little awkward since one has to first provide
--- and then forget the model space
-instance : topological_group circle :=
-{ continuous_mul := let h : continuous (λ x : circle, (x : ℂ)) := continuous_subtype_coe in
-    continuous_induced_rng (continuous_mul.comp (h.prod_map h)),
-  continuous_inv := continuous_induced_rng $
-    complex.conj_cle.continuous.comp continuous_subtype_coe }
+instance : topological_group circle := metric.sphere.topological_group
+
+/-- If `z` is a nonzero complex number, then `conj z / z` belongs to the unit circle. -/
+@[simps] def circle.of_conj_div_self (z : ℂ) (hz : z ≠ 0) : circle :=
+⟨conj z / z, mem_circle_iff_abs.2 $ by rw [complex.abs_div, abs_conj, div_self (abs_ne_zero.2 hz)]⟩
 
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
 def exp_map_circle : C(ℝ, circle) :=
diff --git a/src/analysis/normed/field/unit_ball.lean b/src/analysis/normed/field/unit_ball.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Heather Macbeth
+-/
+import analysis.normed.field.basic
+import analysis.normed.group.ball_sphere
+
+/-!
+# Algebraic structures on unit balls and spheres
+
+In this file we define algebraic structures (`semigroup`, `comm_semigroup`, `monoid`, `comm_monoid`,
+`group`, `comm_group`) on `metric.ball (0 : 𝕜) 1`, `metric.closed_ball (0 : 𝕜) 1`, and
+`metric.sphere (0 : 𝕜) 1`. In each case we use the weakest possible typeclass assumption on `𝕜`,
+from `non_unital_semi_normed_ring` to `normed_field`.
+-/
+
+open set metric
+
+variables {𝕜 : Type*}
+
+/-- Unit ball in a non unital semi normed ring as a bundled `subsemigroup`. -/
+def subsemigroup.unit_ball (𝕜 : Type*) [non_unital_semi_normed_ring 𝕜] :
+  subsemigroup 𝕜 :=
+{ carrier := ball (0 : 𝕜) 1,
+  mul_mem' := λ x y hx hy,
+    begin
+      rw [mem_ball_zero_iff] at *,
+      exact (norm_mul_le x y).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _)
+        hx hy.le)
+    end }
+
+instance [non_unital_semi_normed_ring 𝕜] : semigroup (ball (0 : 𝕜) 1) :=
+mul_mem_class.to_semigroup (subsemigroup.unit_ball 𝕜)
+
+instance [non_unital_semi_normed_ring 𝕜] : has_continuous_mul (ball (0 : 𝕜) 1) :=
+⟨continuous_subtype_mk _ $ continuous.mul (continuous_subtype_val.comp continuous_fst)
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+instance [semi_normed_comm_ring 𝕜] : comm_semigroup (ball (0 : 𝕜) 1) :=
+mul_mem_class.to_comm_semigroup (subsemigroup.unit_ball 𝕜)
+
+instance [non_unital_semi_normed_ring 𝕜] : has_distrib_neg (ball (0 : 𝕜) 1) :=
+subtype.coe_injective.has_distrib_neg (coe : ball (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl)
+
+/-- Closed unit ball in a non unital semi normed ring as a bundled `subsemigroup`. -/
+def subsemigroup.unit_closed_ball (𝕜 : Type*) [non_unital_semi_normed_ring 𝕜] :
+  subsemigroup 𝕜 :=
+{ carrier := closed_ball 0 1,
+  mul_mem' := λ x y hx hy,
+    begin
+      rw [mem_closed_ball_zero_iff] at *,
+      exact (norm_mul_le x y).trans (mul_le_one hx (norm_nonneg _) hy)
+    end }
+
+instance [non_unital_semi_normed_ring 𝕜] : semigroup (closed_ball (0 : 𝕜) 1) :=
+mul_mem_class.to_semigroup (subsemigroup.unit_closed_ball 𝕜)
+
+instance [non_unital_semi_normed_ring 𝕜] : has_distrib_neg (closed_ball (0 : 𝕜) 1) :=
+subtype.coe_injective.has_distrib_neg (coe : closed_ball (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl)
+
+instance [non_unital_semi_normed_ring 𝕜] : has_continuous_mul (closed_ball (0 : 𝕜) 1) :=
+⟨continuous_subtype_mk _ $ continuous.mul (continuous_subtype_val.comp continuous_fst)
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+/-- Closed unit ball in a semi normed ring as a bundled `submonoid`. -/
+def submonoid.unit_closed_ball (𝕜 : Type*) [semi_normed_ring 𝕜] [norm_one_class 𝕜] :
+  submonoid 𝕜 :=
+{ carrier := closed_ball 0 1,
+  one_mem' := mem_closed_ball_zero_iff.2 norm_one.le,
+  .. subsemigroup.unit_closed_ball 𝕜 }
+
+instance [semi_normed_ring 𝕜] [norm_one_class 𝕜] : monoid (closed_ball (0 : 𝕜) 1) :=
+submonoid_class.to_monoid (submonoid.unit_closed_ball 𝕜)
+
+instance [semi_normed_comm_ring 𝕜] [norm_one_class 𝕜] : comm_monoid (closed_ball (0 : 𝕜) 1) :=
+submonoid_class.to_comm_monoid (submonoid.unit_closed_ball 𝕜)
+
+/-- Unit sphere in a normed division ring as a bundled `submonoid`. -/
+def submonoid.unit_sphere (𝕜 : Type*) [normed_division_ring 𝕜] : submonoid 𝕜 :=
+{ carrier := sphere (0 : 𝕜) 1,
+  mul_mem' := λ x y hx hy, by { rw [mem_sphere_zero_iff_norm] at *, simp * },
+  one_mem' := mem_sphere_zero_iff_norm.2 norm_one }
+
+instance [normed_division_ring 𝕜] : group (sphere (0 : 𝕜) 1) :=
+{ inv := λ x, ⟨x⁻¹, mem_sphere_zero_iff_norm.2 $
+    by rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]⟩,
+  mul_left_inv := λ x, subtype.coe_injective $ inv_mul_cancel $ ne_zero_of_mem_unit_sphere x,
+  .. submonoid_class.to_monoid (submonoid.unit_sphere 𝕜) }
+
+instance [normed_division_ring 𝕜] : has_distrib_neg (sphere (0 : 𝕜) 1) :=
+subtype.coe_injective.has_distrib_neg (coe : sphere (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl)
+
+/-- Monoid homomorphism from the unit sphere to the group of units. -/
+def unit_sphere_to_units (𝕜 : Type*) [normed_division_ring 𝕜] : sphere (0 : 𝕜) 1 →* units 𝕜 :=
+units.lift_right (submonoid.unit_sphere 𝕜).subtype (λ x, units.mk0 x $ ne_zero_of_mem_unit_sphere _)
+  (λ x, rfl)
+
+instance [normed_division_ring 𝕜] : topological_group (sphere (0 : 𝕜) 1) :=
+{ continuous_mul := continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).mul
+    (continuous_subtype_val.comp continuous_snd),
+  continuous_inv := continuous_subtype_mk _ $
+    continuous_subtype_coe.inv₀ ne_zero_of_mem_unit_sphere }
+
+instance [normed_field 𝕜] : comm_group (sphere (0 : 𝕜) 1) :=
+{ .. metric.sphere.group,
+  .. submonoid_class.to_comm_monoid (submonoid.unit_sphere 𝕜) }
diff --git a/src/analysis/normed/group/ball_sphere.lean b/src/analysis/normed/group/ball_sphere.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Heather Macbeth
+-/
+import analysis.normed.group.basic
+
+/-!
+# Negation on spheres and balls
+
+In this file we define `has_involutive_neg` instances for spheres, open balls, and closed balls in a
+semi normed group.
+-/
+
+open metric set
+
+variables {E : Type*} [semi_normed_group E] {r : ℝ}
+
+/-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the
+antipodal map. -/
+instance : has_involutive_neg (sphere (0 : E) r) :=
+{ neg := λ w, ⟨-↑w, by simp⟩,
+  neg_neg := λ x, subtype.ext $ neg_neg x }
+
+@[simp] lemma coe_neg_sphere {r : ℝ} (v : sphere (0 : E) r) :
+  ↑(-v) = (-v : E) :=
+rfl
+
+instance : has_continuous_neg (sphere (0 : E) r) :=
+⟨continuous_subtype_mk _ continuous_subtype_coe.neg⟩
+
+/-- We equip the ball, in a seminormed group, with a formal operation of negation, namely the
+antipodal map. -/
+instance {r : ℝ} : has_involutive_neg (ball (0 : E) r) :=
+{ neg := λ w, ⟨-↑w, by simpa using w.coe_prop⟩,
+  neg_neg := λ x, subtype.ext $ neg_neg x }
+
+@[simp] lemma coe_neg_ball {r : ℝ} (v : ball (0 : E) r) :
+  ↑(-v) = (-v : E) :=
+rfl
+
+instance : has_continuous_neg (ball (0 : E) r) :=
+⟨continuous_subtype_mk _ continuous_subtype_coe.neg⟩
+
+/-- We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the
+antipodal map. -/
+instance {r : ℝ} : has_involutive_neg (closed_ball (0 : E) r) :=
+{ neg := λ w, ⟨-↑w, by simpa using w.coe_prop⟩,
+  neg_neg := λ x, subtype.ext $ neg_neg x }
+
+@[simp] lemma coe_neg_closed_ball {r : ℝ} (v : closed_ball (0 : E) r) :
+  ↑(-v) = (-v : E) :=
+rfl
+
+instance : has_continuous_neg (closed_ball (0 : E) r) :=
+⟨continuous_subtype_mk _ continuous_subtype_coe.neg⟩
diff --git a/src/analysis/normed/group/basic.lean b/src/analysis/normed/group/basic.lean
@@ -372,15 +372,6 @@ ne_zero_of_norm_ne_zero $ by rwa norm_eq_of_mem_sphere x
 lemma ne_zero_of_mem_unit_sphere (x : sphere (0:E) 1) : (x:E) ≠ 0 :=
 ne_zero_of_mem_sphere one_ne_zero _
 
-/-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the
-antipodal map. -/
-instance {r : ℝ} : has_neg (sphere (0:E) r) :=
-{ neg := λ w, ⟨-↑w, by simp⟩ }
-
-@[simp] lemma coe_neg_sphere {r : ℝ} (v : sphere (0:E) r) :
-  (((-v) : sphere _ _) : E) = - (v:E) :=
-rfl
-
 namespace isometric
 -- TODO This material is superseded by similar constructions such as
 -- `affine_isometry_equiv.const_vadd`; deduplicate
diff --git a/src/analysis/normed_space/ball_action.lean b/src/analysis/normed_space/ball_action.lean
@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Heather Macbeth
+-/
+import analysis.normed.field.unit_ball
+import analysis.normed_space.basic
+
+/-!
+# Multiplicative actions of/on balls and spheres
+
+Let `E` be a normed vector space over a normed field `𝕜`. In this file we define the following
+multiplicative actions.
+
+- The closed unit ball in `𝕜` acts on open balls and closed balls centered at `0` in `E`.
+- The unit sphere in `𝕜` acts on open balls, closed balls, and spheres centered at `0` in `E`.
+-/
+open metric set
+variables {𝕜 E : Type*} [normed_field 𝕜] [semi_normed_group E] [normed_space 𝕜 E] {r : ℝ}
+
+section closed_ball
+
+instance mul_action_closed_ball_ball : mul_action (closed_ball (0 : 𝕜) 1) (ball (0 : E) r) :=
+{ smul := λ c x, ⟨(c : 𝕜) • x, mem_ball_zero_iff.2 $
+    by simpa only [norm_smul, one_mul]
+      using mul_lt_mul' (mem_closed_ball_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2)
+        (norm_nonneg _) one_pos⟩,
+  one_smul := λ x, subtype.ext $ one_smul 𝕜 _,
+  mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ }
+
+instance has_continuous_smul_closed_ball_ball :
+  has_continuous_smul (closed_ball (0 : 𝕜) 1) (ball (0 : E) r) :=
+⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+instance mul_action_closed_ball_closed_ball :
+  mul_action (closed_ball (0 : 𝕜) 1) (closed_ball (0 : E) r) :=
+{ smul := λ c x, ⟨(c : 𝕜) • x, mem_closed_ball_zero_iff.2 $
+    by simpa only [norm_smul, one_mul]
+      using mul_le_mul (mem_closed_ball_zero_iff.1 c.2) (mem_closed_ball_zero_iff.1 x.2)
+        (norm_nonneg _) zero_le_one⟩,
+  one_smul := λ x, subtype.ext $ one_smul 𝕜 _,
+  mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ }
+
+instance has_continuous_smul_closed_ball_closed_ball :
+  has_continuous_smul (closed_ball (0 : 𝕜) 1) (closed_ball (0 : E) r) :=
+⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+end closed_ball
+
+section sphere
+
+instance mul_action_sphere_ball : mul_action (sphere (0 : 𝕜) 1) (ball (0 : E) r) :=
+{ smul := λ c x, inclusion sphere_subset_closed_ball c • x,
+  one_smul := λ x, subtype.ext $ one_smul _ _,
+  mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ }
+
+instance has_continuous_smul_sphere_ball :
+  has_continuous_smul (sphere (0 : 𝕜) 1) (ball (0 : E) r) :=
+⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+instance mul_action_sphere_closed_ball : mul_action (sphere (0 : 𝕜) 1) (closed_ball (0 : E) r) :=
+{ smul := λ c x, inclusion sphere_subset_closed_ball c • x,
+  one_smul := λ x, subtype.ext $ one_smul _ _,
+  mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ }
+
+instance has_continuous_smul_sphere_closed_ball :
+  has_continuous_smul (sphere (0 : 𝕜) 1) (closed_ball (0 : E) r) :=
+⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+instance mul_action_sphere_sphere : mul_action (sphere (0 : 𝕜) 1) (sphere (0 : E) r) :=
+{ smul := λ c x, ⟨(c : 𝕜) • x, mem_sphere_zero_iff_norm.2 $
+    by rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop,
+      one_mul]⟩,
+  one_smul := λ x, subtype.ext $ one_smul _ _,
+  mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ }
+
+instance has_continuous_smul_sphere_sphere :
+  has_continuous_smul (sphere (0 : 𝕜) 1) (sphere (0 : E) r) :=
+⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul
+  (continuous_subtype_val.comp continuous_snd)⟩
+
+end sphere
+
+variables (𝕜) [char_zero 𝕜]
+
+lemma ne_neg_of_mem_sphere {r : ℝ} (hr : r ≠ 0) (x : sphere (0:E) r) : x ≠ - x :=
+λ h, ne_zero_of_mem_sphere hr x ((self_eq_neg 𝕜 _).mp (by { conv_lhs {rw h}, simp }))
+
+lemma ne_neg_of_mem_unit_sphere (x : sphere (0:E) 1) : x ≠ - x :=
+ne_neg_of_mem_sphere 𝕜 one_ne_zero x
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
@@ -187,16 +187,6 @@ def homeomorph_unit_ball {E : Type*} [semi_normed_group E] [normed_space ℝ E]
     ((continuous_const.sub continuous_subtype_coe.norm).inv₀ $
       λ x, (sub_pos.2 $ mem_ball_zero_iff.1 x.2).ne') continuous_subtype_coe }
 
-variables (α)
-
-lemma ne_neg_of_mem_sphere [char_zero α] {r : ℝ} (hr : r ≠ 0) (x : sphere (0:E) r) : x ≠ - x :=
-λ h, ne_zero_of_mem_sphere hr x ((self_eq_neg α _).mp (by { conv_lhs {rw h}, simp }))
-
-lemma ne_neg_of_mem_unit_sphere [char_zero α] (x : sphere (0:E) 1) : x ≠ - x :=
-ne_neg_of_mem_sphere α one_ne_zero x
-
-variables {α}
-
 open normed_field
 
 instance : normed_space α (ulift E) :=
diff --git a/src/geometry/manifold/instances/sphere.lean b/src/geometry/manifold/instances/sphere.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import analysis.complex.circle
+import analysis.normed_space.ball_action
 import analysis.inner_product_space.calculus
 import analysis.inner_product_space.pi_L2
 import geometry.manifold.algebra.lie_group
@@ -426,6 +427,7 @@ instance : lie_group (𝓡 1) circle :=
   end,
   smooth_inv := begin
     apply cont_mdiff.cod_restrict_sphere,
+    simp only [← coe_inv_circle, coe_inv_circle_eq_conj],
     exact complex.conj_cle.cont_diff.cont_mdiff.comp cont_mdiff_coe_sphere
   end }
 
