feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period (#9490)

Defines `MulAction.period g a` as a wrapper around `Function.minimalPeriod (fun x => g • x) a`,
allowing for some cleaner proofs involving the period of a group action.
The existing `MulAction.*_minimalPeriod_*` lemmas are changed to be defined using their now-preferred `MulAction.*_period_*` counterparts,
although they will only be made deprecated in another pull request.
The `Mathlib.GroupTheory.GroupAction.Period` module is also created, for additional lemmas around `MulAction.period`.

Some core lemmas need to remain in `Mathlib.Dynamics.PeriodicPts`, as they are needed for `ZMod` and the quotient group.

Author: adri326

Mathlib.lean

@@ -2284,6 +2284,7 @@ import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Hom
 import Mathlib.GroupTheory.GroupAction.Opposite
 import Mathlib.GroupTheory.GroupAction.Option
+import Mathlib.GroupTheory.GroupAction.Period
 import Mathlib.GroupTheory.GroupAction.Pi
 import Mathlib.GroupTheory.GroupAction.Prod
 import Mathlib.GroupTheory.GroupAction.Quotient

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -174,6 +174,10 @@ theorem smul_iterate [MulAction G H] : (a • · : H → H)^[n] = (a ^ n • ·)
 #align smul_iterate smul_iterate
 #align vadd_iterate vadd_iterate
 
+@[to_additive]
+lemma smul_iterate_apply [MulAction G H] {b : H} : (a • ·)^[n] b = a ^ n • b := by
+  rw [smul_iterate]
+
 @[to_additive (attr := simp)]
 theorem mul_left_iterate : (a * ·)^[n] = (a ^ n * ·) :=
   smul_iterate a n

Mathlib/Dynamics/PeriodicPts.lean

@@ -27,6 +27,8 @@ A point `x : α` is a periodic point of `f : α → α` of period `n` if `f^[n]
 * `minimalPeriod f x` : the minimal period of a point `x` under an endomorphism `f` or zero
   if `x` is not a periodic point of `f`.
 * `orbit f x`: the cycle `[x, f x, f (f x), ...]` for a periodic point.
+* `MulAction.period g x` : the minimal period of a point `x` under the multiplicative action of `g`;
+  an equivalent `AddAction.period g x` is defined for additive actions.
 
 ## Main statements
 
@@ -628,42 +630,117 @@ namespace MulAction
 
 open Function
 
-variable {α β : Type*} [Group α] [MulAction α β] {a : α} {b : β}
+universe u v
+variable {α : Type v}
+variable {G : Type u} [Group G] [MulAction G α]
+variable {M : Type u} [Monoid M] [MulAction M α]
+
+/--
+The period of a multiplicative action of `g` on `a` is the smallest positive `n` such that
+`g ^ n • a = a`, or `0` if such an `n` does not exist.
+-/
+@[to_additive "The period of an additive action of `g` on `a` is the smallest positive `n`
+such that `(n • g) +ᵥ a = a`, or `0` if such an `n` does not exist."]
+noncomputable def period (m : M) (a : α) : ℕ := minimalPeriod (fun x => m • x) a
+
+/-- `MulAction.period m a` is definitionally equal to `Function.minimalPeriod (m • ·) a`. -/
+@[to_additive "`AddAction.period m a` is definitionally equal to
+`Function.minimalPeriod (m +ᵥ ·) a`"]
+theorem period_eq_minimalPeriod {m : M} {a : α} :
+    MulAction.period m a = minimalPeriod (fun x => m • x) a := rfl
+
+/-- `m ^ (period m a)` fixes `a`. -/
+@[to_additive (attr := simp) "`(period m a) • m` fixes `a`."]
+theorem pow_period_smul (m : M) (a : α) : m ^ (period m a) • a = a := by
+  rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]
+
+@[to_additive]
+lemma isPeriodicPt_smul_iff {m : M} {a : α} {n : ℕ} :
+    IsPeriodicPt (m • ·) n a ↔ m ^ n • a = a := by
+  rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]
+
+/-! ### Multiples of `MulAction.period`
+
+It is easy to convince oneself that if `g ^ n • a = a` (resp. `(n • g) +ᵥ a = a`),
+then `n` must be a multiple of `period g a`.
+
+This also holds for negative powers/multiples.
+-/
+
+@[to_additive]
+theorem pow_smul_eq_iff_period_dvd {n : ℕ} {m : M} {a : α} :
+    m ^ n • a = a ↔ period m a ∣ n := by
+  rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]
+
+@[to_additive]
+theorem zpow_smul_eq_iff_period_dvd {j : ℤ} {g : G} {a : α} :
+    g ^ j • a = a ↔ (period g a : ℤ) ∣ j := by
+  rcases j with n | n
+  · rw [Int.ofNat_eq_coe, zpow_ofNat, Int.coe_nat_dvd, pow_smul_eq_iff_period_dvd]
+  · rw [Int.negSucc_coe, zpow_neg, zpow_ofNat, inv_smul_eq_iff, eq_comm, dvd_neg, Int.coe_nat_dvd,
+      pow_smul_eq_iff_period_dvd]
+
+@[to_additive (attr := simp)]
+theorem pow_mod_period_smul (n : ℕ) {m : M} {a : α} :
+    m ^ (n % period m a) • a = m ^ n • a := by
+  conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
+    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]
+
+@[to_additive (attr := simp)]
+theorem zpow_mod_period_smul (j : ℤ) {g : G} {a : α} :
+    g ^ (j % (period g a : ℤ)) • a = g ^ j • a := by
+  conv_rhs => rw [← Int.emod_add_ediv j (period g a), zpow_add, mul_smul,
+    zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]
+
+@[to_additive (attr := simp)]
+theorem pow_add_period_smul (n : ℕ) (m : M) (a : α) :
+    m ^ (n + period m a) • a = m ^ n • a := by
+  rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]
+
+@[to_additive (attr := simp)]
+theorem pow_period_add_smul (n : ℕ) (m : M) (a : α) :
+    m ^ (period m a + n) • a = m ^ n • a := by
+  rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]
+
+@[to_additive (attr := simp)]
+theorem zpow_add_period_smul (i : ℤ) (g : G) (a : α) :
+    g ^ (i + period g a) • a = g ^ i • a := by
+  rw [← zpow_mod_period_smul, Int.add_emod_self, zpow_mod_period_smul]
+
+@[to_additive (attr := simp)]
+theorem zpow_period_add_smul (i : ℤ) (g : G) (a : α) :
+    g ^ (period g a + i) • a = g ^ i • a := by
+  rw [← zpow_mod_period_smul, Int.add_emod_self_left, zpow_mod_period_smul]
+
+variable {a : G} {b : α}
 
 @[to_additive]
 theorem pow_smul_eq_iff_minimalPeriod_dvd {n : ℕ} :
-    a ^ n • b = b ↔ Function.minimalPeriod (a • ·) b ∣ n := by
-  rw [← isPeriodicPt_iff_minimalPeriod_dvd, IsPeriodicPt, IsFixedPt, smul_iterate]
+    a ^ n • b = b ↔ minimalPeriod (a • ·) b ∣ n := by
+  rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]
 #align mul_action.pow_smul_eq_iff_minimal_period_dvd MulAction.pow_smul_eq_iff_minimalPeriod_dvd
 #align add_action.nsmul_vadd_eq_iff_minimal_period_dvd AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd
 
 @[to_additive]
 theorem zpow_smul_eq_iff_minimalPeriod_dvd {n : ℤ} :
-    a ^ n • b = b ↔ (Function.minimalPeriod (a • ·) b : ℤ) ∣ n := by
-  cases n
-  · rw [Int.ofNat_eq_coe, zpow_ofNat, Int.coe_nat_dvd, pow_smul_eq_iff_minimalPeriod_dvd]
-  · rw [Int.negSucc_coe, zpow_neg, zpow_ofNat, inv_smul_eq_iff, eq_comm, dvd_neg, Int.coe_nat_dvd,
-      pow_smul_eq_iff_minimalPeriod_dvd]
+    a ^ n • b = b ↔ (minimalPeriod (a • ·) b : ℤ) ∣ n := by
+  rw [← period_eq_minimalPeriod, zpow_smul_eq_iff_period_dvd]
 #align mul_action.zpow_smul_eq_iff_minimal_period_dvd MulAction.zpow_smul_eq_iff_minimalPeriod_dvd
 #align add_action.zsmul_vadd_eq_iff_minimal_period_dvd AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd
 
 variable (a b)
 
 @[to_additive (attr := simp)]
 theorem pow_smul_mod_minimalPeriod (n : ℕ) :
-    a ^ (n % Function.minimalPeriod (a • ·) b) • b = a ^ n • b := by
-  conv_rhs =>
-    rw [← Nat.mod_add_div n (minimalPeriod (a • ·) b), pow_add, mul_smul,
-      pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
+    a ^ (n % minimalPeriod (a • ·) b) • b = a ^ n • b := by
+  rw [← period_eq_minimalPeriod, pow_mod_period_smul]
 #align mul_action.pow_smul_mod_minimal_period MulAction.pow_smul_mod_minimalPeriod
 #align add_action.nsmul_vadd_mod_minimal_period AddAction.nsmul_vadd_mod_minimalPeriod
 
 @[to_additive (attr := simp)]
 theorem zpow_smul_mod_minimalPeriod (n : ℤ) :
-    a ^ (n % (Function.minimalPeriod (a • ·) b : ℤ)) • b = a ^ n • b := by
-  conv_rhs =>
-    rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
-      zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
+    a ^ (n % (minimalPeriod (a • ·) b : ℤ)) • b = a ^ n • b := by
+  rw [← period_eq_minimalPeriod, zpow_mod_period_smul]
 #align mul_action.zpow_smul_mod_minimal_period MulAction.zpow_smul_mod_minimalPeriod
 #align add_action.zsmul_vadd_mod_minimal_period AddAction.zsmul_vadd_mod_minimalPeriod
 

Mathlib/GroupTheory/GroupAction/Period.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2024 Emilie Burgun. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Emilie Burgun
+-/
+
+import Mathlib.Dynamics.PeriodicPts
+import Mathlib.GroupTheory.Exponent
+import Mathlib.GroupTheory.GroupAction.Basic
+
+/-!
+# Period of a group action
+
+This module defines some helpful lemmas around [`MulAction.period`] and [`AddAction.period`].
+The period of a point `a` by a group element `g` is the smallest `m` such that `g ^ m • a = a`
+(resp. `(m • g) +ᵥ a = a`) for a given `g : G` and `a : α`.
+
+If such an `m` does not exist,
+then by convention `MulAction.period` and `AddAction.period` return 0.
+-/
+
+namespace MulAction
+
+universe u v
+variable {α : Type v}
+variable {G : Type u} [Group G] [MulAction G α]
+variable {M : Type u} [Monoid M] [MulAction M α]
+
+/-- If the action is periodic, then a lower bound for its period can be computed. -/
+@[to_additive "If the action is periodic, then a lower bound for its period can be computed."]
+theorem le_period {m : M} {a : α} {n : ℕ} (period_pos : 0 < period m a)
+    (moved : ∀ k, 0 < k → k < n → m ^ k • a ≠ a) : n ≤ period m a :=
+  le_of_not_gt fun period_lt_n =>
+    moved _ period_pos period_lt_n <| pow_period_smul m a
+
+/-- If for some `n`, `m ^ n • a = a`, then `period m a ≤ n`. -/
+@[to_additive "If for some `n`, `(n • m) +ᵥ a = a`, then `period m a ≤ n`."]
+theorem period_le_of_fixed {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : m ^ n • a = a) :
+    period m a ≤ n :=
+  (isPeriodicPt_smul_iff.mpr fixed).minimalPeriod_le n_pos
+
+/-- If for some `n`, `m ^ n • a = a`, then `0 < period m a`. -/
+@[to_additive "If for some `n`, `(n • m) +ᵥ a = a`, then `0 < period m a`."]
+theorem period_pos_of_fixed {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : m ^ n • a = a) :
+    0 < period m a :=
+  (isPeriodicPt_smul_iff.mpr fixed).minimalPeriod_pos n_pos
+
+@[to_additive]
+theorem period_eq_one_iff {m : M} {a : α} : period m a = 1 ↔ m • a = a :=
+  ⟨fun eq_one => pow_one m ▸ eq_one ▸ pow_period_smul m a,
+   fun fixed => le_antisymm
+    (period_le_of_fixed one_pos (by simpa))
+    (period_pos_of_fixed one_pos (by simpa))⟩
+
+/-- For any non-zero `n` less than the period of `m` on `a`, `a` is moved by `m ^ n`. -/
+@[to_additive "For any non-zero `n` less than the period of `m` on `a`, `a` is moved by `n • m`."]
+theorem pow_smul_ne_of_lt_period {m : M} {a : α} {n : ℕ} (n_pos : 0 < n)
+    (n_lt_period : n < period m a) : m ^ n • a ≠ a := fun a_fixed =>
+  not_le_of_gt n_lt_period <| period_le_of_fixed n_pos a_fixed
+
+section Identities
+
+/-! ### `MulAction.period` for common group elements
+-/
+
+variable (M) in
+@[to_additive (attr := simp)]
+theorem period_one (a : α) : period (1 : M) a = 1 := period_eq_one_iff.mpr (one_smul M a)
+
+@[to_additive (attr := simp)]
+theorem period_inv (g : G) (a : α) : period g⁻¹ a = period g a := by
+  simp only [period_eq_minimalPeriod, Function.minimalPeriod_eq_minimalPeriod_iff,
+    isPeriodicPt_smul_iff]
+  intro n
+  rw [smul_eq_iff_eq_inv_smul, eq_comm, ← zpow_ofNat, inv_zpow, inv_inv, zpow_ofNat]
+
+end Identities
+
+section MonoidExponent
+
+/-! ### `MulAction.period` and group exponents
+
+The period of a given element `m : M` can be bounded by the `Monoid.exponent M` or `orderOf m`.
+-/
+
+@[to_additive]
+theorem period_dvd_orderOf (m : M) (a : α) : period m a ∣ orderOf m := by
+  rw [← pow_smul_eq_iff_period_dvd, pow_orderOf_eq_one, one_smul]
+
+@[to_additive]
+theorem period_pos_of_orderOf_pos {m : M} (order_pos : 0 < orderOf m) (a : α) :
+    0 < period m a :=
+  Nat.pos_of_dvd_of_pos (period_dvd_orderOf m a) order_pos
+
+@[to_additive]
+theorem period_le_orderOf {m : M} (order_pos : 0 < orderOf m) (a : α) :
+    period m a ≤ orderOf m :=
+  Nat.le_of_dvd order_pos (period_dvd_orderOf m a)
+
+@[to_additive]
+theorem period_dvd_exponent (m : M) (a : α) : period m a ∣ Monoid.exponent M := by
+  rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]
+
+@[to_additive]
+theorem period_pos_of_exponent_pos (exp_pos : 0 < Monoid.exponent M) (m : M) (a : α) :
+    0 < period m a :=
+  Nat.pos_of_dvd_of_pos (period_dvd_exponent m a) exp_pos
+
+@[to_additive]
+theorem period_le_exponent (exp_pos : 0 < Monoid.exponent M) (m : M) (a : α) :
+    period m a ≤ Monoid.exponent M :=
+  Nat.le_of_dvd exp_pos (period_dvd_exponent m a)
+
+variable (α)
+
+@[to_additive]
+theorem period_bounded_of_exponent_pos (exp_pos : 0 < Monoid.exponent M) (m : M) :
+    BddAbove (Set.range (fun a : α => period m a)) := by
+  use Monoid.exponent M
+  simpa [upperBounds] using period_le_exponent exp_pos _
+
+end MonoidExponent
+
+
+end MulAction