TameNorm.lean

1 import Mathlib.FieldTheory.Finite.GaloisField
2 import Mathlib.Data.ZMod.Basic
3 import Mathlib.Basic.Complex.Basic
4 
5 /-! Paper XI, 5.3: norm lifting and Frobenius on actual finite-field unit characters.
6 The characters on subfields are restrictions of one character of the common field.
7 This is the compatible choice of exponent coordinates used by the source formula. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TameNorm
11 
12 variable (K L : Type*) [Field K] [Field L] [Algebra K L] [Finite L]
13 
14 /-- The actual field embedding on multiplicative groups. -/
15 def embedding : Kˣ →* Lˣ := Units.map (algebraMap K L).toMonoidHom
16 
17 omit [Finite L] in
18 theorem embedding_injective : Function.Injective (embedding K L) := by
19   intro x y h
20   apply Units.ext
21   exact (algebraMap K L).injective (congrArg (fun u : Lˣ => (u : L)) h)
22 
23 /-- The actual field norm on multiplicative groups. -/
24 def norm : Lˣ →* Kˣ := Units.map (Algebra.norm K (S := L))
25 
26 /-- The finite-field norm exponent, expressed using field cardinalities. -/
27 def normExponent : ℕ := (Nat.card L - 1) / (Nat.card K - 1)
28 
29 theorem embedding_norm (x : Lˣ) :
30     embedding K L (norm K L x) = x ^ normExponent K L := by
31   apply Units.ext
32   exact FiniteField.algebraMap_norm_eq_pow
33 
34 /-- Pulling a character back by the actual norm multiplies its exponent. -/
35 theorem norm_lift (χ : Lˣ →* ℂˣ) (a : ℕ) :
36     (((χ.comp (embedding K L)) ^ a).comp (norm K L)) =
37       χ ^ (a * normExponent K L) := by
38   apply MonoidHom.ext
39   intro x
40   change χ (embedding K L (norm K L x)) ^ a = χ x ^ (a * normExponent K L)
41   rw [embedding_norm, map_pow, ← pow_mul, Nat.mul_comm]
42 
43 /-- Actual units norm lifting preserves nontriviality because the norm is onto. -/
44 theorem norm_lift_eq_one_iff (χ : Kˣ →* ℂˣ) :
45     χ.comp (norm K L) = 1 ↔ χ = 1 := by
46   constructor
47   · intro h
48     apply MonoidHom.ext
49     intro x
50     obtain ⟨y, rfl⟩ := FiniteField.unitsMap_norm_surjective K L x
51     exact congrArg (fun f : Lˣ →* ℂˣ => f y) h
52   · intro h
53     simp [h]
54 
55 variable (Q : Type*) [Field Q] [Fintype Q] [Algebra Q L]
56 
57 /-- The actual iterate of the relative finite-field Frobenius on units. -/
58 def frobenius (i : ℕ) : Lˣ →* Lˣ :=
59   Units.map (((FiniteField.frobeniusAlgEquivOfAlgebraic Q L) ^ i).toAlgHom.toMonoidHom)
60 
61 @[simp] theorem frobenius_apply (i : ℕ) (x : Lˣ) :
62     frobenius L Q i x = x ^ (Fintype.card Q ^ i) := by
63   apply Units.ext
64   change ((FiniteField.frobeniusAlgEquivOfAlgebraic Q L) ^ i) (x : L) = _
65   rw [AlgEquiv.coe_pow, FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate]
66   rfl
67 
68 theorem frobenius_character (χ : Lˣ →* ℂˣ) (i : ℕ) :
69     χ.comp (frobenius L Q i) = χ ^ (Fintype.card Q ^ i) := by
70   apply MonoidHom.ext
71   intro x
72   simp [MonoidHom.comp_apply]
73 
74 /-- The norm lift of the Frobenius-shifted subfield character, evaluated on
75 an actual common-field unit. -/
76 theorem shifted_norm_lift (χ : Lˣ →* ℂˣ) (a i : ℕ) :
77     ((((χ.comp (embedding K L)) ^ a).comp (norm K L)).comp
78       (frobenius L Q i)) = χ ^ (a * Fintype.card Q ^ i * normExponent K L) := by
79   rw [norm_lift]
80   apply MonoidHom.ext
81   intro x
82   change χ (frobenius L Q i x) ^ (a * normExponent K L) = _
83   rw [frobenius_apply, map_pow, ← pow_mul]
84   congr 1
85   ac_rfl
86 
87 /-- Norm and the actual q-Frobenius commute on units. -/
88 theorem norm_frobenius [Finite K] [Algebra Q K] (i : ℕ) (x : Lˣ) :
89     norm K L (frobenius L Q i x) = frobenius K Q i (norm K L x) := by
90   rw [frobenius_apply, frobenius_apply, map_pow]
91 
92 /-- The source ordering: shift the lower-field character, then lift by the norm. -/
93 theorem shifted_lower_norm_lift [Finite K] [Algebra Q K]
94     (χ : Lˣ →* ℂˣ) (a i : ℕ) :
95     ((((χ.comp (embedding K L)) ^ a).comp (frobenius K Q i)).comp
96       (norm K L)) = χ ^ (a * Fintype.card Q ^ i * normExponent K L) := by
97   rw [← shifted_norm_lift K L Q χ a i]
98   apply MonoidHom.ext
99   intro x
100   simp only [MonoidHom.comp_apply, norm_frobenius]
101 
102 end PaperXI.TameNorm

Back to source controls