feat(analysis/normed_space): Define conformal maps on inner product s…

…paces; define the groupoid of conformal maps (#8367)




Co-authored-by: justadzr <66561890+justadzr@users.noreply.github.com>

src/analysis/calculus/conformal.lean

@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2021 Yourong Zang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yourong Zang
+-/
+import analysis.normed_space.conformal_linear_map
+
+/-!
+# Conformal Maps
+
+A continuous linear map between real normed spaces `X` and `Y` is `conformal_at` some point `x`
+if it is real differentiable at that point and its differential `is_conformal_linear_map`.
+
+## Main definitions
+
+* `conformal_at`: the main definition of conformal maps
+* `conformal`: maps that are conformal at every point
+* `conformal_factor_at`: the conformal factor of a conformal map at some point
+
+## Main results
+* The conformality of the composition of two conformal maps, the identity map
+  and multiplications by nonzero constants
+* `conformal_at_iff_is_conformal_map_fderiv`: an equivalent definition of the conformality of a map
+* `conformal_at_iff`: an equivalent definition of the conformality of a map
+* `conformal_at.preserves_angle`: if a map is conformal at `x`, then its differential
+                                  preserves all angles at `x`
+
+## Tags
+
+conformal
+
+## Warning
+
+The definition of conformality in this file does NOT require the maps to be orientation-preserving.
+Maps such as the complex conjugate is considered as a conformal map.
+-/
+
+noncomputable theory
+
+variables {E F : Type*} [inner_product_space ℝ E] [inner_product_space ℝ F]
+  {X Y Z : Type*} [normed_group X] [normed_group Y] [normed_group Z]
+  [normed_space ℝ X] [normed_space ℝ Y] [normed_space ℝ Z]
+
+section loc_conformality
+
+open linear_isometry continuous_linear_map
+open_locale real_inner_product_space
+
+/-- A map `f` is said to be conformal if it has a conformal differential `f'`. -/
+def conformal_at (f : X → Y) (x : X) :=
+∃ (f' : X →L[ℝ] Y), has_fderiv_at f f' x ∧ is_conformal_map f'
+
+lemma conformal_at_id (x : X) : conformal_at id x :=
+⟨id ℝ X, has_fderiv_at_id _, is_conformal_map_id⟩
+
+lemma conformal_at_const_smul {c : ℝ} (h : c ≠ 0) (x : X) :
+  conformal_at (λ (x': X), c • x') x :=
+⟨c • continuous_linear_map.id ℝ X,
+  (has_fderiv_at_id x).const_smul c, is_conformal_map_const_smul h⟩
+
+/-- A function is a conformal map if and only if its differential is a conformal linear map-/
+lemma conformal_at_iff_is_conformal_map_fderiv {f : X → Y} {x : X} :
+  conformal_at f x ↔ is_conformal_map (fderiv ℝ f x) :=
+begin
+  split,
+  { rintros ⟨c, hf, hf'⟩,
+    rw hf.fderiv,
+    exact hf' },
+  { intros H,
+    by_cases h : differentiable_at ℝ f x,
+    { exact ⟨fderiv ℝ f x, h.has_fderiv_at, H⟩, },
+    { cases subsingleton_or_nontrivial X with w w; resetI,
+      { exact ⟨(0 : X →L[ℝ] Y), has_fderiv_at_of_subsingleton f x,
+        is_conformal_map_of_subsingleton 0⟩, },
+      { exfalso,
+        rcases nontrivial_iff.mp w with ⟨a, b, hab⟩,
+        rw [fderiv_zero_of_not_differentiable_at h] at H,
+        exact hab (H.injective rfl), }, }, },
+end
+
+/-- A real differentiable map `f` is conformal at point `x` if and only if its
+    differential `fderiv ℝ f x` at that point scales every inner product by a positive scalar. -/
+lemma conformal_at_iff' {f : E → F} {x : E} :
+  conformal_at f x ↔
+  ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), ⟪fderiv ℝ f x u, fderiv ℝ f x v⟫ = c * ⟪u, v⟫ :=
+by rw [conformal_at_iff_is_conformal_map_fderiv, is_conformal_map_iff]
+
+/-- A real differentiable map `f` is conformal at point `x` if and only if its
+    differential `f'` at that point scales every inner product by a positive scalar. -/
+lemma conformal_at_iff {f : E → F} {x : E} {f' : E →L[ℝ] F} (h : has_fderiv_at f f' x) :
+  conformal_at f x ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), ⟪f' u, f' v⟫ = c * ⟪u, v⟫ :=
+by simp only [conformal_at_iff', h.fderiv]
+
+namespace conformal_at
+
+lemma differentiable_at {f : X → Y} {x : X} (h : conformal_at f x) :
+  differentiable_at ℝ f x :=
+let ⟨_, h₁, _⟩ := h in h₁.differentiable_at
+
+lemma congr {f g : X → Y} {x : X} {u : set X} (hx : x ∈ u) (hu : is_open u)
+  (hf : conformal_at f x) (h : ∀ (x : X), x ∈ u → g x = f x) :
+  conformal_at g x :=
+let ⟨f', hfderiv, hf'⟩ := hf in
+  ⟨f', hfderiv.congr_of_eventually_eq ((hu.eventually_mem hx).mono h), hf'⟩
+
+lemma comp {f : X → Y} {g : Y → Z} (x : X)
+  (hg : conformal_at g (f x)) (hf : conformal_at f x) : conformal_at (g ∘ f) x :=
+begin
+  rcases hf with ⟨f', hf₁, cf⟩,
+  rcases hg with ⟨g', hg₁, cg⟩,
+  exact ⟨g'.comp f', hg₁.comp x hf₁, cf.comp cg⟩,
+end
+
+lemma const_smul {f : X → Y} {x : X} {c : ℝ} (hc : c ≠ 0) (hf : conformal_at f x) :
+  conformal_at (c • f) x :=
+(conformal_at_const_smul hc $ f x).comp x hf
+
+/-- The conformal factor of a conformal map at some point `x`. Some authors refer to this function
+    as the characteristic function of the conformal map. -/
+def conformal_factor_at {f : E → F} {x : E} (h : conformal_at f x) : ℝ :=
+classical.some (conformal_at_iff'.mp h)
+
+lemma conformal_factor_at_pos {f : E → F} {x : E} (h : conformal_at f x) :
+  0 < conformal_factor_at h :=
+(classical.some_spec $ conformal_at_iff'.mp h).1
+
+lemma conformal_factor_at_inner_eq_mul_inner' {f : E → F} {x : E}
+  (h : conformal_at f x) (u v : E) :
+  ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫ = (conformal_factor_at h : ℝ) * ⟪u, v⟫ :=
+(classical.some_spec $ conformal_at_iff'.mp h).2 u v
+
+lemma conformal_factor_at_inner_eq_mul_inner {f : E → F} {x : E} {f' : E →L[ℝ] F}
+  (h : has_fderiv_at f f' x) (H : conformal_at f x) (u v : E) :
+  ⟪f' u, f' v⟫ = (conformal_factor_at H : ℝ) * ⟪u, v⟫ :=
+(H.differentiable_at.has_fderiv_at.unique h) ▸ conformal_factor_at_inner_eq_mul_inner' H u v
+
+/-- If a real differentiable map `f` is conformal at a point `x`,
+    then it preserves the angles at that point. -/
+lemma preserves_angle {f : E → F} {x : E} {f' : E →L[ℝ] F}
+  (h : has_fderiv_at f f' x) (H : conformal_at f x) (u v : E) :
+  inner_product_geometry.angle (f' u) (f' v) = inner_product_geometry.angle u v :=
+let ⟨f₁, h₁, c⟩ := H in h₁.unique h ▸ c.preserves_angle u v
+
+end conformal_at
+
+end loc_conformality
+
+section global_conformality
+
+/-- A map `f` is conformal if it's conformal at every point. -/
+def conformal (f : X → Y) :=
+∀ (x : X), conformal_at f x
+
+lemma conformal_id : conformal (id : X → X) := λ x, conformal_at_id x
+
+lemma conformal_const_smul {c : ℝ} (h : c ≠ 0) : conformal (λ (x : X), c • x) :=
+λ x, conformal_at_const_smul h x
+
+namespace conformal
+
+lemma conformal_at {f : X → Y} (h : conformal f) (x : X) : conformal_at f x := h x
+
+lemma differentiable {f : X → Y} (h : conformal f) : differentiable ℝ f :=
+λ x, (h x).differentiable_at
+
+lemma comp {f : X → Y} {g : Y → Z} (hf : conformal f) (hg : conformal g) : conformal (g ∘ f) :=
+λ x, (hg $ f x).comp x (hf x)
+
+lemma const_smul {f : X → Y} (hf : conformal f) {c : ℝ} (hc : c ≠ 0) : conformal (c • f) :=
+λ x, (hf x).const_smul hc
+
+end conformal
+
+end global_conformality

src/analysis/calculus/fderiv.lean

@@ -829,6 +829,16 @@ end
 lemma differentiable_on_const (c : F) : differentiable_on 𝕜 (λx, c) s :=
 (differentiable_const _).differentiable_on
 
+lemma has_fderiv_at_of_subsingleton {R X Y : Type*} [nondiscrete_normed_field R]
+  [normed_group X] [normed_group Y] [normed_space R X] [normed_space R Y] [h : subsingleton X]
+  (f : X → Y) (x : X) :
+  has_fderiv_at f (0 : X →L[R] Y) x :=
+begin
+  rw subsingleton_iff at h,
+  have key : function.const X (f 0) = f := by ext x'; rw h x' 0,
+  exact key ▸ (has_fderiv_at_const (f 0) _),
+end
+
 end const
 
 section continuous_linear_map

src/analysis/normed_space/conformal_linear_map.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2021 Yourong Zang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yourong Zang
+-/
+import geometry.euclidean.basic
+import analysis.normed_space.inner_product
+
+/-!
+# Conformal Linear Maps
+
+A continuous linear map between `R`-normed spaces `X` and `Y` `is_conformal_map` if it is
+a nonzero multiple of a linear isometry.
+
+## Main definitions
+
+* `is_conformal_map`: the main definition of conformal linear maps
+
+## Main results
+
+* The conformality of the composition of two conformal linear maps, the identity map
+  and multiplications by nonzero constants as continuous linear maps
+* `is_conformal_map_iff`: an equivalent definition of the conformality
+* `is_conformal_map_of_subsingleton`: all continuous linear maps on singleton spaces are conformal
+* `is_conformal_map.preserves_angle`: if a continuous linear map is conformal, then it
+                                      preserves all angles in the normed space
+
+## Tags
+
+conformal
+
+## Warning
+
+The definition of conformality in this file does NOT require the maps to be orientation-preserving.
+-/
+
+noncomputable theory
+
+open linear_isometry continuous_linear_map
+open_locale real_inner_product_space
+
+/-- A continuous linear map `f'` is said to be conformal if it's
+    a nonzero multiple of a linear isometry. -/
+def is_conformal_map {R : Type*} {X Y : Type*} [nondiscrete_normed_field R]
+  [normed_group X] [normed_group Y] [normed_space R X] [normed_space R Y]
+  (f' : X →L[R] Y) :=
+∃ (c : R) (hc : c ≠ 0) (li : X →ₗᵢ[R] Y), (f' : X → Y) = c • li
+
+variables {E F : Type*} [inner_product_space ℝ E] [inner_product_space ℝ F]
+  {X Y Z : Type*} [normed_group X] [normed_group Y] [normed_group Z]
+  [normed_space ℝ X] [normed_space ℝ Y] [normed_space ℝ Z]
+  {R M N G : Type*} [nondiscrete_normed_field R]
+  [normed_group M] [normed_group N] [normed_group G]
+  [normed_space R M] [normed_space R N] [normed_space R G]
+
+lemma is_conformal_map_id : is_conformal_map (id R M) :=
+⟨1, one_ne_zero, id, by ext; simp⟩
+
+lemma is_conformal_map_const_smul {c : R} (hc : c ≠ 0) : is_conformal_map (c • (id R M)) :=
+⟨c, hc, id, by ext; simp⟩
+
+lemma is_conformal_map_iff (f' : E →L[ℝ] F) :
+  is_conformal_map f' ↔ ∃ (c : ℝ), 0 < c ∧
+  ∀ (u v : E), ⟪f' u, f' v⟫ = (c : ℝ) * ⟪u, v⟫ :=
+begin
+  split,
+  { rintros ⟨c₁, hc₁, li, h⟩,
+    refine ⟨c₁ * c₁, mul_self_pos hc₁, λ u v, _⟩,
+    simp only [h, pi.smul_apply, inner_map_map,
+               real_inner_smul_left, real_inner_smul_right, mul_assoc], },
+  { rintros ⟨c₁, hc₁, huv⟩,
+    let c := real.sqrt c₁⁻¹,
+    have hc : c ≠ 0 := λ w, by {simp only [c] at w;
+      exact (real.sqrt_ne_zero'.mpr $ inv_pos.mpr hc₁) w},
+    let f₁ := c • f',
+    have minor : (f₁ : E → F) = c • f' := rfl,
+    have minor' : (f' : E → F) = c⁻¹ • f₁ := by ext;
+      simp_rw [minor, pi.smul_apply]; rw [smul_smul, inv_mul_cancel hc, one_smul],
+    refine ⟨c⁻¹, inv_ne_zero hc, f₁.to_linear_map.isometry_of_inner (λ u v, _), minor'⟩,
+    simp_rw [to_linear_map_eq_coe, continuous_linear_map.coe_coe, minor, pi.smul_apply],
+    rw [real_inner_smul_left, real_inner_smul_right,
+        huv u v, ← mul_assoc, ← mul_assoc,
+        real.mul_self_sqrt $ le_of_lt $ inv_pos.mpr hc₁,
+        inv_mul_cancel $ ne_of_gt hc₁, one_mul], },
+end
+
+lemma is_conformal_map_of_subsingleton [h : subsingleton M] (f' : M →L[R] N) :
+  is_conformal_map f' :=
+begin
+  rw subsingleton_iff at h,
+  have minor : (f' : M → N) = function.const M 0 := by ext x'; rw h x' 0; exact f'.map_zero,
+  have key : ∀ (x' : M), ∥(0 : M →ₗ[R] N) x'∥ = ∥x'∥ := λ x',
+    by rw [linear_map.zero_apply, h x' 0]; repeat { rw norm_zero },
+  exact ⟨(1 : R), one_ne_zero, ⟨0, key⟩,
+    by rw pi.smul_def; ext p; rw [one_smul, minor]; refl⟩,
+end
+
+namespace is_conformal_map
+
+lemma comp {f' : M →L[R] N} {g' : N →L[R] G}
+  (hf' : is_conformal_map f') (hg' : is_conformal_map g') :
+  is_conformal_map (g'.comp f') :=
+begin
+  rcases hf' with ⟨cf, hcf, lif, hlif⟩,
+  rcases hg' with ⟨cg, hcg, lig, hlig⟩,
+  refine ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, funext (λ x, _)⟩,
+  simp only [coe_comp', linear_isometry.coe_comp, hlif, hlig, pi.smul_apply,
+             function.comp_app, linear_isometry.map_smul, smul_smul],
+end
+
+lemma injective {f' : M →L[R] N} (h : is_conformal_map f') : function.injective f' :=
+let ⟨c, hc, li, hf'⟩ := h in by simp only [hf', pi.smul_def];
+  exact (smul_left_injective _ hc).comp li.injective
+
+lemma preserves_angle {f' : E →L[ℝ] F} (h : is_conformal_map f') (u v : E) :
+  inner_product_geometry.angle (f' u) (f' v) = inner_product_geometry.angle u v :=
+begin
+  obtain ⟨c, hc, li, hcf⟩ := h,
+  suffices : c * (c * inner u v) / (∥c∥ * ∥u∥ * (∥c∥ * ∥v∥)) = inner u v / (∥u∥ * ∥v∥),
+  { simp [this, inner_product_geometry.angle, hcf, norm_smul, inner_smul_left, inner_smul_right] },
+  by_cases hu : ∥u∥ = 0,
+  { simp [norm_eq_zero.mp hu] },
+  by_cases hv : ∥v∥ = 0,
+  { simp [norm_eq_zero.mp hv] },
+  have hc : ∥c∥ ≠ 0 := λ w, hc (norm_eq_zero.mp w),
+  field_simp,
+  have : c * c = ∥c∥ * ∥c∥ := by simp [real.norm_eq_abs, abs_mul_abs_self],
+  convert congr_arg (λ x, x * ⟪u, v⟫ * ∥u∥ * ∥v∥) this using 1; ring,
+end
+
+end is_conformal_map

src/geometry/manifold/conformal_groupoid.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021 Yourong Zang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yourong Zang
+-/
+import analysis.calculus.conformal
+import geometry.manifold.charted_space
+
+/-!
+# Conformal Groupoid
+
+In this file we define the groupoid of conformal maps on normed spaces.
+
+## Main definitions
+
+* `conformal_groupoid`: the groupoid of conformal local homeomorphisms.
+
+## Tags
+
+conformal, groupoid
+-/
+
+variables {X : Type*} [normed_group X] [normed_space ℝ X]
+
+/-- The pregroupoid of conformal maps. -/
+def conformal_pregroupoid : pregroupoid X :=
+{ property := λ f u, ∀ x, x ∈ u → conformal_at f x,
+  comp := λ f g u v hf hg hu hv huv x hx, (hg (f x) hx.2).comp x (hf x hx.1),
+  id_mem := λ x hx, conformal_at_id x,
+  locality := λ f u hu h x hx, let ⟨v, h₁, h₂, h₃⟩ := h x hx in h₃ x ⟨hx, h₂⟩,
+  congr := λ f g u hu h hf x hx, (hf x hx).congr hx hu h, }
+
+/-- The groupoid of conformal maps. -/
+def conformal_groupoid : structure_groupoid X := conformal_pregroupoid.groupoid