HeisenbergForm.lean

1 import Mathlib.LinearAlgebra.Dual.Defs
2 import Mathlib.LinearAlgebra.BilinearMap
3 import Mathlib.LinearAlgebra.Prod
4 import Mathlib.Tactic.Ring
5 
6 /-! The manuscript's standard alternating form on X plus its linear dual. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HeisenbergForm
10 
11 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
12 
13 def form : (X × Module.Dual K X) →ₗ[K] (X × Module.Dual K X) →ₗ[K] K where
14   toFun v :=
15     { toFun := fun w => w.2 v.1 - v.2 w.1
16       map_add' := by
17         intro w t
18         simp only [Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add]
19         ring
20       map_smul' := by
21         intro a w
22         change (a • w.2) v.1 - v.2 (a • w.1) = a • (w.2 v.1 - v.2 w.1)
23         simp only [LinearMap.smul_apply, map_smul, smul_eq_mul]
24         ring }
25   map_add' := by
26     intro v w
27     apply LinearMap.ext
28     intro t
29     change t.2 (v + w).1 - (v + w).2 t.1 =
30       (t.2 v.1 - v.2 t.1) + (t.2 w.1 - w.2 t.1)
31     simp only [Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add]
32     ring
33   map_smul' := by
34     intro a v
35     apply LinearMap.ext
36     intro w
37     change w.2 (a • v.1) - (a • v.2) w.1 = a • (w.2 v.1 - v.2 w.1)
38     simp only [LinearMap.smul_apply, map_smul, smul_eq_mul]
39     ring
40 
41 @[simp] theorem form_apply (v w : X × Module.Dual K X) :
42     form v w = w.2 v.1 - v.2 w.1 := rfl
43 
44 theorem form_self (v : X × Module.Dual K X) : form v v = 0 := by
45   simp
46 
47 theorem form_skew (v w : X × Module.Dual K X) : form v w = -form w v := by
48   simp
49 
50 end PaperXI.HeisenbergForm

Back to source controls