refactor(group_theory/order_of_element): use minimal_period for the d…

…efinition (#7082)

This PR redefines `order_of_element` in terms of `function.minimal_period`. It furthermore introduces a predicate on elements of a finite group to be of finite order.

Co-authored by: Damiano Testa adomani@gmail.com



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Co-authored-by: adomani <adomani@gmail.com>

src/algebra/char_p/basic.lean

@@ -26,11 +26,7 @@ theorem char_p.cast_eq_zero [add_monoid R] [has_one R] (p : ℕ) [char_p R p] :
 
 @[simp] lemma char_p.cast_card_eq_zero [add_group R] [has_one R] [fintype R] :
   (fintype.card R : R) = 0 :=
-begin
-  have : fintype.card R • (1 : R) = 0 :=
-    @pow_card_eq_one (multiplicative R) _ _ (multiplicative.of_add 1),
-  simpa only [nsmul_one]
-end
+by rw [← nsmul_one, card_nsmul_eq_zero]
 
 lemma char_p.int_cast_eq_zero_iff [add_group R] [has_one R] (p : ℕ) [char_p R p]
   (a : ℤ) :

src/algebra/group/basic.lean

@@ -63,8 +63,8 @@ comp_assoc_right _ _ _
 
 end semigroup
 
-section monoid
-variables {M : Type u} [monoid M]
+section mul_one_class
+variables {M : Type u} [mul_one_class M]
 
 @[to_additive]
 lemma ite_mul_one {P : Prop} [decidable P] {a b : M} :
@@ -75,7 +75,13 @@ by { by_cases h : P; simp [h], }
 lemma eq_one_iff_eq_one_of_mul_eq_one {a b : M} (h : a * b = 1) : a = 1 ↔ b = 1 :=
 by split; { rintro rfl, simpa using h }
 
-end monoid
+@[to_additive]
+lemma one_mul_eq_id : ((*) (1 : M)) = id := funext one_mul
+
+@[to_additive]
+lemma mul_one_eq_id : (* (1 : M)) = id := funext mul_one
+
+end mul_one_class
 
 section comm_semigroup
 variables {G : Type u} [comm_semigroup G]

src/algebra/iterate_hom.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 
 import algebra.group_power
+import algebra.group_power.basic
 import logic.function.iterate
 import group_theory.perm.basic
 
@@ -134,18 +135,69 @@ end ring_hom
 lemma equiv.perm.coe_pow {α : Type*} (f : equiv.perm α) (n : ℕ) : ⇑(f ^ n) = (f^[n]) :=
 hom_coe_pow _ rfl (λ _ _, rfl) _ _
 
-@[simp] lemma mul_left_iterate [monoid M] (a : M) (n : ℕ) : ((*) a)^[n] = (*) (a^n) :=
+--what should be the namespace for this section?
+section monoid
+
+variables [monoid G] (a : G) (n : ℕ)
+
+@[simp] lemma mul_left_iterate : ((*) a)^[n] = (*) (a^n) :=
 nat.rec_on n (funext $ λ x, by simp) $ λ n ihn,
 funext $ λ x, by simp [iterate_succ, ihn, pow_succ', mul_assoc]
 
-@[simp] lemma add_left_iterate [add_monoid M] (a : M) (n : ℕ) : ((+) a)^[n] = (+) (n • a) :=
+@[simp] lemma mul_right_iterate : (* a)^[n] = (* a ^ n) :=
+begin
+  induction n with d hd,
+  { simpa },
+  { simp [← pow_succ, hd] }
+end
+
+lemma mul_right_iterate_apply_one : (* a)^[n] 1 = a ^ n :=
+by simp [mul_right_iterate]
+
+end monoid
+
+section semigroup
+
+variables [semigroup G] {a b c : G}
+
+@[to_additive]
+lemma semiconj_by.function_semiconj_mul_left (h : semiconj_by a b c) :
+  function.semiconj ((*)a) ((*)b) ((*)c) :=
+λ j, by rw [← mul_assoc, h.eq, mul_assoc]
+
+@[to_additive]
+lemma commute.function_commute_mul_left (h : commute a b) :
+  function.commute ((*)a) ((*)b) :=
+semiconj_by.function_semiconj_mul_left h
+
+@[to_additive]
+lemma semiconj_by.function_semiconj_mul_right_swap (h : semiconj_by a b c) :
+  function.semiconj (*a) (*c) (*b) :=
+λ j, by simp_rw [mul_assoc, ← h.eq]
+
+@[to_additive]
+lemma commute.function_commute_mul_right (h : commute a b) :
+  function.commute (*a) (*b) :=
+semiconj_by.function_semiconj_mul_right_swap h
+
+end semigroup
+
+--what should be the namespace for this section?
+section add_monoid
+
+variables [add_monoid M] (a : M) (n : ℕ)
+
+@[simp] lemma add_left_iterate : ((+) a)^[n] = (+) (n • a) :=
 @mul_left_iterate (multiplicative M) _ a n
 
-@[simp] lemma mul_right_iterate [monoid M] (a : M) (n : ℕ) :
-  (λ x, x * a)^[n] = (λ x, x * a^n) :=
-nat.rec_on n (funext $ λ x, by simp) $ λ n ihn,
-funext $ λ x, by simp [iterate_succ, ihn, pow_succ, mul_assoc]
+@[simp] lemma add_right_iterate : (+ a)^[n] = (+ n • a) :=
+begin
+  induction n with d hd,
+  { simp [zero_nsmul, id_def] },
+  { simp [hd, add_assoc, succ_nsmul] }
+end
+
+lemma add_right_iterate_apply_zero : (+ a)^[n] 0 = n • a :=
+by simp [add_right_iterate]
 
-@[simp] lemma add_right_iterate [add_monoid M] (a : M) (n : ℕ) :
-  (λ x, x + a)^[n] = λ x, x + (n • a) :=
-@mul_right_iterate (multiplicative M) _ a n
+end add_monoid

src/algebra/regular.lean

@@ -116,11 +116,11 @@ variable [monoid R]
 
 /--  Any power of a left-regular element is left-regular. -/
 lemma is_left_regular.pow (n : ℕ) (rla : is_left_regular a) : is_left_regular (a ^ n) :=
-by simp [is_left_regular, ← mul_left_iterate, rla.iterate n]
+by simp only [is_left_regular, ← mul_left_iterate, rla.iterate n]
 
 /--  Any power of a right-regular element is right-regular. -/
 lemma is_right_regular.pow (n : ℕ) (rra : is_right_regular a) : is_right_regular (a ^ n) :=
-by simp [is_right_regular, ← mul_right_iterate, rra.iterate n]
+by { rw [is_right_regular, ← mul_right_iterate], exact rra.iterate n }
 
 /--  Any power of a regular element is regular. -/
 lemma is_regular.pow (n : ℕ) (ra : is_regular a) : is_regular (a ^ n) :=

src/dynamics/periodic_pts.lean

@@ -6,6 +6,7 @@ Authors: Yury G. Kudryashov
 import dynamics.fixed_points.basic
 import data.set.lattice
 import data.pnat.basic
+import data.int.gcd
 
 /-!
 # Periodic points
@@ -208,6 +209,14 @@ begin
   { exact is_periodic_pt_zero f x }
 end
 
+lemma iterate_eq_mod_minimal_period : f^[n] x = (f^[n % minimal_period f x] x) :=
+begin
+  conv_lhs { rw ← nat.mod_add_div n (minimal_period f x) },
+  rw [iterate_add, mul_comm, iterate_mul, comp_app],
+  congr,
+  exact is_periodic_pt.iterate (is_periodic_pt_minimal_period _ _) _,
+end
+
 lemma minimal_period_pos_of_mem_periodic_pts (hx : x ∈ periodic_pts f) :
   0 < minimal_period f x :=
 by simp only [minimal_period, dif_pos hx, gt_iff_lt.1 (nat.find_spec hx).fst]
@@ -229,12 +238,32 @@ begin
   exact nat.find_min' (mk_mem_periodic_pts hn hx) ⟨hn, hx⟩
 end
 
+lemma minimal_period_id : minimal_period id x = 1 :=
+((is_periodic_id _ _ ).minimal_period_le nat.one_pos).antisymm
+  (nat.succ_le_of_lt ((is_periodic_id _ _ ).minimal_period_pos nat.one_pos))
+
+lemma is_fixed_point_iff_minimal_period_eq_one : minimal_period f x = 1 ↔ is_fixed_pt f x :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { rw ← iterate_one f,
+    refine function.is_periodic_pt.is_fixed_pt _,
+    rw ← h,
+    exact is_periodic_pt_minimal_period f x },
+  { exact ((h.is_periodic_pt 1).minimal_period_le nat.one_pos).antisymm
+      (nat.succ_le_of_lt ((h.is_periodic_pt 1).minimal_period_pos nat.one_pos)) }
+end
+
 lemma is_periodic_pt.eq_zero_of_lt_minimal_period (hx : is_periodic_pt f n x)
   (hn : n < minimal_period f x) :
   n = 0 :=
 eq.symm $ (eq_or_lt_of_le $ n.zero_le).resolve_right $ λ hn0,
 not_lt.2 (hx.minimal_period_le hn0) hn
 
+lemma not_is_periodic_pt_of_pos_of_lt_minimal_period :
+  ∀ {n: ℕ} (n0 : n ≠ 0) (hn : n < minimal_period f x), ¬ is_periodic_pt f n x
+| 0 n0 _ := (n0 rfl).elim
+| (n + 1) _ hn := λ hp, nat.succ_ne_zero _ (hp.eq_zero_of_lt_minimal_period hn)
+
 lemma is_periodic_pt.minimal_period_dvd (hx : is_periodic_pt f n x) :
   minimal_period f x ∣ n :=
 (eq_or_lt_of_le $ n.zero_le).elim (λ hn0, hn0 ▸ dvd_zero _) $ λ hn0,
@@ -244,7 +273,63 @@ nat.mod_lt _ $ hx.minimal_period_pos hn0
 
 lemma is_periodic_pt_iff_minimal_period_dvd :
   is_periodic_pt f n x ↔ minimal_period f x ∣ n :=
-⟨is_periodic_pt.minimal_period_dvd,
-  λ h, (is_periodic_pt_minimal_period f x).trans_dvd h⟩
+⟨is_periodic_pt.minimal_period_dvd, λ h, (is_periodic_pt_minimal_period f x).trans_dvd h⟩
+
+open nat
+
+-- This lemma is part of PR #7132
+lemma nat_dvd_iff_right {m n : ℕ} : (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n :=
+⟨λ h, nat.dvd_antisymm ((h _).mpr (dvd_refl _)) ((h _).mp (dvd_refl _)), λ h n, by rw h⟩
+
+lemma minimal_period_eq_minimal_period_iff {g : β → β} {y : β} :
+  minimal_period f x = minimal_period g y ↔ ∀ n, is_periodic_pt f n x ↔ is_periodic_pt g n y :=
+by simp_rw [is_periodic_pt_iff_minimal_period_dvd, nat_dvd_iff_right]
+
+lemma minimal_period_eq_prime {p : ℕ} [hp : fact p.prime] (hper : is_periodic_pt f p x)
+  (hfix : ¬ is_fixed_pt f x) : minimal_period f x = p :=
+(hp.out.2 _ (hper.minimal_period_dvd)).resolve_left
+  (mt is_fixed_point_iff_minimal_period_eq_one.1 hfix)
+
+lemma minimal_period_eq_prime_pow {p k : ℕ} [hp : fact p.prime] (hk : ¬ is_periodic_pt f (p ^ k) x)
+(hk1 : is_periodic_pt f (p ^ (k + 1)) x) : minimal_period f x = p ^ (k + 1) :=
+begin
+  apply nat.eq_prime_pow_of_dvd_least_prime_pow hp.out;
+  rwa ← is_periodic_pt_iff_minimal_period_dvd
+end
+
+lemma commute.minimal_period_of_comp_dvd_lcm {g : α → α} (h : function.commute f g) :
+  minimal_period (f ∘ g) x ∣ nat.lcm (minimal_period f x) (minimal_period g x) :=
+begin
+  rw [← is_periodic_pt_iff_minimal_period_dvd, is_periodic_pt, h.comp_iterate],
+  refine is_fixed_pt.comp _ _;
+  rw [← is_periodic_pt, is_periodic_pt_iff_minimal_period_dvd];
+  exact nat.dvd_lcm_left _ _ <|> exact dvd_lcm_right _ _
+end
+
+private lemma minimal_period_iterate_eq_div_gcd_aux (h : 0 < gcd (minimal_period f x) n) :
+  minimal_period (f ^[n]) x = minimal_period f x / nat.gcd (minimal_period f x) n :=
+begin
+  apply nat.dvd_antisymm,
+  { apply is_periodic_pt.minimal_period_dvd,
+    rw [is_periodic_pt, is_fixed_pt, ← iterate_mul, ← nat.mul_div_assoc _ (gcd_dvd_left _ _),
+        mul_comm, nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul],
+    exact (is_periodic_pt_minimal_period f x).iterate _ },
+  { apply coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h),
+    apply dvd_of_mul_dvd_mul_right h,
+    rw [nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, nat.div_mul_cancel (gcd_dvd_right _ _),
+        mul_comm],
+    apply is_periodic_pt.minimal_period_dvd,
+    rw [is_periodic_pt, is_fixed_pt, iterate_mul],
+    exact is_periodic_pt_minimal_period _ _ }
+end
+
+lemma minimal_period_iterate_eq_div_gcd (h : n ≠ 0) :
+  minimal_period (f ^[n]) x = minimal_period f x / nat.gcd (minimal_period f x) n :=
+minimal_period_iterate_eq_div_gcd_aux $ gcd_pos_of_pos_right _ (nat.pos_of_ne_zero h)
+
+lemma minimal_period_iterate_eq_div_gcd' (h : x ∈ periodic_pts f) :
+  minimal_period (f ^[n]) x = minimal_period f x / nat.gcd (minimal_period f x) n :=
+minimal_period_iterate_eq_div_gcd_aux $
+  gcd_pos_of_pos_left n (minimal_period_pos_iff_mem_periodic_pts.mpr h)
 
 end function