feat(topology/instances/add_circle): expand API for finite-order poin…

…ts on the circle (#17986)

src/data/set/finite.lean

@@ -945,6 +945,17 @@ lemma infinite.exists_not_mem_finset {s : set α} (hs : s.infinite) (f : finset
 let ⟨a, has, haf⟩ := (hs.diff (to_finite f)).nonempty
 in ⟨a, has, λ h, haf $ finset.mem_coe.1 h⟩
 
+lemma not_inj_on_infinite_finite_image {f : α → β} {s : set α}
+  (h_inf : s.infinite) (h_fin : (f '' s).finite) :
+  ¬ inj_on f s :=
+begin
+  haveI : finite (f '' s) := finite_coe_iff.mpr h_fin,
+  haveI : infinite s := infinite_coe_iff.mpr h_inf,
+  have := not_injective_infinite_finite
+    ((f '' s).cod_restrict (s.restrict f) $ λ x, ⟨x, x.property, rfl⟩),
+  contrapose! this,
+  rwa [injective_cod_restrict, ← inj_on_iff_injective],
+end
 
 /-! ### Order properties -/
 

src/data/set/intervals/infinite.lean

@@ -52,7 +52,7 @@ instance [no_min_order α] {a : α} : infinite (Iic a) := no_min_order.infinite
 lemma Iic_infinite [no_min_order α] (a : α) : (Iic a).infinite := infinite_coe_iff.1 Iic.infinite
 
 instance [no_max_order α] {a : α} : infinite (Ioi a) := no_max_order.infinite
-lemma Ioi_infinite [no_min_order α] (a : α) : (Iio a).infinite := infinite_coe_iff.1 Iio.infinite
+lemma Ioi_infinite [no_max_order α] (a : α) : (Ioi a).infinite := infinite_coe_iff.1 Ioi.infinite
 
 instance [no_max_order α] {a : α} : infinite (Ici a) := no_max_order.infinite
 lemma Ici_infinite [no_max_order α] (a : α) : (Ici a).infinite := infinite_coe_iff.1 Ici.infinite

src/group_theory/order_of_element.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Julian Kuelshammer
 import algebra.hom.iterate
 import data.nat.modeq
 import data.set.pointwise.basic
+import data.set.intervals.infinite
 import dynamics.periodic_pts
 import group_theory.index
 
@@ -68,6 +69,19 @@ lemma is_of_fin_order_iff_pow_eq_one (x : G) :
   is_of_fin_order x ↔ ∃ n, 0 < n ∧ x ^ n = 1 :=
 by { convert iff.rfl, simp [is_periodic_pt_mul_iff_pow_eq_one] }
 
+/-- See also `injective_pow_iff_not_is_of_fin_order`. -/
+@[to_additive not_is_of_fin_add_order_of_injective_nsmul "See also
+`injective_nsmul_iff_not_is_of_fin_add_order`."]
+lemma not_is_of_fin_order_of_injective_pow {x : G} (h : injective (λ (n : ℕ), x^n)) :
+  ¬ is_of_fin_order x :=
+begin
+  simp_rw [is_of_fin_order_iff_pow_eq_one, not_exists, not_and],
+  intros n hn_pos hnx,
+  rw ← pow_zero x at hnx,
+  rw h hnx at hn_pos,
+  exact irrefl 0 hn_pos,
+end
+
 /-- Elements of finite order are of finite order in submonoids.-/
 @[to_additive is_of_fin_add_order_iff_coe "Elements of finite order are of finite order in
 submonoids."]
@@ -380,9 +394,11 @@ lemma mem_powers_iff_mem_range_order_of' [decidable_eq G] (hx : 0 < order_of x)
   y ∈ submonoid.powers x ↔ y ∈ (finset.range (order_of x)).image ((^) x : ℕ → G) :=
 finset.mem_range_iff_mem_finset_range_of_mod_eq' hx (λ i, pow_eq_mod_order_of.symm)
 
+@[to_additive]
 lemma pow_eq_one_iff_modeq : x ^ n = 1 ↔ n ≡ 0 [MOD (order_of x)] :=
 by rw [modeq_zero_iff_dvd, order_of_dvd_iff_pow_eq_one]
 
+@[to_additive]
 lemma pow_eq_pow_iff_modeq : x ^ n = x ^ m ↔ n ≡ m [MOD (order_of x)] :=
 begin
   wlog hmn : m ≤ n,
@@ -391,6 +407,34 @@ begin
   exact ⟨λ h, nat.modeq.add_left _ h, λ h, nat.modeq.add_left_cancel' _ h⟩,
 end
 
+@[simp, to_additive injective_nsmul_iff_not_is_of_fin_add_order]
+lemma injective_pow_iff_not_is_of_fin_order {x : G} :
+  injective (λ (n : ℕ), x^n) ↔ ¬ is_of_fin_order x :=
+begin
+  refine ⟨λ h, not_is_of_fin_order_of_injective_pow h, λ h n m hnm, _⟩,
+  rwa [pow_eq_pow_iff_modeq, order_of_eq_zero_iff.mpr h, modeq_zero_iff] at hnm,
+end
+
+@[to_additive infinite_not_is_of_fin_add_order]
+lemma infinite_not_is_of_fin_order {x : G} (h : ¬ is_of_fin_order x) :
+  {y : G | ¬ is_of_fin_order y}.infinite :=
+begin
+  let s := {n | 0 < n}.image (λ (n : ℕ), x^n),
+  have hs : s ⊆ {y : G | ¬ is_of_fin_order y},
+  { rintros - ⟨n, hn : 0 < n, rfl⟩ (contra : is_of_fin_order (x^n)),
+    apply h,
+    rw is_of_fin_order_iff_pow_eq_one at contra ⊢,
+    obtain ⟨m, hm, hm'⟩ := contra,
+    exact ⟨n * m, mul_pos hn hm, by rwa pow_mul⟩, },
+  suffices : s.infinite, { exact this.mono hs, },
+  contrapose! h,
+  have : ¬ injective (λ (n : ℕ), x^n),
+  { have := set.not_inj_on_infinite_finite_image (set.Ioi_infinite 0) (set.not_infinite.mp h),
+    contrapose! this,
+    exact set.inj_on_of_injective this _, },
+  rwa [injective_pow_iff_not_is_of_fin_order, not_not] at this,
+end
+
 end cancel_monoid
 
 section group
@@ -541,13 +585,9 @@ variables [left_cancel_monoid G] [add_left_cancel_monoid A]
 @[to_additive]
 lemma exists_pow_eq_one [finite G] (x : G) : is_of_fin_order x :=
 begin
-  refine (is_of_fin_order_iff_pow_eq_one _).mpr _,
-  obtain ⟨i, j, a_eq, ne⟩ : ∃(i j : ℕ), x ^ i = x ^ j ∧ i ≠ j :=
-    by simpa only [not_forall, exists_prop, injective]
-      using (not_injective_infinite_finite (λi:ℕ, x^i)),
-  wlog h'' : j ≤ i,
-  refine ⟨i - j, tsub_pos_of_lt (lt_of_le_of_ne h'' ne.symm), mul_right_injective (x^j) _⟩,
-  rw [mul_one, ← pow_add, ← a_eq, add_tsub_cancel_of_le h''],
+  have : (set.univ : set G).finite := set.univ.to_finite,
+  contrapose! this,
+  exact set.infinite.mono (set.subset_univ _) (infinite_not_is_of_fin_order this),
 end
 
 @[to_additive add_order_of_le_card_univ]

src/topology/instances/add_circle.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import data.nat.totient
 import algebra.ring.add_aut
 import group_theory.divisible
 import group_theory.order_of_element
@@ -67,6 +68,10 @@ lemma coe_nsmul {n : ℕ} {x : 𝕜} : (↑(n • x) : add_circle p) = n • (x
 
 lemma coe_zsmul {n : ℤ} {x : 𝕜} : (↑(n • x) : add_circle p) = n • (x : add_circle p) := rfl
 
+lemma coe_add (x y : 𝕜) : (↑(x + y) : add_circle p) = (x : add_circle p) + (y : add_circle p) := rfl
+
+lemma coe_sub (x y : 𝕜) : (↑(x - y) : add_circle p) = (x : add_circle p) - (y : add_circle p) := rfl
+
 lemma coe_neg {x : 𝕜} : (↑(-x) : add_circle p) = -(x : add_circle p) := rfl
 
 lemma coe_eq_zero_iff {x : 𝕜} : (x : add_circle p) = 0 ↔ ∃ (n : ℤ), n • p = x :=
@@ -280,6 +285,72 @@ begin
     simpa [zero_add] using (equiv_Ico p 0 u).2.2, },
 end
 
+lemma add_order_of_eq_pos_iff {u : add_circle p} {n : ℕ} (h : 0 < n) :
+  add_order_of u = n ↔ ∃ m < n, gcd m n = 1 ∧ ↑(↑m / ↑n * p) = u :=
+begin
+  refine ⟨λ hu, _, _⟩,
+  { rw ← hu at h,
+    obtain ⟨m, h₀, h₁, h₂⟩ := exists_gcd_eq_one_of_is_of_fin_add_order (add_order_of_pos_iff.mp h),
+    refine ⟨m, _, _, _⟩;
+    rwa ← hu, },
+  { rintros ⟨m, h₀, h₁, rfl⟩,
+    exact add_order_of_div_of_gcd_eq_one h h₁, },
+end
+
+variables (p)
+
+/-- The natural bijection between points of order `n` and natural numbers less than and coprime to
+`n`. The inverse of the map sends `m ↦ (m/n * p : add_circle p)` where `m` is coprime to `n` and
+satisfies `0 ≤ m < n`. -/
+def set_add_order_of_equiv {n : ℕ} (hn : 0 < n) :
+  {u : add_circle p | add_order_of u = n} ≃ {m | m < n ∧ gcd m n = 1} :=
+{ to_fun := λ u, by
+  { let h := (add_order_of_eq_pos_iff hn).mp u.property,
+    exact ⟨classical.some h, classical.some (classical.some_spec h),
+      (classical.some_spec (classical.some_spec h)).1⟩, },
+  inv_fun := λ m, ⟨↑((m : 𝕜) / n * p), add_order_of_div_of_gcd_eq_one hn (m.property.2)⟩,
+  left_inv := λ u, subtype.ext
+    (classical.some_spec (classical.some_spec $ (add_order_of_eq_pos_iff hn).mp u.2)).2,
+  right_inv :=
+  begin
+    rintros ⟨m, hm₁, hm₂⟩,
+    let u : {u : add_circle p | add_order_of u = n} :=
+      ⟨↑((m : 𝕜) / n * p), add_order_of_div_of_gcd_eq_one hn hm₂⟩,
+    let h := (add_order_of_eq_pos_iff hn).mp u.property,
+    ext,
+    let m' := classical.some h,
+    change m' = m,
+    obtain ⟨h₁ : m' < n, h₂ : gcd m' n = 1, h₃ : quotient_add_group.mk ((m' : 𝕜) / n * p) =
+      quotient_add_group.mk ((m : 𝕜) / n * p)⟩ := classical.some_spec h,
+    replace h₃ := congr_arg (coe : Ico 0 (0 + p) → 𝕜) (congr_arg (equiv_Ico p 0) h₃),
+    simpa only [coe_equiv_Ico_mk_apply, mul_left_inj' hp.out.ne', mul_div_cancel _ hp.out.ne',
+      int.fract_div_nat_cast_eq_div_nat_cast_mod,
+      div_left_inj' (nat.cast_ne_zero.mpr hn.ne' : (n : 𝕜) ≠ 0), nat.cast_inj,
+      (nat.mod_eq_iff_lt hn.ne').mpr hm₁, (nat.mod_eq_iff_lt hn.ne').mpr h₁] using h₃,
+  end }
+
+@[simp] lemma card_add_order_of_eq_totient {n : ℕ} :
+  nat.card {u : add_circle p // add_order_of u = n} = n.totient :=
+begin
+  rcases n.eq_zero_or_pos with rfl | hn,
+  { simp only [nat.totient_zero, add_order_of_eq_zero_iff],
+    rcases em (∃ (u : add_circle p), ¬ is_of_fin_add_order u) with ⟨u, hu⟩ | h,
+    { haveI : infinite {u : add_circle p // ¬is_of_fin_add_order u},
+      { erw infinite_coe_iff,
+        exact infinite_not_is_of_fin_add_order hu, },
+      exact nat.card_eq_zero_of_infinite, },
+    { haveI : is_empty {u : add_circle p // ¬is_of_fin_add_order u}, { simpa using h, },
+      exact nat.card_of_is_empty, }, },
+  { rw [← coe_set_of, nat.card_congr (set_add_order_of_equiv p hn),
+      n.totient_eq_card_lt_and_coprime],
+    simpa only [@nat.coprime_comm _ n], },
+end
+
+lemma finite_set_of_add_order_eq {n : ℕ} (hn : 0 < n) :
+  {u : add_circle p | add_order_of u = n}.finite :=
+finite_coe_iff.mp $ nat.finite_of_card_ne_zero $ by simpa only [coe_set_of,
+  card_add_order_of_eq_totient p] using (nat.totient_pos hn).ne'
+
 end finite_order_points
 
 end linear_ordered_field