FourierProjectors.lean

1 import PaperXI.CyclicAction
2 
3 /-! Finite Fourier projectors derived from cyclic representation laws and a
4 primitive additive character. No idempotence or orthogonality is assumed. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.FourierProjectors
8 open scoped BigOperators
9 open PaperXI.CyclicAction
10 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
11 variable {M : ℕ} [NeZero M]
12 
13 def projector (ρ : Action (K := K) (V := V) (M := M))
14     (ψ : AddChar (ZMod M) K) (j : ZMod M) : Module.End K V :=
15   PaperXI.FourierCovariance.fourierOperator (operator ρ) ψ j
16 
17 theorem projector_formula (ρ : Action (K := K) (V := V) (M := M))
18     (ψ : AddChar (ZMod M) K) (j : ZMod M) :
19     projector ρ ψ j = (M : K)⁻¹ • ∑ a : ZMod M, ψ (-j * a) • operator ρ a := rfl
20 
21 theorem character_sum (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive) (t : ZMod M) :
22     (∑ a : ZMod M, ψ (t * a)) = if t = 0 then (M : K) else 0 := by
23   simpa [mul_comm] using AddChar.sum_mulShift t hψ
24 
25 /-- Every projected vector has the declared inertia character. -/
26 theorem action_projector (ρ : Action (K := K) (V := V) (M := M))
27     (ψ : AddChar (ZMod M) K) (j b : ZMod M) :
28     operator ρ b * projector ρ ψ j = ψ (j * b) • projector ρ ψ j := by
29   have hs : (∑ a : ZMod M, ψ (-j * a) • operator ρ (b + a)) =
30       ψ (j * b) • ∑ a : ZMod M, ψ (-j * a) • operator ρ a := by
31     rw [Finset.smul_sum]
32     apply Fintype.sum_equiv (Equiv.addLeft b)
33     intro a
34     change ψ (-j * a) • operator ρ (b + a) =
35       ψ (j * b) • (ψ (-j * (b + a)) • operator ρ (b + a))
36     simp only [smul_smul, ← AddChar.map_add_eq_mul]
37     congr 2
38     ring
39   rw [projector_formula, mul_smul_comm, Finset.mul_sum]
40   simp_rw [mul_smul_comm, ← operator_add]
41   rw [hs]
42   exact smul_comm _ _ _
43 
44 theorem projector_product (ρ : Action (K := K) (V := V) (M := M))
45     (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive) (hM : (M : K) ≠ 0)
46     (i j : ZMod M) :
47     projector ρ ψ i * projector ρ ψ j = if i = j then projector ρ ψ j else 0 := by
48   rw [projector_formula ρ ψ i, smul_mul_assoc, Finset.sum_mul]
49   simp_rw [smul_mul_assoc, action_projector, smul_smul, ← AddChar.map_add_eq_mul]
50   have h : ∀ a : ZMod M, -i * a + j * a = (j - i) * a := by intro a; ring
51   simp_rw [h]
52   rw [← Finset.sum_smul, character_sum ψ hψ]
53   by_cases hij : i = j
54   · subst j; simp [hM, smul_smul]
55   · have hji : j - i ≠ 0 := sub_ne_zero.mpr (Ne.symm hij)
56     simp [hji, hij]
57 
58 theorem projector_idempotent (ρ : Action (K := K) (V := V) (M := M))
59     (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive) (hM : (M : K) ≠ 0)
60     (j : ZMod M) : projector ρ ψ j ^ 2 = projector ρ ψ j := by
61   simpa [pow_two] using projector_product ρ ψ hψ hM j j
62 
63 theorem projector_orthogonal (ρ : Action (K := K) (V := V) (M := M))
64     (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive) (hM : (M : K) ≠ 0)
65     {i j : ZMod M} (hij : i ≠ j) : projector ρ ψ i * projector ρ ψ j = 0 := by
66   simpa [hij] using projector_product ρ ψ hψ hM i j
67 
68 theorem projector_complete (ρ : Action (K := K) (V := V) (M := M))
69     (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive) (hM : (M : K) ≠ 0) :
70     (∑ j : ZMod M, projector ρ ψ j) = 1 := by
71   have hs (a : ZMod M) : (∑ j : ZMod M, ψ (-j * a)) =
72       if a = 0 then (M : K) else 0 := by
73     simpa [mul_comm, neg_mul, mul_neg] using character_sum ψ hψ (-a)
74   simp only [projector_formula, ← Finset.smul_sum]
75   rw [Finset.sum_comm]
76   simp_rw [← Finset.sum_smul, hs]
77   simp [hM, smul_smul]
78 
79 end PaperXI.FourierProjectors

Back to source controls