[Merged by Bors] - feat(Analysis/SpecialFunctions/Complex/Circle): expMapCircle as a PartialHomeomorph and prove IsLocalHomeomorph

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -195,4 +195,45 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) :=
   linarith
 #align add_circle.injective_to_circle AddCircle.injective_toCircle
 
+private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle :=
+  { toFun := Real.Angle.expMapCircle
+    invFun := fun x ↦ arg x
+    left_inv := Real.Angle.arg_expMapCircle
+    right_inv := expMapCircle_arg
+    continuous_toFun := continuous_coinduced_dom.mpr expMapCircle.continuous
+    continuous_invFun := by
+      let f : circle → Real.Angle := fun x ↦ arg x
+      change Continuous f
+      have hf : ∀ x y, f (x * y) = f x + f y := by
+        intro x y
+        conv_lhs => rw [← expMapCircle_arg x, ← expMapCircle_arg y, ← expMapCircle_add]
+        exact Real.Angle.arg_expMapCircle (arg x + arg y)
+      rw [continuous_iff_continuousAt]
+      intro x
+      have hg : f = (fun y ↦ y - f x⁻¹) ∘ f ∘ (fun y ↦ y * x⁻¹) := by
+        ext y
+        rw [comp_apply, comp_apply, hf, add_sub_cancel_right]
+      rw [hg]
+      exact (continuous_sub_right (f x⁻¹)).continuousAt.comp
+        (((continuousAt_arg_coe_angle (ne_zero_of_mem_circle _)).comp
+        (continuousAt_subtype_val)).comp
+        (continuous_mul_right x⁻¹).continuousAt) }
+
+/-- 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
+  change expMapCircle _ = expMapCircle _
+  congr; simp; ring
+
 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

@@ -11,6 +11,7 @@ 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"
 
@@ -267,6 +268,36 @@ 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. -/
+def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : PartialHomeomorph 𝕜 (AddCircle p) :=
+  { 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, hb⟩ := nonempty_Ioo_subtype (sub_lt_self a hp.out)
+  exact ⟨partialHomeomorphCoe p b, ⟨hb.2, lt_add_of_sub_right_lt hb.1⟩, rfl⟩
+
 end Continuity
 
 /-- The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is
@@ -317,6 +348,12 @@ 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 equivalence 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 _⟩
+
 variable [hp : Fact (0 < p)]
 
 section FloorRing