From 0fbd703b3da57ec0476dc1bc06931994055ae2f5 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue, 11 Oct 2022 09:55:42 +0000
Subject: [PATCH] =?UTF-8?q?feat(topology/instances/add=5Fcircle):=20the=20?=
 =?UTF-8?q?additive=20circle=20`=E2=84=9D=20/=20(a=20=E2=88=99=20=E2=84=A4?=
 =?UTF-8?q?)`=20is=20normal=20(T4)=20and=20second-countable=20(#16594)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The T4 fact is in mathlib already, via the `normed_add_comm_group` instance on `ℝ / (a ∙ ℤ)`, but this gives it earlier in the hierarchy.

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>
---
 src/topology/instances/add_circle.lean | 56 +++++++++++++++++---------
 1 file changed, 36 insertions(+), 20 deletions(-)

diff --git a/src/topology/instances/add_circle.lean b/src/topology/instances/add_circle.lean
index cc7d4a0d9c703..dbc36f21a8f70 100644
--- a/src/topology/instances/add_circle.lean
+++ b/src/topology/instances/add_circle.lean
@@ -38,7 +38,7 @@ the rational circle `add_circle (1 : ℚ)`, and so we set things up more general
 
 noncomputable theory
 
-open set int (hiding mem_zmultiples_iff) add_subgroup
+open set int (hiding mem_zmultiples_iff) add_subgroup topological_space
 
 variables {𝕜 : Type*}
 
@@ -80,55 +80,71 @@ rfl
   (equiv_add_circle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) :=
 rfl
 
-variables [floor_ring 𝕜]
+variables [floor_ring 𝕜] [hp : fact (0 < p)]
+include hp
 
 /-- The natural equivalence between `add_circle p` and the half-open interval `[0, p)`. -/
-def equiv_Ico (hp : 0 < p) : add_circle p ≃ Ico 0 p :=
+def equiv_Ico : add_circle p ≃ Ico 0 p :=
 { inv_fun := quotient_add_group.mk' _ ∘ coe,
-  to_fun := λ x, ⟨(to_Ico_mod_periodic 0 hp).lift x, quot.induction_on x $ to_Ico_mod_mem_Ico' hp⟩,
+  to_fun := λ x, ⟨(to_Ico_mod_periodic 0 hp.out).lift x,
+    quot.induction_on x $ to_Ico_mod_mem_Ico' hp.out⟩,
   right_inv := by { rintros ⟨x, hx⟩, ext, simp [to_Ico_mod_eq_self, hx.1, hx.2], },
   left_inv :=
   begin
     rintros ⟨x⟩,
-    change quotient_add_group.mk (to_Ico_mod 0 hp x) = quotient_add_group.mk x,
+    change quotient_add_group.mk (to_Ico_mod 0 hp.out x) = quotient_add_group.mk x,
     rw [quotient_add_group.eq', neg_add_eq_sub, self_sub_to_Ico_mod, zsmul_eq_mul],
     apply int_cast_mul_mem_zmultiples,
   end }
 
-@[simp] lemma coe_equiv_Ico_mk_apply (hp : 0 < p) (x : 𝕜) :
-  (equiv_Ico p hp $ quotient_add_group.mk x : 𝕜) = fract (x / p) * p :=
-to_Ico_mod_eq_fract_mul hp x
+@[simp] lemma coe_equiv_Ico_mk_apply (x : 𝕜) :
+  (equiv_Ico p $ quotient_add_group.mk x : 𝕜) = fract (x / p) * p :=
+to_Ico_mod_eq_fract_mul _ x
 
-@[continuity] lemma continuous_equiv_Ico_symm (hp : 0 < p) : continuous (equiv_Ico p hp).symm :=
+@[continuity] lemma continuous_equiv_Ico_symm : continuous (equiv_Ico p).symm :=
 continuous_coinduced_rng.comp continuous_induced_dom
 
 /-- The image of the closed interval `[0, p]` under the quotient map `𝕜 → add_circle p` is the
 entire space. -/
-@[simp] lemma coe_image_Icc_eq (hp : 0 < p) :
+@[simp] lemma coe_image_Icc_eq :
   (coe : 𝕜 → add_circle p) '' (Icc 0 p) = univ :=
 begin
   refine eq_univ_iff_forall.mpr (λ x, _),
-  let y := equiv_Ico p hp x,
-  exact ⟨y, ⟨y.2.1, y.2.2.le⟩, (equiv_Ico p hp).symm_apply_apply x⟩,
+  let y := equiv_Ico p x,
+  exact ⟨y, ⟨y.2.1, y.2.2.le⟩, (equiv_Ico p).symm_apply_apply x⟩,
 end
 
 end linear_ordered_field
 
 variables (p : ℝ)
 
-lemma compact_space (hp : 0 < p) : compact_space $ add_circle p :=
+/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is compact. -/
+instance compact_space [fact (0 < p)] : compact_space $ add_circle p :=
 begin
-  rw [← is_compact_univ_iff, ← coe_image_Icc_eq p hp],
+  rw [← is_compact_univ_iff, ← coe_image_Icc_eq p],
   exact is_compact_Icc.image (add_circle.continuous_mk' p),
 end
 
-end add_circle
+/-- The action on `ℝ` by right multiplication of its the subgroup `zmultiples p` (the multiples of
+`p:ℝ`) is properly discontinuous. -/
+instance : properly_discontinuous_vadd (zmultiples p).opposite ℝ :=
+(zmultiples p).properly_discontinuous_vadd_opposite_of_tendsto_cofinite
+  (add_subgroup.tendsto_zmultiples_subtype_cofinite p)
 
-/-- The unit circle `ℝ ⧸ ℤ`. -/
-abbreviation unit_add_circle := add_circle (1 : ℝ)
+/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is Hausdorff. -/
+instance : t2_space (add_circle p) := t2_space_of_properly_discontinuous_vadd_of_t2_space
+
+/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is normal. -/
+instance [fact (0 < p)] : normal_space (add_circle p) := normal_of_compact_t2
 
-namespace unit_add_circle
+/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is second-countable. -/
+instance : second_countable_topology (add_circle p) := quotient_add_group.second_countable_topology
 
-instance : compact_space unit_add_circle := add_circle.compact_space _ zero_lt_one
+end add_circle
+
+private lemma fact_zero_lt_one : fact ((0:ℝ) < 1) := ⟨zero_lt_one⟩
+local attribute [instance] fact_zero_lt_one
 
-end unit_add_circle
+/-- The unit circle `ℝ ⧸ ℤ`. -/
+@[derive [compact_space, normal_space, second_countable_topology]]
+abbreviation unit_add_circle := add_circle (1 : ℝ)