HeisenbergTransport.lean

1 import PaperXI.HeisenbergRepresentation
2 import PaperXI.HeisenbergForm
3 import Mathlib.RepresentationTheory.Irreducible
4 
5 /-! Transport of the coordinate Heisenberg group and actual representations.
6 The lift preserves the alternating cocycle in every characteristic. Its use
7 as the nondegenerate Heisenberg extension requires odd characteristic.
8 No coordinates on an abstract symplectic space are asserted here. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.HeisenbergTransport
12 
13 open Heisenberg
14 
15 variable {K X Y Z : Type*} [Field K]
16 variable [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y]
17 variable [AddCommGroup Z] [Module K Z]
18 
19 /-- The position and frequency coordinates together. -/
20 def vector (a : Element K X) : X × Module.Dual K X := (a.position, a.frequency)
21 
22 @[simp] theorem vector_mul (a b : Element K X) : vector (a * b) = vector a + vector b := rfl
23 
24 /-- Preservation of the actual alternating form, with the manuscript's sign. -/
25 def PreservesForm (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y)) : Prop :=
26   ∀ v w, HeisenbergForm.form (e v) (e w) = HeisenbergForm.form v w
27 
28 theorem preservesForm_refl : PreservesForm (LinearEquiv.refl K (X × Module.Dual K X)) :=
29   fun _ _ => rfl
30 
31 theorem PreservesForm.symm
32     {e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y)}
33     (he : PreservesForm e) : PreservesForm e.symm := by
34   intro v w
35   simpa using (he (e.symm v) (e.symm w)).symm
36 
37 theorem PreservesForm.trans
38     {e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y)}
39     {f : (Y × Module.Dual K Y) ≃ₗ[K] (Z × Module.Dual K Z)}
40     (he : PreservesForm e) (hf : PreservesForm f) : PreservesForm (e.trans f) := by
41   intro v w
42   exact (hf (e v) (e w)).trans (he v w)
43 
44 /-- Lift an arbitrary form-preserving coordinate linear equivalence, fixing
45 the central coordinate. The map need not preserve either polarization. -/
46 def liftIsometry
47     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y))
48     (he : PreservesForm e) : Element K X ≃* Element K Y where
49   toFun a := ⟨(e (vector a)).1, (e (vector a)).2, a.central⟩
50   invFun a := ⟨(e.symm (vector a)).1, (e.symm (vector a)).2, a.central⟩
51   left_inv a := by
52     apply Element.ext
53     · exact congrArg Prod.fst (e.symm_apply_apply (vector a))
54     · exact congrArg Prod.snd (e.symm_apply_apply (vector a))
55     · rfl
56   right_inv a := by
57     apply Element.ext
58     · exact congrArg Prod.fst (e.apply_symm_apply (vector a))
59     · exact congrArg Prod.snd (e.apply_symm_apply (vector a))
60     · rfl
61   map_mul' a b := by
62     apply Element.ext
63     · exact congrArg Prod.fst (e.map_add (vector a) (vector b))
64     · exact congrArg Prod.snd (e.map_add (vector a) (vector b))
65     · change a.central + b.central + (2 : K)⁻¹ * HeisenbergForm.form (vector a) (vector b) =
66         a.central + b.central + (2 : K)⁻¹ * HeisenbergForm.form (e (vector a)) (e (vector b))
67       rw [he]
68 
69 @[simp] theorem liftIsometry_vector
70     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y))
71     (he : PreservesForm e) (a : Element K X) :
72     vector (liftIsometry e he a) = e (vector a) := rfl
73 
74 @[simp] theorem liftIsometry_central
75     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y))
76     (he : PreservesForm e) (a : Element K X) :
77     (liftIsometry e he a).central = a.central := rfl
78 
79 @[simp] theorem liftIsometry_centralElement
80     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y))
81     (he : PreservesForm e) (z : K) :
82     liftIsometry e he (centralElement z) = centralElement z := by
83   apply Element.ext
84   · change (e 0).1 = 0
85     simp
86   · change (e 0).2 = 0
87     simp
88   · rfl
89 
90 @[simp] theorem liftIsometry_refl :
91     liftIsometry (LinearEquiv.refl K (X × Module.Dual K X)) preservesForm_refl =
92       MulEquiv.refl (Element K X) := by
93   ext a <;> rfl
94 
95 @[simp] theorem liftIsometry_symm
96     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y))
97     (he : PreservesForm e) :
98     (liftIsometry e he).symm = liftIsometry e.symm he.symm := by
99   ext a <;> rfl
100 
101 @[simp] theorem liftIsometry_trans
102     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y))
103     (f : (Y × Module.Dual K Y) ≃ₗ[K] (Z × Module.Dual K Z))
104     (he : PreservesForm e) (hf : PreservesForm f) :
105     (liftIsometry e he).trans (liftIsometry f hf) =
106       liftIsometry (e.trans f) (he.trans hf) := by
107   ext a <;> rfl
108 
109 section Pullback
110 
111 variable {k G H W : Type*} [Field k] [Group G] [Group H]
112 variable [AddCommGroup W] [Module k W]
113 
114 /-- Pull back an actual representation through a group equivalence. -/
115 def pullback (e : G ≃* H) (σ : Representation k H W) : Representation k G W :=
116   σ.comp e.toMonoidHom
117 
118 @[simp] theorem pullback_apply (e : G ≃* H) (σ : Representation k H W) (g : G) :
119     pullback e σ g = σ (e g) := rfl
120 
121 @[simp] theorem pullback_refl (σ : Representation k G W) :
122     pullback (MulEquiv.refl G) σ = σ := by
123   ext
124   rfl
125 
126 theorem pullback_trans {J : Type*} [Group J] (e : G ≃* H) (f : H ≃* J)
127     (σ : Representation k J W) :
128     pullback e (pullback f σ) = pullback (e.trans f) σ := rfl
129 
130 @[simp] theorem pullback_symm (e : G ≃* H) (σ : Representation k G W) :
131     pullback e (pullback e.symm σ) = σ := by
132   ext g
133   simp
134 
135 /-- Surjectivity of the group equivalence identifies all stable subspaces. -/
136 def pullbackSubrepresentationEquiv (e : G ≃* H) (σ : Representation k H W) :
137     Subrepresentation (pullback e σ) ≃o Subrepresentation σ where
138   toFun S := ⟨S.toSubmodule, fun h _ hv => by
139     simpa using S.apply_mem_toSubmodule (e.symm h) hv⟩
140   invFun S := ⟨S.toSubmodule, fun g _ hv => S.apply_mem_toSubmodule (e g) hv⟩
141   left_inv _ := Subrepresentation.toSubmodule_injective rfl
142   right_inv _ := Subrepresentation.toSubmodule_injective rfl
143   map_rel_iff' := Iff.rfl
144 
145 theorem pullback_irreducible_iff (e : G ≃* H) (σ : Representation k H W) :
146     Representation.IsIrreducible (pullback e σ) ↔ Representation.IsIrreducible σ :=
147   (pullbackSubrepresentationEquiv e σ).isSimpleOrder_iff
148 
149 theorem pullback_irreducible (e : G ≃* H) (σ : Representation k H W)
150     [Representation.IsIrreducible σ] : Representation.IsIrreducible (pullback e σ) :=
151   (pullback_irreducible_iff e σ).mpr inferInstance
152 
153 /-- Transport scalar action on a parameterized subgroup through an actual
154 group equivalence. In particular this accepts a supplied extension lift. -/
155 theorem pullback_scalar_action {C : Type*} (e : G ≃* H)
156     (cG : C → G) (cH : C → H) (he : ∀ z, e (cG z) = cH z)
157     (σ : Representation k H W) (ψ : C → k)
158     (hσ : ∀ z, σ (cH z) = ψ z • LinearMap.id) (z : C) :
159     pullback e σ (cG z) = ψ z • LinearMap.id := by
160   rw [pullback_apply, he, hσ]
161 
162 end Pullback
163 
164 section CentralAction
165 
166 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
167 
168 /-- Central action is preserved by a coordinate group equivalence fixing
169 the parameterized central subgroup. -/
170 theorem pullback_central_action
171     (e : Element K X ≃* Element K Y)
172     (he : ∀ z, e (centralElement z) = centralElement z)
173     (σ : Representation ℂ (Element K Y) W) (ψ : AddChar K ℂ)
174     (hσ : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) (z : K) :
175     pullback e σ (centralElement z) = ψ z • LinearMap.id := by
176   rw [pullback_apply, he, hσ]
177 
178 end CentralAction
179 
180 end PaperXI.HeisenbergTransport

Back to source controls