GaussCharacters.lean

1 import PaperXI.GaussSums
2 
3 /-! Translation to the manuscript's multiplicative characters kˣ → ℂˣ.
4 No additional unitarity assumption is needed over a finite field. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.GaussCharacters
8 open scoped Classical
9 variable {k : Type*} [Field k] [Fintype k]
10 
11 /-- The manuscript's Gauss sum for a character on the unit group. -/
12 def sum (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) : ℂ :=
13   ∑ x : kˣ, (χ x : ℂ) * ψ x
14 
15 /-- Zero extension preserves the literal unit-group sum. -/
16 theorem sum_eq_unitSum (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
17     sum χ ψ = GaussSums.unitSum (MulChar.ofUnitHom χ) ψ := by
18   simp only [sum, GaussSums.unitSum, MulChar.ofUnitHom_coe]
19 
20 omit [Fintype k] in
21 /-- A nontrivial unit-group character remains nontrivial after zero extension. -/
22 theorem extension_ne_one {χ : kˣ →* ℂˣ} (hχ : χ ≠ 1) :
23     MulChar.ofUnitHom χ ≠ 1 := by
24   intro h
25   apply hχ
26   ext x
27   have hx := congrArg (fun f : MulChar k ℂ => f (x : k)) h
28   simpa only [MulChar.ofUnitHom_coe, MulChar.one_apply_coe,
29     MonoidHom.one_apply, Units.val_one] using hx
30 
31 omit [Fintype k] in
32 /-- Inverting the unit-group character agrees with inverting its extension. -/
33 theorem extension_inverse (χ : kˣ →* ℂˣ) :
34     MulChar.ofUnitHom χ⁻¹ = (MulChar.ofUnitHom χ)⁻¹ := by
35   exact (MulChar.mulEquivToUnitHom (R := k) (R' := ℂ)).symm.map_inv χ
36 
37 /-- Proposition 6.1 in the exact unit-group character convention. -/
38 theorem magnitude {χ : kˣ →* ℂˣ} {ψ : AddChar k ℂ}
39     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
40     ‖sum χ ψ‖ = Real.sqrt (Fintype.card k) := by
41   rw [sum_eq_unitSum]
42   exact GaussSums.magnitude (extension_ne_one hχ) hψ
43 
44 /-- Definition 6.2 uses the positive square root of the field cardinality. -/
45 def phase (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) : ℂ :=
46   sum χ ψ / (Real.sqrt (Fintype.card k) : ℂ)
47 
48 /-- Normalization commutes with extending the multiplicative character. -/
49 theorem phase_eq (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
50     phase χ ψ = GaussSums.phase (MulChar.ofUnitHom χ) ψ := by
51   rw [phase, GaussSums.phase, sum_eq_unitSum]
52 
53 /-- Definition 6.2's unit-circle assertion, for the manuscript's character type. -/
54 theorem phase_norm {χ : kˣ →* ℂˣ} {ψ : AddChar k ℂ}
55     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) : ‖phase χ ψ‖ = 1 := by
56   rw [phase_eq]
57   exact GaussSums.phase_norm (extension_ne_one hχ) hψ
58 
59 /-- Proposition 6.3 with χ(-1) evaluated in the actual unit group. -/
60 theorem phase_duality {χ : kˣ →* ℂˣ} {ψ : AddChar k ℂ}
61     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
62     phase χ ψ * phase χ⁻¹ ψ = (χ (-1) : ℂ) := by
63   rw [phase_eq, phase_eq, extension_inverse,
64     GaussSums.phase_duality (extension_ne_one hχ) hψ]
65   exact MulChar.ofUnitHom_coe χ (-1)
66 
67 end PaperXI.GaussCharacters

Back to source controls