FrobeniusPeriod.lean

1 import PaperXI.PacketSupport
2 import Mathlib.Dynamics.PeriodicPts.Lemmas
3 import Mathlib.GroupTheory.OrderOfElement
4 
5 /-! Minimal return period, exact finite orbit size, and stabilizing powers. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FrobeniusPeriod
9 open PaperXI.FrobeniusOrbit
10 variable {M : ℕ}
11 
12 def permutation (q : (ZMod M)ˣ) : Equiv.Perm (ZMod M) := Units.mulLeft q
13 
14 def period (q : (ZMod M)ˣ) (j : ZMod M) : ℕ := Function.minimalPeriod (permutation q) j
15 
16 theorem iterate_label (q : (ZMod M)ˣ) (j : ZMod M) (n : ℕ) :
17     (permutation q)^[n] j = ((q ^ n : (ZMod M)ˣ) : ZMod M) * j := by
18   induction n with
19   | zero => simp
20   | succ n ih =>
21     rw [Function.iterate_succ_apply']
22     change (q : ZMod M) * ((permutation q)^[n] j) = _
23     rw [ih, pow_succ']
24     simp [mul_assoc]
25 
26 variable [NeZero M]
27 
28 theorem period_pos (q : (ZMod M)ˣ) (j : ZMod M) : 0 < period q j :=
29   Function.minimalPeriod_pos_of_mem_periodicPts ((permutation q).injective.mem_periodicPts j)
30 
31 theorem period_le (q : (ZMod M)ˣ) (j : ZMod M) : period q j ≤ M := by
32   simpa [period] using (Function.minimalPeriod_le_card (f := permutation q) (x := j))
33 
34 omit [NeZero M] in
35 theorem return_label (q : (ZMod M)ˣ) (j : ZMod M) :
36     ((q ^ period q j : (ZMod M)ˣ) : ZMod M) * j = j := by
37   have h := Function.isPeriodicPt_minimalPeriod (permutation q) j
38   change (permutation q)^[period q j] j = j at h
39   rwa [iterate_label] at h
40 
41 omit [NeZero M] in
42 /-- A natural power fixes the label exactly when the minimal period divides it. -/
43 theorem stabilizing_power_iff (q : (ZMod M)ˣ) (j : ZMod M) (n : ℕ) :
44     ((q ^ n : (ZMod M)ˣ) : ZMod M) * j = j ↔ period q j ∣ n := by
45   rw [← iterate_label]
46   exact Function.isPeriodicPt_iff_minimalPeriod_dvd
47 
48 omit [NeZero M] in
49 theorem no_short_return (q : (ZMod M)ˣ) (j : ZMod M) {n : ℕ}
50     (hn : 0 < n) (hnf : n < period q j) :
51     ((q ^ n : (ZMod M)ˣ) : ZMod M) * j ≠ j := by
52   intro h
53   exact (Nat.le_of_dvd hn ((stabilizing_power_iff q j n).mp h)).not_gt hnf
54 
55 omit [NeZero M] in
56 theorem related_iff_nat (q : (ZMod M)ˣ) (j k : ZMod M) :
57     Related q j k ↔ ∃ n : ℕ, ((q ^ n : (ZMod M)ˣ) : ZMod M) * j = k := by
58   constructor
59   · rintro ⟨z, hz⟩
60     have hm : q ^ z ∈ Subgroup.zpowers q := ⟨z, rfl⟩
61     have hp := (isOfFinOrder_of_finite q).mem_powers_iff_mem_zpowers.mpr hm
62     obtain ⟨n, hn⟩ := hp
63     change q ^ n = q ^ z at hn
64     exact ⟨n, by rw [hn]; exact hz⟩
65   · rintro ⟨n, hn⟩
66     exact ⟨n, by simpa using hn⟩
67 
68 theorem related_iff_bounded (q : (ZMod M)ˣ) (j k : ZMod M) :
69     Related q j k ↔ ∃ n : ℕ, n < period q j ∧
70       ((q ^ n : (ZMod M)ˣ) : ZMod M) * j = k := by
71   rw [related_iff_nat]
72   constructor
73   · rintro ⟨n, hn⟩
74     refine ⟨n % period q j, Nat.mod_lt _ (period_pos q j), ?_⟩
75     rw [← iterate_label, period, Function.iterate_mod_minimalPeriod_eq, iterate_label, hn]
76   · rintro ⟨n, _, hn⟩; exact ⟨n, hn⟩
77 
78 /-- Index every orbit label exactly once by the minimal positive period. -/
79 def orbitEquiv (q : (ZMod M)ˣ) (j : ZMod M) :
80     Fin (period q j) ≃ {k : ZMod M // Related q j k} :=
81   Equiv.ofBijective
82     (fun n => ⟨((q ^ (n : ℕ) : (ZMod M)ˣ) : ZMod M) * j,
83       (related_iff_nat q j _).mpr ⟨n, rfl⟩⟩) (by
84     constructor
85     · intro a b hab
86       apply Fin.ext
87       apply Function.iterate_injOn_Iio_minimalPeriod a.isLt b.isLt
88       simpa only [iterate_label] using congrArg Subtype.val hab
89     · intro k
90       obtain ⟨n, hn, hk⟩ := (related_iff_bounded q j k).mp k.property
91       exact ⟨⟨n, hn⟩, Subtype.ext hk⟩)
92 
93 theorem orbit_card (q : (ZMod M)ˣ) (j : ZMod M) :
94     Nat.card {k : ZMod M // Related q j k} = period q j := by
95   rw [← Nat.card_congr (orbitEquiv q j), Nat.card_fin]
96 
97 end PaperXI.FrobeniusPeriod

Back to source controls