FrobeniusOrbit.lean

1 import PaperXI.PacketTransport
2 
3 /-! Frobenius orbits with integer powers, including both transport directions. -/
4 set_option autoImplicit false
5 namespace PaperXI.FrobeniusOrbit
6 variable {M : ℕ}
7 
8 def Related (q : (ZMod M)ˣ) (j k : ZMod M) : Prop :=
9   ∃ n : ℤ, ((q ^ n : (ZMod M)ˣ) : ZMod M) * j = k
10 
11 theorem refl (q : (ZMod M)ˣ) (j : ZMod M) : Related q j j :=
12   ⟨0, by simp⟩
13 
14 theorem trans (q : (ZMod M)ˣ) {i j k : ZMod M}
15     (hij : Related q i j) (hjk : Related q j k) : Related q i k := by
16   obtain ⟨m, rfl⟩ := hij
17   obtain ⟨n, rfl⟩ := hjk
18   exact ⟨n + m, by simp [zpow_add, mul_assoc]⟩
19 
20 theorem symm (q : (ZMod M)ˣ) {i j : ZMod M}
21     (hij : Related q i j) : Related q j i := by
22   obtain ⟨n, rfl⟩ := hij
23   refine ⟨-n, ?_⟩
24   simp [zpow_neg, ← mul_assoc]
25 
26 theorem step (q : (ZMod M)ˣ) (j : ZMod M) : Related q j ((q : ZMod M) * j) :=
27   ⟨1, by simp⟩
28 
29 theorem back (q : (ZMod M)ˣ) (j : ZMod M) :
30     Related q j (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) := ⟨-1, by simp⟩
31 
32 theorem step_mem (q : (ZMod M)ˣ) {i j : ZMod M} (h : Related q i j) :
33     Related q i ((q : ZMod M) * j) := trans q h (step q j)
34 
35 theorem back_mem (q : (ZMod M)ˣ) {i j : ZMod M} (h : Related q i j) :
36     Related q i (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) := trans q h (back q j)
37 
38 theorem same_orbit_iff (q : (ZMod M)ˣ) {i j : ZMod M} (h : Related q i j)
39     (k : ZMod M) : Related q i k ↔ Related q j k :=
40   ⟨fun hk => trans q (symm q h) hk, fun hk => trans q h hk⟩
41 
42 end PaperXI.FrobeniusOrbit

Back to source controls