TameGaussNaturality.lean

1 import PaperXI.GaussCharacters
2 import Mathlib.Algebra.Group.Units.Equiv
3 
4 /-! Additive-character normalization is part of the finite comparison data.
5 These statements concern the literal finite Gauss sum, not a full local epsilon
6 factor. A nontrivial residue character is required for a unit-norm phase. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TameGaussNaturality
10 open scoped Classical
11 variable {k : Type*} [Field k] [Fintype k]
12 
13 /-- Pull the multiplicative character back along a field automorphism. -/
14 def pullMul (e : k ≃+* k) (χ : kˣ →* ℂˣ) : kˣ →* ℂˣ :=
15   χ.comp (Units.map e.toMonoidHom)
16 
17 /-- The additive character must be transported at the same time. -/
18 def pullAdd (e : k ≃+* k) (ψ : AddChar k ℂ) : AddChar k ℂ :=
19   ψ.compAddMonoidHom e.toAddMonoidHom
20 
21 /-- Simultaneous transport of both characters is an exact change of summation variable. -/
22 theorem sum_transport (e : k ≃+* k) (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
23     GaussCharacters.sum (pullMul e χ) (pullAdd e ψ) = GaussCharacters.sum χ ψ := by
24   unfold GaussCharacters.sum
25   exact Fintype.sum_equiv (Units.mapEquiv e.toMulEquiv).toEquiv _ _ (fun _ => rfl)
26 
27 theorem phase_transport (e : k ≃+* k) (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
28     GaussCharacters.phase (pullMul e χ) (pullAdd e ψ) = GaussCharacters.phase χ ψ := by
29   unfold GaussCharacters.phase
30   rw [sum_transport]
31 
32 /-- Rotation of the residue character preserves the phase only with the stated
33 additive-character invariance. In particular this applies to Frobenius-stable ψ. -/
34 theorem phase_of_stable_additive (e : k ≃+* k) (χ : kˣ →* ℂˣ)
35     (ψ : AddChar k ℂ) (hψ : pullAdd e ψ = ψ) :
36     GaussCharacters.phase (pullMul e χ) ψ = GaussCharacters.phase χ ψ := by
37   simpa only [hψ] using phase_transport e χ ψ
38 
39 /-- Rescaling the additive character contributes the inverse multiplicative value. -/
40 theorem phase_mulShift (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) (a : kˣ) :
41     GaussCharacters.phase χ (ψ.mulShift (a : k)) =
42       (χ a : ℂ)⁻¹ * GaussCharacters.phase χ ψ := by
43   simp only [GaussCharacters.phase, GaussCharacters.sum_eq_unitSum,
44     GaussSums.unitSum_eq_gaussSum]
45   rw [gaussSum_mulShift_eq, MulChar.inv_apply_eq_inv', MulChar.ofUnitHom_coe,
46     mul_div_assoc]
47 
48 /-- The trivial multiplicative character does not have a unit-norm normalized sum. -/
49 theorem phase_trivial {ψ : AddChar k ℂ} (hψ : ψ ≠ 1) :
50     GaussCharacters.phase (1 : kˣ →* ℂˣ) ψ =
51       -1 / (Real.sqrt (Fintype.card k) : ℂ) := by
52   have he : MulChar.ofUnitHom (1 : kˣ →* ℂˣ) = (1 : MulChar k ℂ) :=
53     (MulChar.mulEquivToUnitHom (R := k) (R' := ℂ)).symm.map_one
54   simp only [GaussCharacters.phase, GaussCharacters.sum_eq_unitSum,
55     GaussSums.unitSum_eq_gaussSum, he]
56   rw [gaussSum_one_left hψ]
57 
58 /-- Both trivial and nontrivial residue characters have an exact magnitude rule. -/
59 theorem phase_norm_cases (χ : kˣ →* ℂˣ) {ψ : AddChar k ℂ} (hψ : ψ ≠ 1) :
60     ‖GaussCharacters.phase χ ψ‖ =
61       if χ = 1 then (Real.sqrt (Fintype.card k))⁻¹ else 1 := by
62   by_cases hχ : χ = 1
63   · subst χ
64     rw [ite_eq_left rfl, phase_trivial hψ, norm_div]
65     simp [Complex.norm_real, Real.norm_eq_abs,
66       abs_of_pos (GaussSums.sqrt_card_pos (k := k)), one_div]
67   · rw [ite_eq_right hχ]
68     exact GaussCharacters.phase_norm hχ hψ
69 
70 /-- A declared residue phase is never zero under a nontrivial additive character. -/
71 theorem phase_ne_zero (χ : kˣ →* ℂˣ) {ψ : AddChar k ℂ} (hψ : ψ ≠ 1) :
72     GaussCharacters.phase χ ψ ≠ 0 := by
73   apply norm_ne_zero_iff.mp
74   rw [phase_norm_cases χ hψ]
75   split_ifs
76   · exact inv_ne_zero (ne_of_gt (GaussSums.sqrt_card_pos (k := k)))
77   · exact one_ne_zero
78 
79 end PaperXI.TameGaussNaturality

Back to source controls