CyclicFrobeniusCount.lean

1 import PaperXI.FrobeniusPeriodCount
2 import Mathlib.GroupTheory.SpecificGroups.Cyclic
3 import Mathlib.Data.Nat.GCD.Basic
4 
5 /-! Fixed points and regular orbit counts for the power map on a finite cyclic
6  group. No fixed-point cardinality is assumed. -/
7 set_option autoImplicit false
8 namespace PaperXI.CyclicFrobeniusCount
9 open Function Finset PaperXI.FrobeniusPeriodCount
10 open scoped Classical
11 
12 variable {G : Type*} [CommGroup G] [Finite G] [IsCyclic G]
13 
14 omit [Finite G] [IsCyclic G] in
15 /-- Iteration of the qth-power map is the q^r-th-power map. -/
16 theorem iterate_power (q r : ℕ) (x : G) :
17     (fun y : G => y ^ q)^[r] x = x ^ (q ^ r) := by
18   induction r with
19   | zero => simp
20   | succ r ih => simp [Function.iterate_succ_apply', ih, pow_succ, pow_mul]
21 
22 omit [Finite G] [IsCyclic G] in
23 /-- Fixed points are the actual kernel of the (q^r-1)th-power homomorphism. -/
24 theorem fixed_iff_kernel (q r : ℕ) (hq : 0 < q) (x : G) :
25     IsPeriodicPt (fun y : G => y ^ q) r x ↔
26       x ∈ (powMonoidHom (q ^ r - 1) : G →* G).ker := by
27   have hp : 1 ≤ q ^ r := Nat.one_le_pow r q hq
28   change (fun y : G => y ^ q)^[r] x = x ↔ x ^ (q ^ r - 1) = 1
29   rw [iterate_power]
30   have he : x ^ (q ^ r - 1) * x = x ^ (q ^ r) := by
31     rw [← pow_succ, Nat.sub_add_cancel hp]
32   constructor
33   · intro h
34     apply mul_right_cancel (b := x)
35     simpa only [one_mul, he] using h
36   · intro h
37     simpa only [h, one_mul] using he.symm
38 
39 /-- The fixed-point count is a kernel cardinality, hence a greatest common divisor. -/
40 theorem fixedCount_gcd (q r : ℕ) (hq : 0 < q) :
41     fixedCount (fun y : G => y ^ q) r = (Nat.card G).gcd (q ^ r - 1) := by
42   calc
43     _ = Nat.card (powMonoidHom (q ^ r - 1) : G →* G).ker :=
44       Nat.card_congr (Equiv.subtypeEquivRight (fixed_iff_kernel q r hq))
45     _ = _ := IsCyclic.card_powMonoidHom_ker G _
46 
47 /-- Stronger fixed-point formula, valid for every iterate r, not just r dividing n. -/
48 theorem fixedCount_pow_gcd (q n r : ℕ) (hq : 0 < q)
49     (hc : Nat.card G = q ^ n - 1) :
50     fixedCount (fun y : G => y ^ q) r = q ^ (n.gcd r) - 1 := by
51   rw [fixedCount_gcd q r hq, hc, Nat.pow_sub_one_gcd_pow_sub_one]
52 
53 /-- The divisor fixed-point counts used in the manuscript are now derived. -/
54 theorem fixedCount_of_dvd (q n r : ℕ) (hq : 0 < q)
55     (hc : Nat.card G = q ^ n - 1) (hr : r ∣ n) :
56     fixedCount (fun y : G => y ^ q) r = q ^ r - 1 := by
57   rw [fixedCount_pow_gcd q n r hq hc, Nat.gcd_eq_right hr]
58 
59 /-- An integral formula for characters of exact Frobenius period n. -/
60 theorem exactCount_formula (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
61     (hc : Nat.card G = q ^ n - 1) :
62     (exactCount (fun y : G => y ^ q) n : ℤ) =
63       ∑ d ∈ n.divisors, ArithmeticFunction.moebius d * ((q : ℤ) ^ (n / d) - 1) := by
64   rw [moebius_exactCount _ n hn]
65   apply sum_congr rfl
66   intro d hd
67   rw [fixedCount_of_dvd q n (n / d) hq hc (Nat.div_dvd_of_dvd (Nat.mem_divisors.mp hd).1)]
68   rw [Nat.cast_sub (Nat.one_le_pow _ q hq), Nat.cast_pow, Nat.cast_one]
69 
70 omit [CommGroup G] [Finite G] [IsCyclic G] in
71 /-- The power map is invertible for cyclic groups of order q^n-1. -/
72 theorem card_coprime_q (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
73     (hc : Nat.card G = q ^ n - 1) : (Nat.card G).Coprime q := by
74   rw [hc]
75   have h : (q ^ n - 1).Coprime (q ^ n) :=
76     (Nat.coprime_self_sub_left (Nat.one_le_pow n q hq)).mpr (Nat.coprime_one_left _)
77   exact h.of_dvd_right (dvd_pow_self q hn.ne')
78 
79 noncomputable def frobeniusPerm (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
80     (hc : Nat.card G = q ^ n - 1) : Equiv.Perm G :=
81   powCoprime (card_coprime_q q n hq hn hc)
82 
83 omit [Finite G] [IsCyclic G] in
84 @[simp] theorem frobeniusPerm_apply (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
85     (hc : Nat.card G = q ^ n - 1) (x : G) :
86     frobeniusPerm q n hq hn hc x = x ^ q := rfl
87 
88 /-- The actual regular-orbit count times n equals the integral Möbius sum. -/
89 theorem orbitCount_mul_formula (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
90     (hc : Nat.card G = q ^ n - 1) :
91     (orbitCount (frobeniusPerm q n hq hn hc) n : ℤ) * n =
92       ∑ d ∈ n.divisors, ArithmeticFunction.moebius d * ((q : ℤ) ^ (n / d) - 1) := by
93   have h := exactCount_eq_orbitCount_mul (frobeniusPerm q n hq hn hc) n
94   have he : (exactCount (fun y : G => y ^ q) n : ℤ) =
95       (orbitCount (frobeniusPerm q n hq hn hc) n : ℤ) * n := by
96     exact_mod_cast h
97   exact he.symm.trans (exactCount_formula q n hq hn hc)
98 
99 /-- The numerator is divisible by n because it counts a disjoint union of n-cycles. -/
100 theorem moebius_sum_dvd (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
101     (hc : Nat.card G = q ^ n - 1) :
102     (n : ℤ) ∣ ∑ d ∈ n.divisors,
103       ArithmeticFunction.moebius d * ((q : ℤ) ^ (n / d) - 1) := by
104   rw [← orbitCount_mul_formula q n hq hn hc]
105   exact dvd_mul_left _ _
106 
107 /-- Rational display of the manuscript's formula, with actual quotient cardinality. -/
108 theorem orbitCount_formula (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
109     (hc : Nat.card G = q ^ n - 1) :
110     (orbitCount (frobeniusPerm q n hq hn hc) n : ℚ) =
111       (1 / (n : ℚ)) * ∑ d ∈ n.divisors,
112         (ArithmeticFunction.moebius d : ℚ) * ((q : ℚ) ^ (n / d) - 1) := by
113   have h : (orbitCount (frobeniusPerm q n hq hn hc) n : ℚ) * n =
114       ∑ d ∈ n.divisors, (ArithmeticFunction.moebius d : ℚ) * ((q : ℚ) ^ (n / d) - 1) := by
115     exact_mod_cast orbitCount_mul_formula q n hq hn hc
116   have hnq : (n : ℚ) ≠ 0 := by exact_mod_cast hn.ne'
117   apply (eq_div_iff hnq).mpr h |>.trans
118   ring
119 
120 end PaperXI.CyclicFrobeniusCount

Back to source controls