SymplecticCoordinates.lean

1 import PaperXI.SymplecticSplit
2 import PaperXI.SymplecticAssembly
3 import PaperXI.DyadicDimension
4 
5 /-! Symplectic coordinates constructed from alternation and nondegeneracy,
6 by strong induction on the dimension. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.SymplecticCoordinates
10 open scoped BigOperators Classical
11 open PaperXI.Dyadic PaperXI.DyadicCoordinates
12 
13 variable {V : Type*} [AddCommGroup V] [Module F2 V] [FiniteDimensional F2 V]
14 
15 /-- Every finite-dimensional alternating left-nondegenerate F2-form admits
16 actual form-preserving coordinates in finitely many hyperbolic planes. -/
17 theorem exists_coordinates (b : V →ₗ[F2] V →ₗ[F2] F2)
18     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
19     ∃ r : ℕ, ∃ e : V ≃ₗ[F2] (Fin r → F2 × F2),
20       ∀ x y, b x y = symplectic (e x) (e y) := by
21   suffices ∀ n, Module.finrank F2 V = n →
22       ∃ r : ℕ, ∃ e : V ≃ₗ[F2] (Fin r → F2 × F2),
23         ∀ x y, b x y = symplectic (e x) (e y) by
24     exact this _ rfl
25   intro n hdim
26   induction n using Nat.strong_induction_on generalizing V with
27   | h n ih =>
28     by_cases hz : n = 0
29     · have hzero : Module.finrank F2 V = 0 := hdim.trans hz
30       let : Subsingleton V := (Module.finrank_zero_iff (R := F2) (M := V)).mp hzero
31       refine ⟨0, LinearEquiv.ofSubsingleton (R := F2) V (Fin 0 → F2 × F2), ?_⟩
32       intro x y
33       have hx : x = 0 := Subsingleton.elim _ _
34       simp [hx, symplectic_apply]
35     · let : Nontrivial V := (Module.finrank_pos_iff (R := F2) (M := V)).mp (by omega)
36       obtain ⟨W, e, he, haW, hnW, hW⟩ :=
37         PaperXI.SymplecticSplit.exists_split b ha hn
38       obtain ⟨r, f, hf⟩ := ih (Module.finrank F2 W) (by omega)
39         (b.compl₁₂ W.subtype W.subtype) haW hnW rfl
40       refine ⟨r + 1, PaperXI.SymplecticAssembly.assemble r e f, ?_⟩
41       exact PaperXI.SymplecticAssembly.assemble_form r b
42         (b.compl₁₂ W.subtype W.subtype) e f he hf
43 
44 /-- The chosen coordinate count is exactly half the dimension. -/
45 theorem exists_coordinates_dimension (b : V →ₗ[F2] V →ₗ[F2] F2)
46     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
47     ∃ r : ℕ, ∃ e : V ≃ₗ[F2] (Fin r → F2 × F2),
48       (∀ x y, b x y = symplectic (e x) (e y)) ∧
49       Module.finrank F2 V = 2 * r := by
50   obtain ⟨r, e, he⟩ := exists_coordinates b ha hn
51   refine ⟨r, e, he, ?_⟩
52   simpa using PaperXI.DyadicDimension.finrank_eq_twice_card e
53 
54 theorem even_finrank (b : V →ₗ[F2] V →ₗ[F2] F2)
55     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
56     Even (Module.finrank F2 V) := by
57   obtain ⟨r, _, _, hr⟩ := exists_coordinates_dimension b ha hn
58   exact ⟨r, by omega⟩
59 
60 /-- Coordinates with the canonical half-dimension index. -/
61 theorem exists_half_coordinates (b : V →ₗ[F2] V →ₗ[F2] F2)
62     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
63     ∃ e : V ≃ₗ[F2] (Fin (Module.finrank F2 V / 2) → F2 × F2),
64       ∀ x y, b x y = symplectic (e x) (e y) := by
65   obtain ⟨r, e, he, hr⟩ := exists_coordinates_dimension b ha hn
66   have h : r = Module.finrank F2 V / 2 := by omega
67   subst r
68   exact ⟨e, he⟩
69 
70 end PaperXI.SymplecticCoordinates

Back to source controls