refactor(geometry/manifold/instances/circle): split out (topological)…

… group facts (#7951)

Move the group and topological group facts about the unit circle in `ℂ` from `geometry.manifold.instances.circle` to a new file `analysis.complex.circle`.  Delete `geometry.manifold.instances.circle`, moving the remaining material to a section in `geometry.manifold.instances.sphere`.

src/geometry/manifold/instances/circle.lean → src/analysis/complex/circle.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import geometry.manifold.instances.sphere
+import analysis.special_functions.exp_log
 
 /-!
 # The circle
@@ -14,29 +14,24 @@ radius `1`.  We equip it with the following structure:
 * a submonoid of `ℂ`
 * a group
 * a topological group
-* a charted space with model space `euclidean_space ℝ (fin 1)` (inherited from `metric.sphere`)
-* a Lie group with model with corners `𝓡 1`
 
 We furthermore define `exp_map_circle` to be the natural map `λ t, exp (t * I)` from `ℝ` to
-`circle`, and show that this map is a group homomorphism and is smooth.
+`circle`, and show that this map is a group homomorphism.
 
 ## Implementation notes
 
-To borrow the smooth manifold structure cleanly, the circle needs to be defined using
-`metric.sphere`, and therefore the underlying set is `{z : ℂ | abs (z - 0) = 1}`.  This prevents
-certain algebraic facts from working definitionally -- for example, the circle is not defeq to
-`{z : ℂ | abs z = 1}`, which is the kernel of `complex.abs` considered as a homomorphism from `ℂ`
-to `ℝ`, nor is it defeq to `{z : ℂ | norm_sq z = 1}`, which is the kernel of the homomorphism
-`complex.norm_sq` from `ℂ` to `ℝ`.
+Because later (in `geometry.manifold.instances.sphere`) one wants to equip the circle with a smooth
+manifold structure borrowed from `metric.sphere`, the underlying set is
+`{z : ℂ | abs (z - 0) = 1}`.  This prevents certain algebraic facts from working definitionally --
+for example, the circle is not defeq to `{z : ℂ | abs z = 1}`, which is the kernel of `complex.abs`
+considered as a homomorphism from `ℂ` to `ℝ`, nor is it defeq to `{z : ℂ | norm_sq z = 1}`, which
+is the kernel of the homomorphism `complex.norm_sq` from `ℂ` to `ℝ`.
 
 -/
 
 noncomputable theory
 
-open complex finite_dimensional metric
-open_locale manifold
-
-local attribute [instance] finrank_real_complex_fact
+open complex metric
 
 /-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`. -/
 def circle : submonoid ℂ :=
@@ -88,28 +83,6 @@ instance : topological_group circle :=
   continuous_inv := continuous_induced_rng $
     complex.conj_clm.continuous.comp continuous_subtype_coe }
 
-/-- The unit circle in `ℂ` is a charted space modelled on `euclidean_space ℝ (fin 1)`.  This
-follows by definition from the corresponding result for `metric.sphere`. -/
-instance : charted_space (euclidean_space ℝ (fin 1)) circle := metric.sphere.charted_space
-
-instance : smooth_manifold_with_corners (𝓡 1) circle :=
-metric.sphere.smooth_manifold_with_corners
-
-/-- The unit circle in `ℂ` is a Lie group. -/
-instance : lie_group (𝓡 1) circle :=
-{ smooth_mul := begin
-    let c : circle → ℂ := coe,
-    have h₁ : times_cont_mdiff _ _ _ (prod.map c c) :=
-      times_cont_mdiff_coe_sphere.prod_map times_cont_mdiff_coe_sphere,
-    have h₂ : times_cont_mdiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ∞ (λ (z : ℂ × ℂ), z.fst * z.snd),
-    { rw times_cont_mdiff_iff,
-      exact ⟨continuous_mul, λ x y, (times_cont_diff_mul.restrict_scalars ℝ).times_cont_diff_on⟩ },
-    exact (h₂.comp h₁).cod_restrict_sphere _,
-  end,
-  smooth_inv := (complex.conj_clm.times_cont_diff.times_cont_mdiff.comp
-    times_cont_mdiff_coe_sphere).cod_restrict_sphere _,
-  .. metric.sphere.smooth_manifold_with_corners }
-
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
 def exp_map_circle (t : ℝ) : circle :=
 ⟨exp (t * I), by simp [exp_mul_I, abs_cos_add_sin_mul_I]⟩
@@ -124,8 +97,3 @@ def exp_map_circle_hom : ℝ →+ (additive circle) :=
   map_zero' := by { rw exp_map_circle, convert of_mul_one, simp },
   map_add' := λ x y, show exp_map_circle (x + y) = (exp_map_circle x) * (exp_map_circle y),
     from subtype.ext $ by simp [exp_map_circle, exp_add, add_mul] }
-
-/-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ` is smooth. -/
-lemma times_cont_mdiff_exp_map_circle : times_cont_mdiff 𝓘(ℝ, ℝ) (𝓡 1) ∞ exp_map_circle :=
-(((times_cont_diff_exp.restrict_scalars ℝ).comp
-  (times_cont_diff_id.smul times_cont_diff_const)).times_cont_mdiff).cod_restrict_sphere _

src/analysis/fourier.lean

@@ -5,7 +5,7 @@ Authors: Heather Macbeth
 -/
 import measure_theory.l2_space
 import measure_theory.haar_measure
-import geometry.manifold.instances.circle
+import analysis.complex.circle
 
 /-!
 

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 geometry.manifold.instances.real
+import analysis.complex.circle
 
 /-!
 # Manifold structure on the sphere
@@ -21,7 +22,7 @@ For finite-dimensional `E`, we then construct a smooth manifold instance on the
 here are obtained by composing the local homeomorphisms `stereographic` with arbitrary isometries
 from `(ℝ ∙ v)ᗮ` to Euclidean space.
 
-Finally, two lemmas about smooth maps:
+We prove two lemmas about smooth maps:
 * `times_cont_mdiff_coe_sphere` states that the coercion map from the sphere into `E` is smooth;
   this is a useful tool for constructing smooth maps *from* the sphere.
 * `times_cont_mdiff.cod_restrict_sphere` states that a map from a manifold into the sphere is
@@ -30,6 +31,15 @@ Finally, two lemmas about smooth maps:
 
 As an application we prove `times_cont_mdiff_neg_sphere`, that the antipodal map is smooth.
 
+Finally, we equip the `circle` (defined in `analysis.complex.circle` to be the sphere in `ℂ`
+centred at `0` of radius `1`) with the following structure:
+* a charted space with model space `euclidean_space ℝ (fin 1)` (inherited from `metric.sphere`)
+* a Lie group with model with corners `𝓡 1`
+
+We furthermore show that `exp_map_circle` (defined in `analysis.complex.circle` to be the natural
+map `λ t, exp (t * I)` from `ℝ` to `circle`) is smooth.
+
+
 ## Implementation notes
 
 The model space for the charted space instance is `euclidean_space ℝ (fin n)`, where `n` is a
@@ -377,3 +387,38 @@ lemma times_cont_mdiff_neg_sphere {n : ℕ} [fact (finrank ℝ E = n + 1)] :
 (times_cont_diff_neg.times_cont_mdiff.comp times_cont_mdiff_coe_sphere).cod_restrict_sphere _
 
 end smooth_manifold
+
+section circle
+
+open complex
+
+local attribute [instance] finrank_real_complex_fact
+
+/-- The unit circle in `ℂ` is a charted space modelled on `euclidean_space ℝ (fin 1)`.  This
+follows by definition from the corresponding result for `metric.sphere`. -/
+instance : charted_space (euclidean_space ℝ (fin 1)) circle := metric.sphere.charted_space
+
+instance : smooth_manifold_with_corners (𝓡 1) circle :=
+metric.sphere.smooth_manifold_with_corners
+
+/-- The unit circle in `ℂ` is a Lie group. -/
+instance : lie_group (𝓡 1) circle :=
+{ smooth_mul := begin
+    let c : circle → ℂ := coe,
+    have h₁ : times_cont_mdiff _ _ _ (prod.map c c) :=
+      times_cont_mdiff_coe_sphere.prod_map times_cont_mdiff_coe_sphere,
+    have h₂ : times_cont_mdiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ∞ (λ (z : ℂ × ℂ), z.fst * z.snd),
+    { rw times_cont_mdiff_iff,
+      exact ⟨continuous_mul, λ x y, (times_cont_diff_mul.restrict_scalars ℝ).times_cont_diff_on⟩ },
+    exact (h₂.comp h₁).cod_restrict_sphere _,
+  end,
+  smooth_inv := (complex.conj_clm.times_cont_diff.times_cont_mdiff.comp
+    times_cont_mdiff_coe_sphere).cod_restrict_sphere _,
+  .. metric.sphere.smooth_manifold_with_corners }
+
+/-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ` is smooth. -/
+lemma times_cont_mdiff_exp_map_circle : times_cont_mdiff 𝓘(ℝ, ℝ) (𝓡 1) ∞ exp_map_circle :=
+(((times_cont_diff_exp.restrict_scalars ℝ).comp
+  (times_cont_diff_id.smul times_cont_diff_const)).times_cont_mdiff).cod_restrict_sphere _
+
+end circle