OddEnvelopeHeisenberg.lean

1 import PaperXI.BilinearHeisenberg
2 import PaperXI.HeisenbergPrime
3 
4 /-! Canonical odd-characteristic extension, constructed directly on the given
5 alternating space. No polarization, symplectic basis or pre-existing group is input. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.OddEnvelopeHeisenberg
9 open BilinearHeisenberg
10 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
11 
12 /-- The half-form factor set is available without choosing coordinates. -/
13 def factor (b : LinearMap.BilinForm K V) : LinearMap.BilinForm K V := (2 : K)⁻¹ • b
14 
15 @[simp] theorem factor_apply (b : LinearMap.BilinForm K V) (x y : V) :
16     factor b x y = (2 : K)⁻¹ * b x y := rfl
17 
18 /-- Alternation and invertibility of two give the required commutator exactly. -/
19 theorem factor_commutator (b : LinearMap.BilinForm K V)
20     (ha : b.IsAlt) (h2 : (2 : K) ≠ 0) (x y : V) :
21     factor b x y - factor b y x = b x y := by
22   have hskew : b x y + b y x = 0 := by
23     have h := ha (x + y)
24     simpa only [map_add, LinearMap.add_apply, ha x, ha y, zero_add, add_zero, add_comm] using h
25   simp only [factor_apply]
26   have hi : (2 : K)⁻¹ * 2 = 1 := inv_mul_cancel₀ h2
27   calc
28     (2 : K)⁻¹ * b x y - (2 : K)⁻¹ * b y x =
29         ((2 : K)⁻¹ * 2) * b x y := by linear_combination -(2 : K)⁻¹ * hskew
30     _ = _ := by rw [hi, one_mul]
31 
32 /-- Every isometry lifts by the literal formula (v,z) -> (e(v),z). -/
33 def isometryEquiv {V' : Type*} [AddCommGroup V'] [Module K V']
34     (b : LinearMap.BilinForm K V) (b' : LinearMap.BilinForm K V')
35     (e : V ≃ₗ[K] V') (he : ∀ x y, b' (e x) (e y) = b x y) :
36     Element (factor b) ≃* Element (factor b') where
37   toFun h := ⟨e h.vector, h.central⟩
38   invFun h := ⟨e.symm h.vector, h.central⟩
39   left_inv h := by ext <;> simp
40   right_inv h := by ext <;> simp
41   map_mul' h k := by
42     ext
43     · exact e.map_add _ _
44     · simp only [mul_central, factor_apply, he]
45 
46 @[simp] theorem isometryEquiv_center {V' : Type*} [AddCommGroup V'] [Module K V']
47     (b : LinearMap.BilinForm K V) (b' : LinearMap.BilinForm K V')
48     (e : V ≃ₗ[K] V') (he : ∀ x y, b' (e x) (e y) = b x y) (z : Multiplicative K) :
49     isometryEquiv b b' e he (i (factor b) z) = i (factor b') z := by
50   ext <;> simp [isometryEquiv]
51 
52 end PaperXI.OddEnvelopeHeisenberg

Back to source controls