HeisenbergGroup.lean

1 import Mathlib.LinearAlgebra.Dual.Lemmas
2 import Mathlib.Tactic.Ring
3 
4 /-! The Heisenberg group in position, frequency, and central coordinates.
5 The alternating bilinear cocycle defines a group in every characteristic.
6 Identifying its commutator with the symplectic pairing additionally needs 2 ≠ 0. -/
7 set_option autoImplicit false
8 
9 namespace PaperXI.Heisenberg
10 
11 @[ext]
12 structure Element (K X : Type*) [Field K] [AddCommGroup X] [Module K X] where
13   position : X
14   frequency : Module.Dual K X
15   central : K
16 
17 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
18 
19 instance instMul : Mul (Element K X) where
20   mul a b := ⟨a.position + b.position, a.frequency + b.frequency,
21     a.central + b.central + (2 : K)⁻¹ * (b.frequency a.position - a.frequency b.position)⟩
22 
23 instance instOne : One (Element K X) where
24   one := ⟨0, 0, 0⟩
25 
26 instance instInv : Inv (Element K X) where
27   inv a := ⟨-a.position, -a.frequency, -a.central⟩
28 
29 @[simp] theorem mul_position (a b : Element K X) :
30     (a * b).position = a.position + b.position := rfl
31 
32 @[simp] theorem mul_frequency (a b : Element K X) :
33     (a * b).frequency = a.frequency + b.frequency := rfl
34 
35 @[simp] theorem mul_central (a b : Element K X) :
36     (a * b).central = a.central + b.central +
37       (2 : K)⁻¹ * (b.frequency a.position - a.frequency b.position) := rfl
38 
39 @[simp] theorem one_position : (1 : Element K X).position = 0 := rfl
40 @[simp] theorem one_frequency : (1 : Element K X).frequency = 0 := rfl
41 @[simp] theorem one_central : (1 : Element K X).central = 0 := rfl
42 @[simp] theorem inv_position (a : Element K X) : a⁻¹.position = -a.position := rfl
43 @[simp] theorem inv_frequency (a : Element K X) : a⁻¹.frequency = -a.frequency := rfl
44 @[simp] theorem inv_central (a : Element K X) : a⁻¹.central = -a.central := rfl
45 
46 /-- The alternating cocycle gives the actual Heisenberg group operation. -/
47 instance instGroup : Group (Element K X) where
48   mul_assoc a b c := by
49     ext <;> simp [add_assoc, map_add]
50     ring
51   one_mul a := by
52     ext <;> simp
53   mul_one a := by
54     ext <;> simp
55   inv_mul_cancel a := by
56     ext <;> simp
57 
58 /-- Pure central elements. -/
59 def centralElement (z : K) : Element K X := ⟨0, 0, z⟩
60 
61 /-- Pure position elements act by translation in the Schrödinger model. -/
62 def translationElement (x : X) : Element K X := ⟨x, 0, 0⟩
63 
64 /-- Pure frequency elements act by modulation in the Schrödinger model. -/
65 def modulationElement (ξ : Module.Dual K X) : Element K X := ⟨0, ξ, 0⟩
66 
67 @[simp] theorem centralElement_position (z : K) :
68     (centralElement (X := X) z).position = 0 := rfl
69 @[simp] theorem centralElement_frequency (z : K) :
70     (centralElement (X := X) z).frequency = 0 := rfl
71 @[simp] theorem centralElement_central (z : K) :
72     (centralElement (X := X) z).central = z := rfl
73 @[simp] theorem translationElement_position (x : X) :
74     (translationElement (K := K) x).position = x := rfl
75 @[simp] theorem translationElement_frequency (x : X) :
76     (translationElement (K := K) x).frequency = 0 := rfl
77 @[simp] theorem translationElement_central (x : X) :
78     (translationElement (K := K) x).central = 0 := rfl
79 @[simp] theorem modulationElement_position (ξ : Module.Dual K X) :
80     (modulationElement ξ).position = 0 := rfl
81 @[simp] theorem modulationElement_frequency (ξ : Module.Dual K X) :
82     (modulationElement ξ).frequency = ξ := rfl
83 @[simp] theorem modulationElement_central (ξ : Module.Dual K X) :
84     (modulationElement ξ).central = 0 := rfl
85 
86 @[simp] theorem centralElement_zero : centralElement (X := X) (0 : K) = 1 := rfl
87 @[simp] theorem translationElement_zero : translationElement (K := K) (0 : X) = 1 := rfl
88 @[simp] theorem modulationElement_zero :
89     modulationElement (0 : Module.Dual K X) = 1 := rfl
90 
91 @[simp] theorem centralElement_mul (z t : K) :
92     centralElement (X := X) z * centralElement t = centralElement (z + t) := by
93   ext <;> simp
94 
95 @[simp] theorem translationElement_mul (x y : X) :
96     translationElement (K := K) x * translationElement y = translationElement (x + y) := by
97   ext <;> simp
98 
99 @[simp] theorem modulationElement_mul (ξ η : Module.Dual K X) :
100     modulationElement ξ * modulationElement η = modulationElement (ξ + η) := by
101   ext <;> simp
102 
103 /-- The central coordinate commutes with every group element. -/
104 theorem centralElement_commute (z : K) (a : Element K X) :
105     Commute (centralElement z) a := by
106   show centralElement z * a = a * centralElement z
107   ext <;> simp [add_comm]
108 
109 end PaperXI.Heisenberg

Back to source controls