SymplecticSplit.lean

1 import PaperXI.DyadicGauss
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 import Mathlib.LinearAlgebra.Dimension.Constructions
4 import Mathlib.Algebra.CharP.Two
5 
6 /-! A constructive hyperbolic-plane splitting of a nondegenerate alternating
7 form over F₂. The complement and both directions of the coordinate map are
8 built explicitly from one hyperbolic pair. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.SymplecticSplit
12 open PaperXI.Dyadic
13 
14 variable {V : Type*} [AddCommGroup V] [Module F2 V]
15 
16 /-- In characteristic two, an alternating bilinear form is symmetric. -/
17 theorem alternating_symmetric (b : V →ₗ[F2] V →ₗ[F2] F2)
18     (ha : ∀ x, b x x = 0) (x y : V) : b x y = b y x := by
19   have h := ha (x + y)
20   simp only [map_add, LinearMap.add_apply, ha, zero_add, add_zero] at h
21   exact ((eq_neg_of_add_eq_zero_left h).trans (CharTwo.neg_eq _)).symm
22 
23 /-- Every nonzero nondegenerate alternating space contains a hyperbolic pair. -/
24 theorem exists_pair [Nontrivial V] (b : V →ₗ[F2] V →ₗ[F2] F2)
25     (hn : ∀ x, (∀ y, b x y = 0) → x = 0) : ∃ u v, b u v = 1 := by
26   obtain ⟨u, hu⟩ := exists_ne (0 : V)
27   have h : ∃ v, b u v ≠ 0 := by
28     by_contra! h
29     exact hu (hn u h)
30   obtain ⟨v, hv⟩ := h
31   refine ⟨u, (b u v)⁻¹ • v, ?_⟩
32   simp [hv]
33 
34 /-- A hyperbolic pair supplies an actual product decomposition. -/
35 theorem split_of_pair [FiniteDimensional F2 V]
36     (b : V →ₗ[F2] V →ₗ[F2] F2) (ha : ∀ x, b x x = 0)
37     (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
38     (u v : V) (huv : b u v = 1) :
39     ∃ W : Submodule F2 V, ∃ e : V ≃ₗ[F2] ((F2 × F2) × W),
40       (∀ x y, b x y = (e x).1.1 * (e y).1.2 +
41         (e x).1.2 * (e y).1.1 +
42         (b.compl₁₂ W.subtype W.subtype) (e x).2 (e y).2) ∧
43       (∀ w, (b.compl₁₂ W.subtype W.subtype) w w = 0) ∧
44       (∀ w, (∀ z, (b.compl₁₂ W.subtype W.subtype) w z = 0) → w = 0) ∧
45       Module.finrank F2 W < Module.finrank F2 V := by
46   have hvu : b v u = 1 := (alternating_symmetric b ha v u).trans huv
47   let W : Submodule F2 V := (b u).ker ⊓ (b v).ker
48   let r : V →ₗ[F2] V := LinearMap.id - (b v).smulRight u - (b u).smulRight v
49   have hr (x : V) : r x = x - (b v x) • u - (b u x) • v := rfl
50   have hr_mem (x : V) : r x ∈ W := by
51     change b u (r x) = 0 ∧ b v (r x) = 0
52     simp [hr, huv, hvu, ha]
53   have huW (w : W) : b u w = 0 := w.property.1
54   have hvW (w : W) : b v w = 0 := w.property.2
55   have hWu (w : W) : b w u = 0 := (alternating_symmetric b ha w u).trans (huW w)
56   have hWv (w : W) : b w v = 0 := (alternating_symmetric b ha w v).trans (hvW w)
57   let e : V ≃ₗ[F2] ((F2 × F2) × W) :=
58     { toFun := fun x => ((b v x, b u x), ⟨r x, hr_mem x⟩)
59       invFun := fun z => z.1.1 • u + z.1.2 • v + z.2
60       left_inv := by
61         intro x
62         dsimp
63         rw [hr]
64         abel
65       right_inv := by
66         rintro ⟨⟨a, d⟩, w⟩
67         apply Prod.ext
68         · apply Prod.ext <;> simp [ha, huv, hvu, huW, hvW]
69         · apply Subtype.ext
70           dsimp
71           rw [hr]
72           simp [ha, huv, hvu, huW, hvW]
73           abel
74       map_add' := by
75         intro x y
76         apply Prod.ext
77         · simp
78         · apply Subtype.ext
79           exact r.map_add x y
80       map_smul' := by
81         intro a x
82         apply Prod.ext
83         · simp
84         · apply Subtype.ext
85           exact r.map_smul a x }
86   have hinv (z : (F2 × F2) × W) : e.symm z = z.1.1 • u + z.1.2 • v + z.2 := rfl
87   have hform (x y : V) : b x y = (e x).1.1 * (e y).1.2 +
88         (e x).1.2 * (e y).1.1 +
89         (b.compl₁₂ W.subtype W.subtype) (e x).2 (e y).2 := by
90     obtain ⟨s, rfl⟩ := e.symm.surjective x
91     obtain ⟨t, rfl⟩ := e.symm.surjective y
92     simp only [LinearEquiv.apply_symm_apply]
93     rw [hinv, hinv]
94     simp [map_add, map_smul, ha, huv, hvu, huW, hvW, hWu, hWv,
95       LinearMap.compl₁₂_apply]
96     ring
97   refine ⟨W, e, hform, ?_, ?_, ?_⟩
98   · intro w
99     exact ha w
100   · intro w hw
101     apply Subtype.ext
102     apply hn w
103     intro y
104     obtain ⟨z, rfl⟩ := e.symm.surjective y
105     rw [hinv]
106     simpa [hWu, hWv] using hw z.2
107   · have hd := e.finrank_eq
108     rw [Module.finrank_prod, Module.finrank_prod, Module.finrank_self] at hd
109     omega
110 
111 /-- A nontrivial nondegenerate alternating F₂-space splits as one hyperbolic
112 plane and a strictly smaller nondegenerate alternating space. -/
113 theorem exists_split [FiniteDimensional F2 V] [Nontrivial V]
114     (b : V →ₗ[F2] V →ₗ[F2] F2) (ha : ∀ x, b x x = 0)
115     (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
116     ∃ W : Submodule F2 V, ∃ e : V ≃ₗ[F2] ((F2 × F2) × W),
117       (∀ x y, b x y = (e x).1.1 * (e y).1.2 +
118         (e x).1.2 * (e y).1.1 +
119         (b.compl₁₂ W.subtype W.subtype) (e x).2 (e y).2) ∧
120       (∀ w, (b.compl₁₂ W.subtype W.subtype) w w = 0) ∧
121       (∀ w, (∀ z, (b.compl₁₂ W.subtype W.subtype) w z = 0) → w = 0) ∧
122       Module.finrank F2 W < Module.finrank F2 V := by
123   obtain ⟨u, v, huv⟩ := exists_pair b hn
124   exact split_of_pair b ha hn u v huv
125 
126 end PaperXI.SymplecticSplit

Back to source controls