HeisenbergFrequency.lean

1 import PaperXI.DualCharacterSums
2 import PaperXI.HeisenbergNormalForm
3 import PaperXI.HeisenbergRepresentation
4 
5 /-! Frequency projectors in an arbitrary representation of the actual Heisenberg group.
6 Completeness and translation produce a nonzero modulation-fixed vector without any
7 assumption on the dimension of the target representation. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.HeisenbergFrequency
11 open scoped Classical
12 open PaperXI.Heisenberg
13 
14 variable {K X W : Type*} [Field K] [AddCommGroup X] [Module K X]
15 variable [AddCommGroup W] [Module ℂ W]
16 variable [Fintype (Module.Dual K X)]
17 
18 /-- The literal finite Fourier projector onto frequency `a`. -/
19 def projector (ψ : AddChar K ℂ) (σ : Representation ℂ (Element K X) W) (a : X) :
20     Module.End ℂ W :=
21   (Fintype.card (Module.Dual K X) : ℂ)⁻¹ •
22     ∑ ξ : Module.Dual K X, ψ (-(ξ a)) • σ (modulationElement ξ)
23 
24 @[simp] theorem projector_apply (ψ : AddChar K ℂ)
25     (σ : Representation ℂ (Element K X) W) (a : X) (w : W) :
26     projector ψ σ a w = (Fintype.card (Module.Dual K X) : ℂ)⁻¹ •
27       ∑ ξ : Module.Dual K X, ψ (-(ξ a)) • σ (modulationElement ξ) w := by
28   simp [projector, LinearMap.sum_apply]
29 
30 /-- A projector value has the indicated modulation eigencharacter. -/
31 theorem eigen (ψ : AddChar K ℂ) (σ : Representation ℂ (Element K X) W)
32     (a : X) (η : Module.Dual K X) (w : W) :
33     σ (modulationElement η) (projector ψ σ a w) =
34       ψ (η a) • projector ψ σ a w := by
35   have hphase (ξ : Module.Dual K X) :
36       ψ (-(ξ a)) = ψ (η a) * ψ (-((η + ξ) a)) := by
37     rw [← ψ.map_add_eq_mul]
38     congr 1
39     simp
40   have hshift : (∑ ξ : Module.Dual K X,
41       ψ (-((η + ξ) a)) • σ (modulationElement (η + ξ)) w) =
42       ∑ ξ : Module.Dual K X, ψ (-(ξ a)) • σ (modulationElement ξ) w := by
43     exact Fintype.sum_equiv (Equiv.addLeft η) _ _ (fun _ => rfl)
44   rw [projector_apply, map_smul, map_sum]
45   simp only [map_smul]
46   have hmul (ξ : Module.Dual K X) :
47       σ (modulationElement η) (σ (modulationElement ξ) w) =
48         σ (modulationElement (η + ξ)) w := by
49     rw [← modulationElement_mul, map_mul]
50     rfl
51   simp_rw [hmul]
52   have hs : (∑ ξ : Module.Dual K X,
53       ψ (-(ξ a)) • σ (modulationElement (η + ξ)) w) =
54       ψ (η a) • ∑ ξ : Module.Dual K X,
55         ψ (-((η + ξ) a)) • σ (modulationElement (η + ξ)) w := by
56     rw [Finset.smul_sum]
57     apply Finset.sum_congr rfl
58     intro ξ _
59     rw [hphase ξ, mul_smul]
60   rw [hs, hshift, smul_comm]
61 
62 /-- Finite Fourier completeness as an equality of actual endomorphisms. -/
63 theorem complete [Fintype X] [FiniteDimensional K X]
64     {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
65     (σ : Representation ℂ (Element K X) W) :
66     (∑ a : X, projector ψ σ a) = LinearMap.id := by
67   have hs (ξ : Module.Dual K X) : (∑ a : X, ψ (-(ξ a))) =
68       if ξ = 0 then (Fintype.card X : ℂ) else 0 := by
69     simpa using DualCharacters.sum_over_points hψ (-ξ)
70   have hn : (Fintype.card (Module.Dual K X) : ℂ) ≠ 0 :=
71     Nat.cast_ne_zero.mpr Fintype.card_ne_zero
72   calc
73     (∑ a : X, projector ψ σ a) =
74         (Fintype.card (Module.Dual K X) : ℂ)⁻¹ •
75           ∑ ξ : Module.Dual K X, (∑ a : X, ψ (-(ξ a))) •
76             σ (modulationElement ξ) := by
77       simp only [projector]
78       rw [← Finset.smul_sum, Finset.sum_comm]
79       congr 1
80       apply Finset.sum_congr rfl
81       intro ξ _
82       rw [Finset.sum_smul]
83     _ = (Fintype.card (Module.Dual K X) : ℂ)⁻¹ •
84         ((Fintype.card X : ℂ) • LinearMap.id) := by
85       simp [hs]
86       rfl
87     _ = LinearMap.id := by
88       rw [← DualCharacters.card_dual (K := K) (X := X), ← mul_smul,
89         inv_mul_cancel₀ hn, one_smul]
90 
91 /-- A frequency projector selects its character on any eigenvector. -/
92 theorem projector_of_eigen {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
93     (σ : Representation ℂ (Element K X) W) (a b : X) (w : W)
94     (hw : ∀ ξ : Module.Dual K X, σ (modulationElement ξ) w = ψ (ξ b) • w) :
95     projector ψ σ a w = if a = b then w else 0 := by
96   have hn : (Fintype.card (Module.Dual K X) : ℂ) ≠ 0 :=
97     Nat.cast_ne_zero.mpr Fintype.card_ne_zero
98   have hs : (∑ ξ : Module.Dual K X, ψ (-(ξ a)) •
99       σ (modulationElement ξ) w) =
100       (∑ ξ : Module.Dual K X, ψ (ξ (b - a))) • w := by
101     rw [Finset.sum_smul]
102     apply Finset.sum_congr rfl
103     intro ξ _
104     rw [hw, ← mul_smul, ← ψ.map_add_eq_mul]
105     congr 2
106     simp [sub_eq_add_neg, add_comm]
107   rw [projector_apply, hs, DualCharacters.sum_over_dual hψ]
108   by_cases hab : a = b
109   · simp [hab, ← mul_smul, hn]
110   · have hba : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
111     simp [hab, hba]
112 
113 /-- The projectors are pairwise orthogonal idempotents, without a unitary hypothesis. -/
114 theorem orthogonal_idempotents {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
115     (σ : Representation ℂ (Element K X) W) (a b : X) :
116     projector ψ σ a * projector ψ σ b =
117       if a = b then projector ψ σ a else 0 := by
118   ext w
119   change projector ψ σ a (projector ψ σ b w) = _
120   rw [projector_of_eigen hψ σ a b _ (fun ξ => eigen ψ σ b ξ w)]
121   split_ifs with hab
122   · simp [hab]
123   · rfl
124 
125 omit [Fintype (Module.Dual K X)] in
126 /-- The actual commutation law after imposing the central character. -/
127 theorem modulation_translation_action (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
128     (σ : Representation ℂ (Element K X) W)
129     (hcentral : ∀ z : K, σ (centralElement z) = ψ z • LinearMap.id)
130     (ξ : Module.Dual K X) (x : X) (w : W) :
131     σ (modulationElement ξ) (σ (translationElement x) w) =
132       ψ (-(ξ x)) • σ (translationElement x) (σ (modulationElement ξ) w) := by
133   calc
134     σ (modulationElement ξ) (σ (translationElement x) w) =
135         σ (modulationElement ξ * translationElement x) w := by
136       rw [map_mul]
137       rfl
138     _ = σ (centralElement (-(ξ x)) *
139         (translationElement x * modulationElement ξ)) w := by
140       rw [modulation_translation h2]
141     _ = ψ (-(ξ x)) • σ (translationElement x)
142         (σ (modulationElement ξ) w) := by
143       rw [map_mul, map_mul, hcentral]
144       rfl
145 
146 /-- Translation shifts a frequency by minus its position, with the source convention. -/
147 theorem translation_covariance (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
148     (σ : Representation ℂ (Element K X) W)
149     (hcentral : ∀ z : K, σ (centralElement z) = ψ z • LinearMap.id)
150     (a x : X) :
151     σ (translationElement x) * projector ψ σ a =
152       projector ψ σ (a - x) * σ (translationElement x) := by
153   ext w
154   change σ (translationElement x) (projector ψ σ a w) =
155     projector ψ σ (a - x) (σ (translationElement x) w)
156   simp only [projector_apply, map_smul, map_sum]
157   congr 1
158   apply Finset.sum_congr rfl
159   intro ξ _
160   rw [modulation_translation_action ψ h2 σ hcentral, ← mul_smul,
161     ← ψ.map_add_eq_mul]
162   congr 2
163   simp only [map_sub]
164   abel
165 
166 /-- Every nonzero target has a nonzero vector in the zero-frequency fiber.
167 Completeness first gives a nonzero projector value; an invertible translation
168 moves its frequency to zero. No irreducibility or target dimension is assumed. -/
169 theorem nonzero_zero_fiber [Fintype X] [FiniteDimensional K X] [Nontrivial W]
170     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
171     (σ : Representation ℂ (Element K X) W)
172     (hcentral : ∀ z : K, σ (centralElement z) = ψ z • LinearMap.id) :
173     ∃ w₀ : W, w₀ ≠ 0 ∧
174       ∀ ξ : Module.Dual K X, σ (modulationElement ξ) w₀ = w₀ := by
175   obtain ⟨w, hw⟩ := exists_ne (0 : W)
176   have hex : ∃ a : X, projector ψ σ a w ≠ 0 := by
177     by_contra! h
178     have hh := congrArg (fun f : Module.End ℂ W => f w) (complete hψ σ)
179     simp only [LinearMap.sum_apply, LinearMap.id_apply] at hh
180     simp only [h, Finset.sum_const_zero] at hh
181     exact hw hh.symm
182   obtain ⟨a, ha⟩ := hex
183   refine ⟨σ (translationElement a) (projector ψ σ a w), ?_, ?_⟩
184   · intro hz
185     apply ha
186     have hh := congrArg (fun v : W => σ (translationElement (-a)) v) hz
187     have hinv : σ (translationElement (-a))
188         (σ (translationElement a) (projector ψ σ a w)) = projector ψ σ a w := by
189       rw [← Module.End.mul_apply, ← map_mul, translationElement_mul]
190       simp
191     simpa only [hinv, map_zero] using hh
192   · intro ξ
193     rw [modulation_translation_action ψ h2 σ hcentral, eigen, map_smul,
194       ← mul_smul, ← ψ.map_add_eq_mul]
195     simp
196 
197 end PaperXI.HeisenbergFrequency

Back to source controls