HeisenbergCenter.lean

1 import PaperXI.HeisenbergGroup
2 import PaperXI.HeisenbergCardinality
3 import Mathlib.GroupTheory.Subgroup.Center
4 import Mathlib.Tactic.LinearCombination
5 
6 /-! The center is proved to consist exactly of the central-coordinate elements. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HeisenbergCenter
10 
11 open PaperXI.Heisenberg PaperXI.HeisenbergForm
12 
13 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
14 
15 theorem commute_iff (h2 : (2 : K) ≠ 0) (a b : Element K X) :
16     a * b = b * a ↔ form (a.position, a.frequency) (b.position, b.frequency) = 0 := by
17   constructor
18   · intro h
19     have hc := congrArg Element.central h
20     simp only [mul_central] at hc
21     have hz : 2 * (2 : K)⁻¹ *
22         (b.frequency a.position - a.frequency b.position) = 0 := by
23       linear_combination hc
24     simpa [h2] using hz
25   · intro h
26     have hz : b.frequency a.position - a.frequency b.position = 0 := h
27     have hr : a.frequency b.position - b.frequency a.position = 0 := by
28       rw [sub_eq_zero] at hz ⊢
29       exact hz.symm
30     apply Element.ext
31     · exact add_comm _ _
32     · exact add_comm _ _
33     · simp [mul_central, hz, hr, add_comm]
34 
35 theorem mem_center_iff (h2 : (2 : K) ≠ 0) (a : Element K X) :
36     a ∈ Subgroup.center (Element K X) ↔ a.position = 0 ∧ a.frequency = 0 := by
37   constructor
38   · intro h
39     have hz : (a.position, a.frequency) = 0 :=
40       (HeisenbergCardinality.form_forall_eq_zero_iff _).mp (by
41         intro w
42         exact (commute_iff h2 a ⟨w.1, w.2, 0⟩).mp
43           ((Subgroup.mem_center_iff.mp h _).symm))
44     exact ⟨congrArg Prod.fst hz, congrArg Prod.snd hz⟩
45   · rintro ⟨hx, hξ⟩
46     apply Subgroup.mem_center_iff.mpr
47     intro b
48     apply (commute_iff h2 b a).mpr
49     simp [hx, hξ]
50 
51 theorem center_eq_centralElement (h2 : (2 : K) ≠ 0) (a : Element K X) :
52     a ∈ Subgroup.center (Element K X) ↔ a = centralElement a.central := by
53   rw [mem_center_iff h2]
54   constructor
55   · rintro ⟨hx, hξ⟩
56     apply Element.ext
57     · exact hx
58     · exact hξ
59     · rfl
60   · intro h
61     exact ⟨by simpa using congrArg Element.position h,
62       by simpa using congrArg Element.frequency h⟩
63 
64 end PaperXI.HeisenbergCenter

Back to source controls