OddSymplectic.lean

1 import Mathlib.LinearAlgebra.Matrix.BilinearForm
2 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
3 import Mathlib.Algebra.Ring.Parity
4 import Mathlib.Algebra.Field.ZMod
5 
6 /-! Even dimension of the actual alternating nondegenerate form in odd
7 characteristic. The determinant argument uses its matrix in a constructed
8 finite basis and does not assume symplectic coordinates or evenness. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.OddSymplectic
12 
13 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
14 variable [FiniteDimensional K V]
15 
16 /-- The actual form matrix is skew under transposition. -/
17 theorem transpose_toMatrix (b : LinearMap.BilinForm K V) (ha : b.IsAlt) :
18     (LinearMap.BilinForm.toMatrix (Module.finBasis K V) b).transpose =
19       -LinearMap.BilinForm.toMatrix (Module.finBasis K V) b := by
20   ext i j
21   simpa only [Matrix.transpose_apply, Matrix.neg_apply, LinearMap.BilinForm.toMatrix_apply]
22     using (ha.neg_eq (Module.finBasis K V i) (Module.finBasis K V j)).symm
23 
24 /-- A finite-dimensional nondegenerate alternating form over a field of
25 characteristic different from two has even dimension. -/
26 theorem even_finrank (b : LinearMap.BilinForm K V) (ha : b.IsAlt)
27     (hn : b.Nondegenerate) (h2 : (2 : K) ≠ 0) : Even (Module.finrank K V) := by
28   let M := LinearMap.BilinForm.toMatrix (Module.finBasis K V) b
29   have hd0 : M.det ≠ 0 :=
30     (LinearMap.BilinForm.nondegenerate_iff_det_ne_zero (Module.finBasis K V)).mp hn
31   have hd := congrArg Matrix.det (transpose_toMatrix b ha)
32   change M.transpose.det = (-M).det at hd
33   rw [Matrix.det_transpose, Matrix.det_neg, Fintype.card_fin] at hd
34   have hp : (-1 : K) ^ Module.finrank K V = 1 := by
35     apply mul_right_cancel₀ hd0
36     simpa only [one_mul] using hd.symm
37   apply (neg_one_pow_eq_one_iff_even ?_).mp hp
38   intro h
39   apply h2
40   have hh := congrArg (fun x : K => x + 1) h
41   simpa only [neg_add_cancel, ← one_add_one_eq_two] using hh.symm
42 
43 /-- The half-dimension is an exact integer, proved from the form hypotheses. -/
44 theorem finrank_eq_two_mul_half (b : LinearMap.BilinForm K V) (ha : b.IsAlt)
45     (hn : b.Nondegenerate) (h2 : (2 : K) ≠ 0) :
46     Module.finrank K V = 2 * (Module.finrank K V / 2) := by
47   obtain ⟨n, hn⟩ := even_finrank b ha hn h2
48   omega
49 
50 /-- The odd-prime source hypothesis gives the needed nonzero scalar two. -/
51 theorem two_ne_zero {p : ℕ} [Fact p.Prime] (hp : p ≠ 2) : (2 : ZMod p) ≠ 0 := by
52   intro h
53   have hd : p ∣ 2 := (ZMod.natCast_eq_zero_iff 2 p).mp h
54   rcases (Nat.dvd_prime Nat.prime_two).mp hd with h1 | htwo
55   · exact (Nat.Prime.ne_one (Fact.out : p.Prime)) h1
56   · exact hp htwo
57 
58 /-- Source specialization with actual odd-prime and symplectic-form hypotheses. -/
59 theorem even_finrank_zmod {p : ℕ} [Fact p.Prime] (hp : p ≠ 2)
60     {W : Type*} [AddCommGroup W] [Module (ZMod p) W] [FiniteDimensional (ZMod p) W]
61     (b : LinearMap.BilinForm (ZMod p) W) (ha : b.IsAlt) (hn : b.Nondegenerate) :
62     Even (Module.finrank (ZMod p) W) := even_finrank b ha hn (two_ne_zero hp)
63 
64 theorem finrank_eq_two_mul_half_zmod {p : ℕ} [Fact p.Prime] (hp : p ≠ 2)
65     {W : Type*} [AddCommGroup W] [Module (ZMod p) W] [FiniteDimensional (ZMod p) W]
66     (b : LinearMap.BilinForm (ZMod p) W) (ha : b.IsAlt) (hn : b.Nondegenerate) :
67     Module.finrank (ZMod p) W = 2 * (Module.finrank (ZMod p) W / 2) :=
68   finrank_eq_two_mul_half b ha hn (two_ne_zero hp)
69 
70 end PaperXI.OddSymplectic

Back to source controls