[Merged by Bors] - feat(analysis/normed/group/add_circle): results about finite-order points on the circle

src/algebra/order/floor.lean

@@ -678,6 +678,45 @@ sub_nonneg_of_le $ (le_div_iff hb).1 $ floor_le _
 lemma sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
 sub_lt_iff_lt_add.2 $ by { rw [←one_add_mul, ←div_lt_iff hb, add_comm], exact lt_floor_add_one _ }
 
+lemma fract_div_nat_cast_eq_div_nat_cast_mod {m n : ℕ} :
+  fract ((m : k) / n) = ↑(m % n) / n :=
+begin
+  rcases n.eq_zero_or_pos with rfl | hn, { simp, },
+  have hn' : 0 < (n : k), { norm_cast, assumption, },
+  refine fract_eq_iff.mpr ⟨by positivity, _, m / n, _⟩,
+  { simpa only [div_lt_one hn', nat.cast_lt] using m.mod_lt hn, },
+  { rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne.symm, mul_div_cancel' _ hn'.ne.symm, mul_add,
+      mul_div_cancel' _ hn'.ne.symm],
+    norm_cast,
+    rw [← nat.cast_add, nat.mod_add_div m n], },
+end
+
+-- TODO Generalise this to allow `n : ℤ` using `int.fmod` instead of `int.mod`.
+lemma fract_div_int_cast_eq_div_int_cast_mod {m : ℤ} {n : ℕ} :
+  fract ((m : k) / n) = ↑(m % n) / n :=
+begin
+  rcases n.eq_zero_or_pos with rfl | hn, { simp, },
+  replace hn : 0 < (n : k), { norm_cast, assumption, },
+  have : ∀ {l : ℤ} (hl : 0 ≤ l), fract ((l : k) / n) = ↑(l % n) / n,
+  { intros,
+    obtain ⟨l₀, rfl | rfl⟩ := l.eq_coe_or_neg,
+    { rw [cast_coe_nat, ← coe_nat_mod, cast_coe_nat, fract_div_nat_cast_eq_div_nat_cast_mod], },
+    { rw [right.nonneg_neg_iff, coe_nat_nonpos_iff] at hl, simp [hl, zero_mod], }, },
+  obtain ⟨m₀, rfl | rfl⟩ := m.eq_coe_or_neg, { exact this (of_nat_nonneg m₀), },
+  let q := ⌈↑m₀ / (n : k)⌉,
+  let m₁ := (q * ↑n) -(↑m₀ : ℤ),
+  have hm₁ : 0 ≤ m₁, { simpa [←@cast_le k, ←div_le_iff hn] using floor_ring.gc_ceil_coe.le_u_l _, },
+  calc fract (↑-↑m₀ / ↑n) = fract (-(m₀ : k) / n) : by rw [coe_neg, cast_coe_nat]
+                      ... = fract ((m₁ : k) / n) : _
+                      ... = ↑(m₁ % (n : ℤ)) / ↑n : this hm₁
+                      ... = ↑(-(↑m₀ : ℤ) % ↑n) / ↑n : _,
+  { rw [← fract_int_add q, ← mul_div_cancel (q : k) (ne_of_gt hn), ← add_div, ← sub_eq_add_neg,
+      coe_sub, coe_mul, cast_coe_nat, cast_coe_nat], },
+  { congr' 2,
+    change ((q * ↑n) -(↑m₀ : ℤ)) % ↑n = _,
+    rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_mod_self], },
+end
+
 end linear_ordered_field
 
 /-! #### Ceil -/
@@ -925,6 +964,16 @@ begin
   split; linarith
 end
 
+lemma abs_sub_round_div_nat_cast_eq {m n : ℕ} :
+  |(m : α) / n - round ((m : α) / n)| = ↑(min (m % n) (n - m % n)) / n :=
+begin
+  rcases n.eq_zero_or_pos with rfl | hn, { simp, },
+  have hn' : 0 < (n : α), { norm_cast, assumption, },
+  rw [abs_sub_round_eq_min, nat.cast_min, ← min_div_div_right hn'.le,
+    fract_div_nat_cast_eq_div_nat_cast_mod, nat.cast_sub (m.mod_lt hn).le, sub_div,
+    div_self hn'.ne.symm],
+end
+
 end linear_ordered_field
 
 end round

src/analysis/normed/group/add_circle.lean

@@ -109,6 +109,13 @@ begin
     simp, },
 end
 
+lemma norm_eq' (hp : 0 < p) {x : ℝ} :
+  ‖(x : add_circle p)‖ = p * |(p⁻¹ * x) - round (p⁻¹ * x)| :=
+begin
+  conv_rhs { congr, rw ← abs_eq_self.mpr hp.le, },
+  rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p],
+end
+
 lemma norm_le_half_period {x : add_circle p} (hp : p ≠ 0) : ‖x‖ ≤ |p|/2 :=
 begin
   obtain ⟨x⟩ := x,
@@ -211,6 +218,43 @@ begin
         linarith [abs_eq_neg_self.mpr hp.le] } } },
 end
 
+section finite_order_points
+
+variables {p} [hp : fact (0 < p)]
+include hp
+
+lemma norm_div_nat_cast {m n : ℕ} :
+  ‖(↑((↑m / ↑n) * p) : add_circle p)‖ = p * (↑(min (m % n) (n - m % n)) / n) :=
+begin
+  have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n, { rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm], },
+  rw [norm_eq' p hp.out, this, abs_sub_round_div_nat_cast_eq],
+end
+
+lemma exists_norm_eq_of_fin_add_order {u : add_circle p} (hu : is_of_fin_add_order u) :
+  ∃ (k : ℕ), ‖u‖ = p * (k / add_order_of u) :=
+begin
+  let n := add_order_of u,
+  change ∃ (k : ℕ), ‖u‖ = p * (k / n),
+  obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_is_of_fin_add_order hu,
+  refine ⟨min (m % n) (n - m % n), _⟩,
+  rw [← hm, norm_div_nat_cast],
+end
+
+lemma le_add_order_smul_norm_of_is_of_fin_add_order
+  {u : add_circle p} (hu : is_of_fin_add_order u) (hu' : u ≠ 0) :
+  p ≤ add_order_of u • ‖u‖ :=
+begin
+  obtain ⟨n, hn⟩ := exists_norm_eq_of_fin_add_order hu,
+  replace hu : (add_order_of u : ℝ) ≠ 0, { norm_cast, exact (add_order_of_pos_iff.mpr hu).ne.symm },
+  conv_lhs { rw ← mul_one p, },
+  rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel' _ hu,
+    mul_le_mul_left hp.out, nat.one_le_cast, nat.one_le_iff_ne_zero],
+  contrapose! hu',
+  simpa only [hu', algebra_map.coe_zero, zero_div, mul_zero, norm_eq_zero] using hn,
+end
+
+end finite_order_points
+
 end add_circle
 
 namespace unit_add_circle

src/data/nat/cast/field.lean

@@ -30,6 +30,14 @@ begin
   rw [nat.mul_div_cancel_left _ this.bot_lt, cast_mul, mul_div_cancel_left _ n_nonzero],
 end
 
+lemma cast_div_div_div_cancel_right [field α] [char_zero α] {m n d : ℕ} (hn : d ∣ n) (hm : d ∣ m) :
+  (↑(m / d) : α) / (↑(n / d) : α) = (m : α) / n :=
+begin
+  rcases eq_or_ne d 0 with rfl | hd, { simp [zero_dvd_iff.mp hm], },
+  replace hd : (d : α) ≠ 0, { norm_cast, assumption, },
+  simp [hd, hm, hn, div_div_div_cancel_right _ hd],
+end
+
 section linear_ordered_semifield
 variables [linear_ordered_semifield α]
 

src/group_theory/subgroup/basic.lean

@@ -2605,6 +2605,9 @@ iff.rfl
 @[simp] lemma zpow_mem_zpowers (g : G) (k : ℤ) : g^k ∈ zpowers g :=
 mem_zpowers_iff.mpr ⟨k, rfl⟩
 
+@[simp] lemma npow_mem_zpowers (g : G) (k : ℕ) : g^k ∈ zpowers g :=
+(zpow_coe_nat g k) ▸ zpow_mem_zpowers g k
+
 @[simp] lemma forall_zpowers {x : G} {p : zpowers x → Prop} :
   (∀ g, p g) ↔ ∀ m : ℤ, p ⟨x ^ m, m, rfl⟩ :=
 set.forall_subtype_range_iff
@@ -2641,6 +2644,7 @@ attribute [to_additive add_subgroup.range_zmultiples_hom] subgroup.range_zpowers
 attribute [to_additive add_subgroup.zmultiples_subset] subgroup.zpowers_subset
 attribute [to_additive add_subgroup.mem_zmultiples_iff] subgroup.mem_zpowers_iff
 attribute [to_additive add_subgroup.zsmul_mem_zmultiples] subgroup.zpow_mem_zpowers
+attribute [to_additive add_subgroup.nsmul_mem_zmultiples] subgroup.npow_mem_zpowers
 attribute [to_additive add_subgroup.forall_zmultiples] subgroup.forall_zpowers
 attribute [to_additive add_subgroup.forall_mem_zmultiples] subgroup.forall_mem_zpowers
 attribute [to_additive add_subgroup.exists_zmultiples] subgroup.exists_zpowers

src/topology/instances/add_circle.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import group_theory.divisible
+import group_theory.order_of_element
+import ring_theory.int.basic
 import algebra.order.floor
 import algebra.order.to_interval_mod
 import topology.instances.real
@@ -22,6 +24,8 @@ See also `circle` and `real.angle`.  For the normed group structure on `add_circ
  * `unit_add_circle`: the special case `ℝ ⧸ ℤ`
  * `add_circle.equiv_add_circle`: the rescaling equivalence `add_circle p ≃+ add_circle q`
  * `add_circle.equiv_Ico`: the natural equivalence `add_circle p ≃ Ico 0 p`
+ * `add_circle.add_order_of_div_of_gcd_eq_one`: rational points have finite order
+ * `add_circle.exists_gcd_eq_one_of_is_of_fin_add_order`: finite-order points are rational
 
 ## Implementation notes:
 
@@ -38,7 +42,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 topological_space
+open set add_subgroup topological_space
 
 variables {𝕜 : Type*}
 
@@ -54,6 +58,26 @@ section linear_ordered_field
 
 variables [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p q : 𝕜)
 
+instance : coe_is_add_monoid_hom 𝕜 (add_circle p) :=
+{ coe_zero := rfl,
+  coe_add := λ x y, rfl }
+
+lemma coe_eq_zero_iff {x : 𝕜} : (x : add_circle p) = 0 ↔ ∃ (n : ℤ), n • p = x :=
+by simp [add_subgroup.mem_zmultiples_iff]
+
+lemma coe_eq_zero_of_pos_iff (hp : 0 < p) {x : 𝕜} (hx : 0 < x) :
+  (x : add_circle p) = 0 ↔ ∃ (n : ℕ), n • p = x :=
+begin
+  rw coe_eq_zero_iff,
+  split;
+  rintros ⟨n, rfl⟩,
+  { replace hx : 0 < n,
+    { contrapose! hx,
+      simpa only [←neg_nonneg, ←zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx) },
+    exact ⟨n.to_nat, by rw [← coe_nat_zsmul, int.to_nat_of_nonneg hx.le]⟩, },
+  { exact ⟨(n : ℤ), by simp⟩, },
+end
+
 @[continuity, nolint unused_arguments] protected lemma continuous_mk' :
   continuous (quotient_add_group.mk' (zmultiples p) : 𝕜 → add_circle p) :=
 continuous_coinduced_rng
@@ -80,9 +104,13 @@ rfl
   (equiv_add_circle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) :=
 rfl
 
-variables [floor_ring 𝕜] [hp : fact (0 < p)]
+variables [hp : fact (0 < p)]
 include hp
 
+section floor_ring
+
+variables [floor_ring 𝕜]
+
 /-- The natural equivalence between `add_circle p` and the half-open interval `[0, p)`. -/
 def equiv_Ico : add_circle p ≃ Ico 0 p :=
 { inv_fun := quotient_add_group.mk' _ ∘ coe,
@@ -98,7 +126,7 @@ def equiv_Ico : add_circle p ≃ Ico 0 p :=
   end }
 
 @[simp] lemma coe_equiv_Ico_mk_apply (x : 𝕜) :
-  (equiv_Ico p $ quotient_add_group.mk x : 𝕜) = fract (x / p) * p :=
+  (equiv_Ico p $ quotient_add_group.mk x : 𝕜) = int.fract (x / p) * p :=
 to_Ico_mod_eq_fract_mul _ x
 
 @[continuity] lemma continuous_equiv_Ico_symm : continuous (equiv_Ico p).symm :=
@@ -126,6 +154,103 @@ instance : divisible_by (add_circle p) ℤ :=
     exact (equiv_Ico p).symm_apply_apply x,
   end, }
 
+end floor_ring
+
+section finite_order_points
+
+variables {p}
+
+lemma add_order_of_div_of_gcd_eq_one {m n : ℕ} (hn : 0 < n) (h : gcd m n = 1) :
+  add_order_of (↑(↑m / ↑n * p) : add_circle p) = n :=
+begin
+  rcases m.eq_zero_or_pos with rfl | hm, { rw [gcd_zero_left, normalize_eq] at h, simp [h], },
+  set x : add_circle p := ↑(↑m / ↑n * p),
+  have hn₀ : (n : 𝕜) ≠ 0, { norm_cast, exact ne_of_gt hn, },
+  have hnx : n • x = 0,
+  { rw [← _root_.coe_nsmul, nsmul_eq_mul, ← mul_assoc, mul_div, mul_div_cancel_left _ hn₀,
+      ← nsmul_eq_mul, quotient_add_group.eq_zero_iff],
+    exact nsmul_mem_zmultiples p m, },
+  apply nat.dvd_antisymm (add_order_of_dvd_of_nsmul_eq_zero hnx),
+  suffices : ∃ (z : ℕ), z * n = (add_order_of x) * m,
+  { obtain ⟨z, hz⟩ := this,
+    simpa only [h, mul_one, gcd_comm n] using dvd_mul_gcd_of_dvd_mul (dvd.intro_left z hz), },
+  replace hp := hp.out,
+  have : 0 < add_order_of x • (↑m / ↑n * p) := smul_pos
+    (add_order_of_pos' $ (is_of_fin_add_order_iff_nsmul_eq_zero _).2 ⟨n, hn, hnx⟩) (by positivity),
+  obtain ⟨z, hz⟩ := (coe_eq_zero_of_pos_iff p hp this).mp (add_order_of_nsmul_eq_zero x),
+  rw [← smul_mul_assoc, nsmul_eq_mul, nsmul_eq_mul, mul_left_inj' hp.ne.symm, mul_div,
+    eq_div_iff hn₀] at hz,
+  norm_cast at hz,
+  exact ⟨z, hz⟩,
+end
+
+lemma add_order_of_div_of_gcd_eq_one' {m : ℤ} {n : ℕ} (hn : 0 < n) (h : gcd m.nat_abs n = 1) :
+  add_order_of (↑(↑m / ↑n * p) : add_circle p) = n :=
+begin
+  induction m,
+  { simp only [int.of_nat_eq_coe, int.cast_coe_nat, int.nat_abs_of_nat] at h ⊢,
+    exact add_order_of_div_of_gcd_eq_one hn h, },
+  { simp only [int.cast_neg_succ_of_nat, neg_div, neg_mul, _root_.coe_neg, order_of_neg],
+    exact add_order_of_div_of_gcd_eq_one hn h, },
+end
+
+lemma add_order_of_coe_rat {q : ℚ} : add_order_of (↑(↑q * p) : add_circle p) = q.denom :=
+begin
+  have : (↑(q.denom : ℤ) : 𝕜) ≠ 0, { norm_cast, exact q.pos.ne.symm, },
+  rw [← @rat.num_denom q, rat.cast_mk_of_ne_zero _ _ this, int.cast_coe_nat, rat.num_denom,
+    add_order_of_div_of_gcd_eq_one' q.pos q.cop],
+  apply_instance,
+end
+
+variables (p)
+
+lemma gcd_mul_add_order_of_div_eq {n : ℕ} (m : ℕ) (hn : 0 < n) :
+  gcd m n * add_order_of (↑(↑m / ↑n * p) : add_circle p) = n :=
+begin
+  let n' := n / gcd m n,
+  let m' := m / gcd m n,
+  have h₀ : 0 < gcd m n,
+  { rw zero_lt_iff at hn ⊢, contrapose! hn, exact ((gcd_eq_zero_iff m n).mp hn).2, },
+  have hk' : 0 < n' := nat.div_pos (nat.le_of_dvd hn $ gcd_dvd_right m n) h₀,
+  have hgcd : gcd m' n' = 1 := nat.coprime_div_gcd_div_gcd h₀,
+  simp only [mul_left_inj' hp.out.ne.symm,
+    ← nat.cast_div_div_div_cancel_right (gcd_dvd_right m n) (gcd_dvd_left m n),
+    add_order_of_div_of_gcd_eq_one hk' hgcd, mul_comm _ n', nat.div_mul_cancel (gcd_dvd_right m n)],
+end
+
+variables {p} [floor_ring 𝕜]
+
+lemma exists_gcd_eq_one_of_is_of_fin_add_order {u : add_circle p} (h : is_of_fin_add_order u) :
+  ∃ m, gcd m (add_order_of u) = 1 ∧
+       m < (add_order_of u) ∧
+       ↑(((m : 𝕜) / add_order_of u) * p) = u :=
+begin
+  rcases eq_or_ne u 0 with rfl | hu, { exact ⟨0, by simp⟩, },
+  set n := add_order_of u,
+  change ∃ m, gcd m n = 1 ∧ m < n ∧ ↑((↑m / ↑n) * p) = u,
+  have hn : 0 < n := add_order_of_pos' h,
+  have hn₀ : (n : 𝕜) ≠ 0, { norm_cast, exact ne_of_gt hn, },
+  let x := (equiv_Ico p u : 𝕜),
+  have hxu : (x : add_circle p) = u := (equiv_Ico p).symm_apply_apply u,
+  have hx₀ : 0 < (add_order_of (x : add_circle p)), { rw ← hxu at h, exact add_order_of_pos' h, },
+  have hx₁ : 0 < x,
+  { refine lt_of_le_of_ne (equiv_Ico p u).2.1 _,
+    contrapose! hu,
+    rw [← hxu, ← hu, quotient_add_group.coe_zero], },
+  obtain ⟨m, hm : m • p = add_order_of ↑x • x⟩ := (coe_eq_zero_of_pos_iff p hp.out
+    (by positivity)).mp (add_order_of_nsmul_eq_zero (x : add_circle p)),
+  replace hm : ↑m * p = ↑n * x, { simpa only [hxu, nsmul_eq_mul] using hm, },
+  have hux : ↑(↑m / ↑n * p) = u,
+  { rw [← hxu, ← mul_div_right_comm, hm, mul_comm _ x, mul_div_cancel x hn₀], },
+  refine ⟨m, (_ : gcd m n = 1), (_ : m < n), hux⟩,
+  { have := gcd_mul_add_order_of_div_eq p m hn,
+    rwa [hux, nat.mul_left_eq_self_iff hn] at this, },
+  { have : n • x < n • p := smul_lt_smul_of_pos (equiv_Ico p u).2.2 hn,
+    rwa [nsmul_eq_mul, nsmul_eq_mul, ← hm, mul_lt_mul_right hp.out, nat.cast_lt] at this, },
+end
+
+end finite_order_points
+
 end linear_ordered_field
 
 variables (p : ℝ)