HeisenbergCochain.lean

1 import PaperXI.BilinearHeisenberg
2 import Mathlib.Algebra.CharP.Two
3 
4 /-! Actual changes of central section and the square obstruction in characteristic
5 two. These statements concern the middle groups, not just their commutator forms. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.HeisenbergCochain
9 open BilinearHeisenberg
10 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
11 variable (c d : LinearMap.BilinForm K V)
12 
13 /-- A normalized coboundary constructs a genuine central-extension isomorphism. -/
14 def equiv (f : V → K) (_h0 : f 0 = 0)
15     (hf : ∀ x y, d x y - c x y = f (x + y) - f x - f y) :
16     Element c ≃* Element d where
17   toFun h := ⟨h.vector, h.central + f h.vector⟩
18   invFun h := ⟨h.vector, h.central - f h.vector⟩
19   left_inv h := by ext <;> simp
20   right_inv h := by ext <;> simp
21   map_mul' h k := by
22     ext
23     · rfl
24     · change h.central + k.central + c h.vector k.vector + f (h.vector + k.vector) =
25         (h.central + f h.vector) + (k.central + f k.vector) + d h.vector k.vector
26       linear_combination -(hf h.vector k.vector)
27 
28 @[simp] theorem equiv_center (f : V → K) (h0 : f 0 = 0)
29     (hf : ∀ x y, d x y - c x y = f (x + y) - f x - f y) (z : Multiplicative K) :
30     equiv c d f h0 hf (i c z) = i d z := by
31   ext <;> simp [equiv, h0]
32 
33 @[simp] theorem equiv_vector (f : V → K) (h0 : f 0 = 0)
34     (hf : ∀ x y, d x y - c x y = f (x + y) - f x - f y) (h : Element c) :
35     (equiv c d f h0 hf h).vector = h.vector := rfl
36 
37 section CharacteristicTwo
38 variable [CharP K 2]
39 
40 /-- All lifts of a quotient vector have the same square, calculated from c. -/
41 theorem square (h : Element c) :
42     h * h = i c (Multiplicative.ofAdd (c h.vector h.vector)) := by
43   ext
44   · change h.vector + h.vector = 0
45     rw [← two_smul K, show (2 : K) = 0 from CharP.cast_eq_zero K 2, zero_smul]
46   · change h.central + h.central + c h.vector h.vector = c h.vector h.vector
47     rw [CharTwo.add_self_eq_zero, zero_add]
48 
49 /-- A center- and quotient-preserving isomorphism must preserve the diagonal
50 factor set. Thus the alternating commutator alone does not determine the extension. -/
51 theorem diagonal_preserved (e : Element c ≃* Element d)
52     (he : ∀ z, e (i c z) = i d z)
53     (hq : ∀ h, (e h).vector = h.vector) (v : V) : c v v = d v v := by
54   let h : Element c := ⟨v, 0⟩
55   have hm := e.map_mul h h
56   rw [square, he, square] at hm
57   have hv := congrArg Element.central hm
58   change c h.vector h.vector = d (e h).vector (e h).vector at hv
59   rw [hq] at hv
60   exact hv
61 
62 theorem no_equiv_of_diagonal_mismatch (v : V) (hv : c v v ≠ d v v) :
63     ¬ ∃ e : Element c ≃* Element d,
64       (∀ z, e (i c z) = i d z) ∧ (∀ h, (e h).vector = h.vector) := by
65   rintro ⟨e, he, hq⟩
66   exact hv (diagonal_preserved c d e he hq v)
67 
68 end CharacteristicTwo
69 end PaperXI.HeisenbergCochain

Back to source controls