feat(Analysis/SpecialFunctions/Complex/Circle): expMapCircle as a PartialHomeomorph and prove IsLocalHomeomorph (#11334)

This PR proves `IsLocalHomeomorph expMapCircle` (eventually this should be upgraded to `IsCoveringMap`, but that's a good deal harder and is probably best done via general theory such as in #7596).

Author: tb65536

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -170,12 +170,14 @@ noncomputable def toCircle : AddCircle T → circle :=
   (@scaled_exp_map_periodic T).lift
 #align add_circle.to_circle AddCircle.toCircle
 
+theorem toCircle_apply_mk (x : ℝ) : @toCircle T x = expMapCircle (2 * π / T * x) :=
+  rfl
+
 theorem toCircle_add (x : AddCircle T) (y : AddCircle T) :
     @toCircle T (x + y) = toCircle x * toCircle y := by
   induction x using QuotientAddGroup.induction_on'
   induction y using QuotientAddGroup.induction_on'
-  rw [← QuotientAddGroup.mk_add]
-  simp_rw [toCircle, Function.Periodic.lift_coe, mul_add, expMapCircle_add]
+  simp_rw [← coe_add, toCircle_apply_mk, mul_add, expMapCircle_add]
 #align add_circle.to_circle_add AddCircle.toCircle_add
 
 theorem continuous_toCircle : Continuous (@toCircle T) :=
@@ -186,7 +188,7 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) :=
   intro a b h
   induction a using QuotientAddGroup.induction_on'
   induction b using QuotientAddGroup.induction_on'
-  simp_rw [toCircle, Function.Periodic.lift_coe] at h
+  simp_rw [toCircle_apply_mk] at h
   obtain ⟨m, hm⟩ := expMapCircle_eq_expMapCircle.mp h.symm
   rw [QuotientAddGroup.eq]; simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul]
   use m
@@ -195,4 +197,38 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) :=
   linarith
 #align add_circle.injective_to_circle AddCircle.injective_toCircle
 
+/-- The homeomorphism between `AddCircle (2 * π)` and `circle`. -/
+@[simps] noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where
+  toFun := Angle.expMapCircle
+  invFun := fun x ↦ arg x
+  left_inv := Angle.arg_expMapCircle
+  right_inv := expMapCircle_arg
+  continuous_toFun := continuous_coinduced_dom.mpr expMapCircle.continuous
+  continuous_invFun := by
+    rw [continuous_iff_continuousAt]
+    intro x
+    apply (continuousAt_arg_coe_angle (ne_zero_of_mem_circle x)).comp
+      continuousAt_subtype_val
+
+theorem homeomorphCircle'_apply_mk (x : ℝ) : homeomorphCircle' x = expMapCircle x :=
+  rfl
+
+/-- The homeomorphism between `AddCircle` and `circle`. -/
+noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle :=
+  (homeomorphAddCircle T (2 * π) hT (by positivity)).trans homeomorphCircle'
+
+theorem homeomorphCircle_apply (hT : T ≠ 0) (x : AddCircle T) :
+    homeomorphCircle hT x = toCircle x := by
+  induction' x using QuotientAddGroup.induction_on' with x
+  rw [homeomorphCircle, Homeomorph.trans_apply,
+    homeomorphAddCircle_apply_mk, homeomorphCircle'_apply_mk, toCircle_apply_mk]
+  ring_nf
+
 end AddCircle
+
+open AddCircle
+
+-- todo: upgrade this to `IsCoveringMap expMapCircle`.
+lemma isLocalHomeomorph_expMapCircle : IsLocalHomeomorph expMapCircle := by
+  have : Fact (0 < 2 * π) := ⟨by positivity⟩
+  exact homeomorphCircle'.isLocalHomeomorph.comp (isLocalHomeomorph_coe (2 * π))

Mathlib/Topology/Instances/AddCircle.lean

@@ -3,14 +3,12 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.Data.Nat.Totient
+import Mathlib.Algebra.Order.ToIntervalMod
 import Mathlib.Algebra.Ring.AddAut
+import Mathlib.Data.Nat.Totient
 import Mathlib.GroupTheory.Divisible
-import Mathlib.GroupTheory.OrderOfElement
-import Mathlib.Algebra.Order.Floor
-import Mathlib.Algebra.Order.ToIntervalMod
-import Mathlib.Topology.Instances.Real
 import Mathlib.Topology.Connected.PathConnected
+import Mathlib.Topology.IsLocalHomeomorph
 
 #align_import topology.instances.add_circle from "leanprover-community/mathlib"@"213b0cff7bc5ab6696ee07cceec80829ce42efec"
 
@@ -278,6 +276,37 @@ theorem continuousAt_equivIoc : ContinuousAt (equivIoc p a) x := by
   exact (continuousAt_toIocMod hp.out a hx).codRestrict _
 #align add_circle.continuous_at_equiv_Ioc AddCircle.continuousAt_equivIoc
 
+/-- The quotient map `𝕜 → AddCircle p` as a partial homeomorphism. -/
+@[simps] def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] :
+    PartialHomeomorph 𝕜 (AddCircle p) where
+  toFun := (↑)
+  invFun := fun x ↦ equivIco p a x
+  source := Ioo a (a + p)
+  target := {↑a}ᶜ
+  map_source' := by
+    intro x hx hx'
+    exact hx.1.ne' ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx)
+      (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx')
+  map_target' := by
+    intro x hx
+    exact (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left
+      (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _)
+  left_inv' :=
+    fun x hx ↦ congrArg _ ((equivIco p a).apply_symm_apply ⟨x, Ioo_subset_Ico_self hx⟩)
+  right_inv' := fun x _ ↦ (equivIco p a).symm_apply_apply x
+  open_source := isOpen_Ioo
+  open_target := isOpen_compl_singleton
+  continuousOn_toFun := (AddCircle.continuous_mk' p).continuousOn
+  continuousOn_invFun := by
+    exact ContinuousAt.continuousOn
+      (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a)
+
+lemma isLocalHomeomorph_coe [DiscreteTopology (zmultiples p)] [DenselyOrdered 𝕜] :
+    IsLocalHomeomorph ((↑) : 𝕜 → AddCircle p) := by
+  intro a
+  obtain ⟨b, hb1, hb2⟩ := exists_between (sub_lt_self a hp.out)
+  exact ⟨partialHomeomorphCoe p b, ⟨hb2, lt_add_of_sub_right_lt hb1⟩, rfl⟩
+
 end Continuity
 
 /-- The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is
@@ -328,6 +357,22 @@ theorem equivAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
   rfl
 #align add_circle.equiv_add_circle_symm_apply_mk AddCircle.equivAddCircle_symm_apply_mk
 
+/-- The rescaling homeomorphism between additive circles with different periods. -/
+def homeomorphAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q :=
+  ⟨equivAddCircle p q hp hq,
+    (continuous_quotient_mk'.comp (continuous_mul_right (p⁻¹ * q))).quotient_lift _,
+    (continuous_quotient_mk'.comp (continuous_mul_right (q⁻¹ * p))).quotient_lift _⟩
+
+@[simp]
+theorem homeomorphAddCircle_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
+    homeomorphAddCircle p q hp hq (x : 𝕜) = (x * (p⁻¹ * q) : 𝕜) :=
+  rfl
+
+@[simp]
+theorem homeomorphAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
+    (homeomorphAddCircle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) :=
+  rfl
+
 variable [hp : Fact (0 < p)]
 
 section FloorRing