FiniteFieldOrbitCount.lean

1 import PaperXI.CyclicFrobeniusCount
2 import Mathlib.NumberTheory.MulChar.Duality
3 import Mathlib.RingTheory.RootsOfUnity.Complex
4 import Mathlib.FieldTheory.Finite.Basic
5 
6 /-! Proposition 3.6 on actual complex-valued multiplicative characters.
7 The cyclicity and cardinality of the character group are derived, not assumed. -/
8 set_option autoImplicit false
9 namespace PaperXI.FiniteFieldOrbitCount
10 open Function Finset PaperXI.FrobeniusPeriodCount PaperXI.CyclicFrobeniusCount
11 open scoped Classical
12 
13 noncomputable instance complexEnoughRoots (m : ℕ) [NeZero m] : HasEnoughRootsOfUnity ℂ m where
14   prim := ⟨_, Complex.isPrimitiveRoot_exp m (NeZero.ne m)⟩
15   cyc := inferInstance
16 
17 variable (F : Type*) [Field F] [Finite F]
18 
19 theorem characterGroup_isCyclic : IsCyclic (MulChar F ℂ) :=
20   (MulChar.mulEquiv_units F ℂ).some.isCyclic.mpr inferInstance
21 
22 attribute [local instance] characterGroup_isCyclic
23 
24 /-- The full multiplicative character group has |F|-1 elements. -/
25 theorem character_card : Nat.card (MulChar F ℂ) = Nat.card F - 1 := by
26   rw [MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity, Nat.card_units]
27 
28 noncomputable def characterFrobenius (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
29     (hF : Nat.card F = q ^ n) : Equiv.Perm (MulChar F ℂ) :=
30   frobeniusPerm q n hq hn (by rw [character_card, hF])
31 
32 /-- This permutation is exactly precomposition with the qth-power map on units. -/
33 theorem characterFrobenius_apply (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
34     (hF : Nat.card F = q ^ n) (χ : MulChar F ℂ) (x : Fˣ) :
35     characterFrobenius F q n hq hn hF χ x = χ (x ^ q : Fˣ) := by
36   change (χ ^ q) (x : F) = χ (x ^ q : Fˣ)
37   rw [MulChar.pow_apply_coe]
38   simp only [Units.val_pow_eq_pow_val, map_pow]
39 
40 /-- Every iterate has a derived fixed-character count, q^gcd(n,r)-1. -/
41 theorem fixed_character_count (q n r : ℕ) (hq : 0 < q)
42     (hF : Nat.card F = q ^ n) :
43     fixedCount (fun χ : MulChar F ℂ => χ ^ q) r = q ^ (n.gcd r) - 1 := by
44   exact fixedCount_pow_gcd q n r hq (by rw [character_card, hF])
45 
46 /-- Exact-period character count with no division and no free count certificate. -/
47 theorem exact_character_count (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
48     (hF : Nat.card F = q ^ n) :
49     (exactCount (fun χ : MulChar F ℂ => χ ^ q) n : ℤ) =
50       ∑ d ∈ n.divisors, ArithmeticFunction.moebius d * ((q : ℤ) ^ (n / d) - 1) := by
51   exact exactCount_formula q n hq hn (by rw [character_card, hF])
52 
53 /-- Proposition 3.6: cardinality of the quotient of actual regular characters. -/
54 theorem regular_character_orbits (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
55     (hF : Nat.card F = q ^ n) :
56     (orbitCount (characterFrobenius F q n hq hn hF) n : ℚ) =
57       (1 / (n : ℚ)) * ∑ d ∈ n.divisors,
58         (ArithmeticFunction.moebius d : ℚ) * ((q : ℚ) ^ (n / d) - 1) := by
59   exact orbitCount_formula q n hq hn (by rw [character_card, hF])
60 
61 /-- Integrality of the manuscript's numerator follows from the orbit quotient. -/
62 theorem regular_numerator_divisible (q n : ℕ) (hq : 0 < q) (hn : 0 < n)
63     (hF : Nat.card F = q ^ n) :
64     (n : ℤ) ∣ ∑ d ∈ n.divisors,
65       ArithmeticFunction.moebius d * ((q : ℤ) ^ (n / d) - 1) := by
66   exact moebius_sum_dvd (G := MulChar F ℂ) q n hq hn (by rw [character_card, hF])
67 
68 
69 /-- All hypotheses can be supplied by a genuine finite-field extension K ⊆ F. -/
70 noncomputable def extensionFrobenius (K : Type*) [Field K] [Fintype K]
71     [Fintype F] [Algebra K F] : Equiv.Perm (MulChar F ℂ) :=
72   characterFrobenius F (Fintype.card K) (Module.finrank K F)
73     Fintype.card_pos Module.finrank_pos
74     (by simpa only [Nat.card_eq_fintype_card] using (Module.card_eq_pow_finrank (K := K) (V := F)))
75 
76 /-- The manuscript count on a finite-field extension, with its true extension degree. -/
77 theorem extension_regular_orbits (K : Type*) [Field K] [Fintype K]
78     [Fintype F] [Algebra K F] :
79     (orbitCount (extensionFrobenius F K) (Module.finrank K F) : ℚ) =
80       (1 / (Module.finrank K F : ℚ)) * ∑ d ∈ (Module.finrank K F).divisors,
81         (ArithmeticFunction.moebius d : ℚ) *
82           ((Fintype.card K : ℚ) ^ (Module.finrank K F / d) - 1) := by
83   exact regular_character_orbits F (Fintype.card K) (Module.finrank K F)
84     Fintype.card_pos Module.finrank_pos
85     (by simpa only [Nat.card_eq_fintype_card] using (Module.card_eq_pow_finrank (K := K) (V := F)))
86 
87 /-- The extension action evaluates characters on the actual qth power of field units. -/
88 theorem extensionFrobenius_apply (K : Type*) [Field K] [Fintype K]
89     [Fintype F] [Algebra K F] (χ : MulChar F ℂ) (x : Fˣ) :
90     extensionFrobenius F K χ x = χ (x ^ Fintype.card K : Fˣ) := by
91   exact characterFrobenius_apply F _ _ _ _ _ χ x
92 
93 end PaperXI.FiniteFieldOrbitCount

Back to source controls