TameExponent.lean

1 import PaperXI.TameNorm
2 import PaperXI.ElementaryEnvelope
3 import Mathlib.GroupTheory.SpecificGroups.Cyclic
4 
5 /-! Faithful exponent coordinates for genuine finite-field unit characters. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TameExponent
9 
10 /-- The standard injective character of the finite cyclic exponent group. -/
11 def rootEmbedding (N : ℕ) [NeZero N] : Multiplicative (ZMod N) →* ℂˣ where
12   toFun x := ((ElementaryEnvelope.rootEquiv N x.toAdd).toMul : ℂˣ)
13   map_one' := by
14     change ((ElementaryEnvelope.rootEquiv N 0).toMul : ℂˣ) = 1
15     rw [map_zero]
16     rfl
17   map_mul' x y := by
18     change ((ElementaryEnvelope.rootEquiv N (x.toAdd + y.toAdd)).toMul : ℂˣ) = _
19     rw [map_add]
20     rfl
21 
22 theorem rootEmbedding_injective (N : ℕ) [NeZero N] :
23     Function.Injective (rootEmbedding N) := by
24   intro x y h
25   apply Multiplicative.toAdd.injective
26   apply (ElementaryEnvelope.rootEquiv N).injective
27   exact Subtype.ext h
28 
29 variable (F : Type*) [Field F] [Finite F]
30 
31 /-- A faithful complex character exists on every finite-field multiplicative group. -/
32 def faithfulCharacter : Fˣ →* ℂˣ :=
33   letI : NeZero (Nat.card Fˣ) := ⟨Nat.card_pos.ne'⟩
34   (rootEmbedding (Nat.card Fˣ)).comp (zmodCyclicMulEquiv (G := Fˣ) inferInstance).symm.toMonoidHom
35 
36 theorem faithfulCharacter_injective : Function.Injective (faithfulCharacter F) := by
37   let : NeZero (Nat.card Fˣ) := ⟨Nat.card_pos.ne'⟩
38   exact (rootEmbedding_injective (Nat.card Fˣ)).comp
39     (zmodCyclicMulEquiv (G := Fˣ) inferInstance).symm.injective
40 
41 variable {F}
42 
43 /-- A faithful character power is trivial precisely at a zero residue exponent. -/
44 theorem pow_eq_one_iff (χ : Fˣ →* ℂˣ) (hχ : Function.Injective χ) (a : ℕ) :
45     χ ^ a = 1 ↔ (a : ZMod (Nat.card F - 1)) = 0 := by
46   rw [ZMod.natCast_eq_zero_iff]
47   rw [← Nat.card_units]
48   constructor
49   · intro h
50     obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
51     rw [← orderOf_eq_card_of_forall_mem_zpowers hg, orderOf_dvd_iff_pow_eq_one]
52     apply hχ
53     rw [map_pow, map_one]
54     exact congrArg (fun f : Fˣ →* ℂˣ => f g) h
55   · rintro ⟨k, rfl⟩
56     apply MonoidHom.ext
57     intro x
58     change χ x ^ (Nat.card Fˣ * k) = 1
59     rw [pow_mul, ← map_pow, pow_card_eq_one', map_one, one_pow]
60 
61 omit [Finite F] in
62 /-- Exponent coordinates are periodic by the actual unit-group cardinality. -/
63 theorem pow_add_card (χ : Fˣ →* ℂˣ) (a : ℕ) :
64     χ ^ (a + (Nat.card F - 1)) = χ ^ a := by
65   apply MonoidHom.ext
66   intro x
67   change χ x ^ (a + (Nat.card F - 1)) = χ x ^ a
68   rw [pow_add, ← Nat.card_units, ← map_pow χ x (Nat.card Fˣ),
69     pow_card_eq_one', map_one, mul_one]
70 
71 omit [Finite F] in
72 /-- Products of actual characters add exponent coordinates. -/
73 theorem product (χ : Fˣ →* ℂˣ) (a b : ℕ) : χ ^ a * χ ^ b = χ ^ (a + b) :=
74   (pow_add χ a b).symm
75 
76 /-- Every complex unit character has an exponent in any faithful coordinate system. -/
77 theorem exists_exponent (χ : Fˣ →* ℂˣ) (hχ : Function.Injective χ)
78     (η : Fˣ →* ℂˣ) : ∃ a < Nat.card F - 1, η = χ ^ a := by
79   let : NeZero (Nat.card Fˣ) := ⟨Nat.card_pos.ne'⟩
80   obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
81   have hp : IsPrimitiveRoot (χ g) (Nat.card Fˣ) := by
82     rw [IsPrimitiveRoot.iff_orderOf, orderOf_injective χ hχ,
83       orderOf_eq_card_of_forall_mem_zpowers hg]
84   have hη : η g ∈ rootsOfUnity (Nat.card Fˣ) ℂ := by
85     rw [mem_rootsOfUnity, ← map_pow, pow_card_eq_one', map_one]
86   obtain ⟨a, ha, heq⟩ := hp.eq_pow_of_mem_rootsOfUnity hη
87   refine ⟨a, by simpa only [Nat.card_units] using ha, ?_⟩
88   apply (MonoidHom.eq_iff_eq_on_generator hg η (χ ^ a)).mpr
89   exact heq.symm
90 
91 /-- Equality of actual characters is exactly equality of residue exponents. -/
92 theorem pow_eq_pow_iff (χ : Fˣ →* ℂˣ) (hχ : Function.Injective χ) (a b : ℕ) :
93     χ ^ a = χ ^ b ↔ (a : ZMod (Nat.card F - 1)) = b := by
94   obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
95   rw [MonoidHom.eq_iff_eq_on_generator hg]
96   change χ g ^ a = χ g ^ b ↔ _
97   rw [pow_eq_pow_iff_modEq, orderOf_injective χ hχ,
98     orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_units,
99     ZMod.natCast_eq_natCast_iff]
100 
101 /-- Residue exponents parameterize actual characters, using their natural representatives. -/
102 def coordinate (χ : Fˣ →* ℂˣ) (a : ZMod (Nat.card F - 1)) : Fˣ →* ℂˣ := χ ^ a.val
103 
104 /-- The parameterization is a bijection, not just a collection of selected powers. -/
105 theorem coordinate_bijective (χ : Fˣ →* ℂˣ) (hχ : Function.Injective χ) :
106     Function.Bijective (coordinate χ) := by
107   let : NeZero (Nat.card F - 1) := ⟨by rw [← Nat.card_units]; exact Nat.card_pos.ne'⟩
108   constructor
109   · intro a b h
110     have h' := (pow_eq_pow_iff χ hχ a.val b.val).mp h
111     simpa only [ZMod.natCast_zmod_val] using h'
112   · intro η
113     obtain ⟨a, ha, hη⟩ := exists_exponent χ hχ η
114     refine ⟨a, ?_⟩
115     simpa only [coordinate, ZMod.val_cast_of_lt ha] using hη.symm
116 
117 end PaperXI.TameExponent

Back to source controls