SchrodingerUniversal.lean

1 import PaperXI.HeisenbergNormalForm
2 import PaperXI.HeisenbergFrequency
3 import PaperXI.HeisenbergDimension
4 import PaperXI.HeisenbergRepresentation
5 import PaperXI.SchurScalar
6 import Mathlib.LinearAlgebra.StdBasis
7 
8 /-! The actual map from the Schrödinger model, built from a nonzero vector
9 fixed by all modulations, and its representation equivalence. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.SchrodingerUniversal
13 open PaperXI.Heisenberg
14 variable {K X W : Type*} [Field K] [AddCommGroup X] [Module K X] [Fintype X]
15 variable [AddCommGroup W] [Module ℂ W]
16 
17 /-- The coordinate basis vector at `a` maps to `σ(T_(-a)) w₀`. -/
18 def basis_map (σ : Representation ℂ (Element K X) W) (w₀ : W) :
19     (X → ℂ) →ₗ[ℂ] W :=
20   (Pi.basisFun ℂ X).constr ℂ (fun a => σ (translationElement (-a)) w₀)
21 
22 @[simp] theorem basis_map_basis (σ : Representation ℂ (Element K X) W)
23     (w₀ : W) (a : X) :
24     basis_map σ w₀ (Pi.basisFun ℂ X a) = σ (translationElement (-a)) w₀ := by
25   exact (Pi.basisFun ℂ X).constr_basis ℂ _ a
26 
27 /-- With the manuscript convention, translation moves `δ_a` to `δ_(a-x)`. -/
28 theorem translation_basis (x a : X) :
29     Schrodinger.translation x (Pi.basisFun ℂ X a) = Pi.basisFun ℂ X (a - x) := by
30   classical
31   ext u
32   simp [Pi.single_apply, ← eq_sub_iff_add_eq]
33 
34 theorem modulation_basis (ψ : AddChar K ℂ) (ξ : Module.Dual K X) (a : X) :
35     Schrodinger.modulation ψ ξ (Pi.basisFun ℂ X a) = ψ (ξ a) • Pi.basisFun ℂ X a := by
36   classical
37   ext u
38   by_cases h : u = a
39   · subst u
40     simp
41   · simp [h]
42 
43 theorem basis_map_translation (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
44     (σ : Representation ℂ (Element K X) W) (w₀ : W) (x : X) :
45     (basis_map σ w₀).comp (representation ψ h2 (translationElement x)) =
46       (σ (translationElement x)).comp (basis_map σ w₀) := by
47   apply (Pi.basisFun ℂ X).ext
48   intro a
49   simp only [LinearMap.comp_apply, translation_action, translation_basis, basis_map_basis]
50   change σ (translationElement (-(a - x))) w₀ =
51     (σ (translationElement x) * σ (translationElement (-a))) w₀
52   rw [← map_mul, translationElement_mul]
53   congr 2
54   abel_nf
55 
56 theorem basis_map_modulation (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
57     (σ : Representation ℂ (Element K X) W)
58     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
59     (w₀ : W) (hfixed : ∀ ξ, σ (modulationElement ξ) w₀ = w₀)
60     (ξ : Module.Dual K X) :
61     (basis_map σ w₀).comp (representation ψ h2 (modulationElement ξ)) =
62       (σ (modulationElement ξ)).comp (basis_map σ w₀) := by
63   apply (Pi.basisFun ℂ X).ext
64   intro a
65   simp only [LinearMap.comp_apply, modulation_action, modulation_basis, map_smul,
66     basis_map_basis]
67   change ψ (ξ a) • σ (translationElement (-a)) w₀ =
68     (σ (modulationElement ξ) * σ (translationElement (-a))) w₀
69   rw [← map_mul, modulation_translation h2, map_mul, map_mul, hcentral]
70   simp [hfixed]
71 
72 theorem basis_map_central (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
73     (σ : Representation ℂ (Element K X) W)
74     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
75     (w₀ : W) (z : K) :
76     (basis_map σ w₀).comp (representation ψ h2 (centralElement z)) =
77       (σ (centralElement z)).comp (basis_map σ w₀) := by
78   rw [central_action, hcentral]
79   ext f
80   simp
81 
82 /-- Generator intertwinement extends to every actual group element by its normal form. -/
83 theorem intertwines (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
84     (σ : Representation ℂ (Element K X) W)
85     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
86     (w₀ : W) (hfixed : ∀ ξ, σ (modulationElement ξ) w₀ = w₀)
87     (g : Element K X) :
88     (basis_map σ w₀).comp (representation ψ h2 g) =
89       (σ g).comp (basis_map σ w₀) := by
90   have hc := basis_map_central ψ h2 σ hcentral w₀
91   have ht := basis_map_translation ψ h2 σ w₀
92   have hm := basis_map_modulation ψ h2 σ hcentral w₀ hfixed
93   rw [normal_form g]
94   ext f
95   simp only [map_mul, LinearMap.comp_apply, Module.End.mul_apply]
96   have hc' (z : K) (v : X → ℂ) := LinearMap.congr_fun (hc z) v
97   have ht' (x : X) (v : X → ℂ) := LinearMap.congr_fun (ht x) v
98   have hm' (ξ : Module.Dual K X) (v : X → ℂ) := LinearMap.congr_fun (hm ξ) v
99   simp only [LinearMap.comp_apply] at hc' ht' hm'
100   rw [hc', ht', hm']
101 
102 /-- The constructed map bundled with the actual representation actions. -/
103 def intertwiningMap (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
104     (σ : Representation ℂ (Element K X) W)
105     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
106     (w₀ : W) (hfixed : ∀ ξ, σ (modulationElement ξ) w₀ = w₀) :
107     Representation.IntertwiningMap (representation ψ h2) σ :=
108   ⟨basis_map σ w₀, intertwines ψ h2 σ hcentral w₀ hfixed⟩
109 
110 /-- The map is nonzero because its value at the origin basis vector is `w₀`. -/
111 theorem intertwiningMap_ne_zero (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
112     (σ : Representation ℂ (Element K X) W)
113     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
114     (w₀ : W) (hw₀ : w₀ ≠ 0) (hfixed : ∀ ξ, σ (modulationElement ξ) w₀ = w₀) :
115     intertwiningMap ψ h2 σ hcentral w₀ hfixed ≠ 0 := by
116   intro h
117   have hh := congrArg (fun F : Representation.IntertwiningMap (representation ψ h2) σ =>
118     F (Pi.basisFun ℂ X 0)) h
119   exact hw₀ (by simpa [intertwiningMap] using hh)
120 
121 /-- Irreducibility of both actual actions proves bijectivity; it is not assumed. -/
122 def equiv_of_fixed (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
123     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
124     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
125     (w₀ : W) (hw₀ : w₀ ≠ 0) (hfixed : ∀ ξ, σ (modulationElement ξ) w₀ = w₀) :
126     Representation.Equiv (representation ψ h2) σ := by
127   letI : Representation.IsIrreducible (representation (X := X) ψ h2) :=
128     irreducible ψ hψ h2
129   exact (intertwiningMap ψ h2 σ hcentral w₀ hfixed).ofBijective
130     ((Representation.IsIrreducible.bijective_or_eq_zero _).resolve_right
131       (intertwiningMap_ne_zero ψ h2 σ hcentral w₀ hw₀ hfixed))
132 
133 variable [Fintype (Module.Dual K X)] [FiniteDimensional K X]
134 
135 /-- Finite Stone–von Neumann for the actual odd-characteristic coordinate group:
136 every irreducible representation with central character `ψ ≠ 1` is the model.
137 The fixed vector, bijectivity, and target dimension are conclusions of the proof. -/
138 theorem exists_equiv (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
139     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
140     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
141     Nonempty (Representation.Equiv (representation ψ h2) σ) := by
142   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space σ
143   obtain ⟨w₀, hw₀, hfixed⟩ :=
144     HeisenbergFrequency.nonzero_zero_fiber ψ hψ h2 σ hcentral
145   exact ⟨equiv_of_fixed ψ hψ h2 σ hcentral w₀ hw₀ hfixed⟩
146 
147 /-- A chosen actual equivalence supplied by finite Stone–von Neumann. -/
148 def equiv (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
149     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
150     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
151     Representation.Equiv (representation ψ h2) σ :=
152   Classical.choice (exists_equiv ψ hψ h2 σ hcentral)
153 
154 /-- The chosen linear equivalence intertwines every actual group element. -/
155 theorem equiv_intertwines (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
156     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
157     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
158     (g : Element K X) (f : X → ℂ) :
159     equiv ψ hψ h2 σ hcentral ((representation ψ h2 g) f) =
160       σ g (equiv ψ hψ h2 σ hcentral f) :=
161   Representation.IntertwiningMap.isIntertwining (representation ψ h2) σ
162     (equiv ψ hψ h2 σ hcentral).toIntertwiningMap g f
163 
164 /-- Finite dimensionality of the arbitrary irreducible target is transported
165 from the constructed model equivalence. -/
166 theorem finiteDimensional (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
167     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
168     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
169     FiniteDimensional ℂ W := by
170   let U := (equiv ψ hψ h2 σ hcentral).toLinearEquiv
171   exact FiniteDimensional.of_injective U.symm.toLinearMap U.symm.injective
172 
173 /-- The actual target dimension is the number of position coordinates. -/
174 theorem finrank_eq (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
175     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
176     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
177     Module.finrank ℂ W = Fintype.card X := by
178   rw [← (equiv ψ hψ h2 σ hcentral).toLinearEquiv.finrank_eq]
179   exact Module.finrank_fintype_fun_eq_card ℂ
180 
181 /-- The target dimension equals the square root of the symplectic quotient order. -/
182 theorem finrank_eq_sqrt (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
183     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
184     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
185     Module.finrank ℂ W = Nat.sqrt (Nat.card (X × Module.Dual K X)) := by
186   rw [finrank_eq ψ hψ h2 σ hcentral, HeisenbergDimension.sqrt_natCard_symplectic,
187     Nat.card_eq_fintype_card]
188 
189 /-- Every invertible intertwiner differs from the constructed equivalence
190 by a unique nonzero complex scalar. -/
191 theorem unique_scalar (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
192     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
193     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
194     (T : (X → ℂ) ≃ₗ[ℂ] W)
195     (hT : ∀ g f, T ((representation ψ h2 g) f) = σ g (T f)) :
196     ∃! c : ℂˣ, ∀ f, T f = (c : ℂ) • equiv ψ hψ h2 σ hcentral f := by
197   let : Representation.IsIrreducible (representation (X := X) ψ h2) :=
198     irreducible ψ hψ h2
199   exact SchurScalar.bridge_unique (representation ψ h2) σ
200     (equiv ψ hψ h2 σ hcentral).toLinearEquiv T
201     (equiv_intertwines ψ hψ h2 σ hcentral) hT
202 
203 omit [Fintype X] [Fintype (Module.Dual K X)] in
204 /-- The finite-field formulation needs no separately supplied enumeration
205 of the position or dual space. -/
206 theorem exists_equiv_finiteField [Finite K]
207     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
208     (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
209     (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
210     Nonempty (Representation.Equiv (representation ψ h2) σ) := by
211   let : Finite X := Module.finite_of_finite K
212   let : Finite (Module.Dual K X) := Module.finite_of_finite K
213   let : Fintype X := Fintype.ofFinite X
214   let : Fintype (Module.Dual K X) := Fintype.ofFinite (Module.Dual K X)
215   exact exists_equiv ψ hψ h2 σ hcentral
216 
217 end PaperXI.SchrodingerUniversal

Back to source controls