SchrodingerOperator.lean

1 import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
2 import Mathlib.LinearAlgebra.Dual.Defs
3 import Mathlib.RepresentationTheory.Basic
4 
5 /-! The literal Schrödinger operators in the manuscript's sign convention. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.Schrodinger
9 open scoped BigOperators
10 
11 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
12 
13 def operator (ψ : AddChar K ℂ) (x : X) (ξ : Module.Dual K X) (z : K) :
14     Module.End ℂ (X → ℂ) where
15   toFun f u := ψ (z + ξ u + (2 : K)⁻¹ * ξ x) * f (u + x)
16   map_add' f g := by
17     funext u
18     simp only [Pi.add_apply]
19     ring
20   map_smul' a f := by
21     funext u
22     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
23     ring
24 
25 @[simp] theorem operator_apply (ψ : AddChar K ℂ) (x : X) (ξ : Module.Dual K X)
26     (z : K) (f : X → ℂ) (u : X) :
27     operator ψ x ξ z f u = ψ (z + ξ u + (2 : K)⁻¹ * ξ x) * f (u + x) := rfl
28 
29 def translation (x : X) : Module.End ℂ (X → ℂ) where
30   toFun f u := f (u + x)
31   map_add' _ _ := rfl
32   map_smul' _ _ := rfl
33 
34 @[simp] theorem translation_apply (x : X) (f : X → ℂ) (u : X) :
35     translation x f u = f (u + x) := rfl
36 
37 def modulation (ψ : AddChar K ℂ) (ξ : Module.Dual K X) :
38     Module.End ℂ (X → ℂ) where
39   toFun f u := ψ (ξ u) * f u
40   map_add' f g := by
41     funext u
42     simp only [Pi.add_apply]
43     ring
44   map_smul' a f := by
45     funext u
46     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
47     ring
48 
49 @[simp] theorem modulation_apply (ψ : AddChar K ℂ) (ξ : Module.Dual K X)
50     (f : X → ℂ) (u : X) : modulation ψ ξ f u = ψ (ξ u) * f u := rfl
51 
52 theorem operator_translation (ψ : AddChar K ℂ) (x : X) :
53     operator ψ x 0 0 = translation x := by
54   ext f u
55   simp [translation]
56 
57 theorem operator_modulation (ψ : AddChar K ℂ) (ξ : Module.Dual K X) :
58     operator ψ 0 ξ 0 = modulation ψ ξ := by
59   ext f u
60   simp [modulation]
61 
62 theorem operator_central (ψ : AddChar K ℂ) (z : K) :
63     operator ψ (0 : X) 0 z = ψ z • LinearMap.id := by
64   ext f u
65   simp
66 
67 theorem operator_one (ψ : AddChar K ℂ) :
68     operator ψ (0 : X) 0 0 = LinearMap.id := by
69   rw [operator_central]
70   simp
71 
72 /-- The phase identity verifies the manuscript's half-symplectic cocycle. -/
73 theorem phase_add (h2 : (2 : K) ≠ 0) (x y u : X) (ξ η : Module.Dual K X)
74     (z t : K) :
75     (z + ξ u + (2 : K)⁻¹ * ξ x) +
76       (t + η (u + x) + (2 : K)⁻¹ * η y) =
77     z + t + (2 : K)⁻¹ * (η x - ξ y) +
78       (ξ + η) u + (2 : K)⁻¹ * (ξ + η) (x + y) := by
79   simp only [map_add, LinearMap.add_apply]
80   field_simp
81   ring
82 
83 theorem operator_mul (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
84     (x y : X) (ξ η : Module.Dual K X) (z t : K) :
85     operator ψ x ξ z * operator ψ y η t =
86       operator ψ (x + y) (ξ + η) (z + t + (2 : K)⁻¹ * (η x - ξ y)) := by
87   ext f u
88   change ψ (z + ξ u + (2 : K)⁻¹ * ξ x) *
89     (ψ (t + η (u + x) + (2 : K)⁻¹ * η y) * f ((u + x) + y)) = _
90   rw [← mul_assoc, ← ψ.map_add_eq_mul, phase_add h2]
91   simp [add_assoc]
92 
93 end PaperXI.Schrodinger

Back to source controls