OddPhaseCertificate.lean

1 import PaperXI.OddPhase
2 import PaperXI.OddSymplectic
3 
4 /-! The actual characteristic-polynomial certificate for the determinant phase.
5 The source specialization derives even dimension from the supplied form. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.OddPhase
9 
10 variable {p : ℕ} [Fact p.Prime]
11 variable {V : Type*} [AddCommGroup V] [Module (ZMod p) V]
12 variable [FiniteDimensional (ZMod p) V]
13 
14 /-- The actual characteristic polynomial at one is the determinant of the
15 negative difference. No parity hypothesis is needed for this identity. -/
16 theorem charpoly_eval_one (g : V ≃ₗ[ZMod p] V) :
17     g.toLinearMap.charpoly.eval 1 = LinearMap.det (-difference g) := by
18   rw [LinearMap.eval_charpoly]
19   congr 1
20   ext v
21   simp [difference, sub_eq_add_neg]
22 
23 /-- In even dimension the two difference conventions have the same determinant. -/
24 theorem determinant_neg_difference (g : V ≃ₗ[ZMod p] V)
25     (heven : Even (Module.finrank (ZMod p) V)) :
26     LinearMap.det (-difference g) = LinearMap.det (difference g) := by
27   rw [← neg_one_smul (ZMod p) (difference g), LinearMap.det_smul,
28     heven.neg_one_pow, one_mul]
29 
30 theorem characteristic_determinant (g : V ≃ₗ[ZMod p] V)
31     (heven : Even (Module.finrank (ZMod p) V)) :
32     g.toLinearMap.charpoly.eval 1 = LinearMap.det (difference g) := by
33   rw [charpoly_eval_one, determinant_neg_difference g heven]
34 
35 /-- The phase certificate for a supplied even-dimensional space. -/
36 theorem characteristic_certificate_of_even (g : V ≃ₗ[ZMod p] V)
37     (heven : Even (Module.finrank (ZMod p) V)) :
38     phase g = quadraticChar (ZMod p) (-1) ^ (Module.finrank (ZMod p) V / 2) *
39       quadraticChar (ZMod p) (g.toLinearMap.charpoly.eval 1) := by
40   rw [characteristic_determinant g heven]
41   rfl
42 
43 /-- Source 12.5: the actual nondegenerate alternating form in odd
44 characteristic supplies the parity needed for the characteristic certificate.
45 The formula also remains valid when the action has fixed vectors. -/
46 theorem characteristic_certificate (hp : p ≠ 2)
47     (b : LinearMap.BilinForm (ZMod p) V) (hb : b.IsAlt) (hbn : b.Nondegenerate)
48     (g : V ≃ₗ[ZMod p] V) :
49     phase g = quadraticChar (ZMod p) (-1) ^ (Module.finrank (ZMod p) V / 2) *
50       quadraticChar (ZMod p) (g.toLinearMap.charpoly.eval 1) :=
51   characteristic_certificate_of_even g (OddSymplectic.even_finrank_zmod hp b hb hbn)
52 
53 /-- Fixed-point-free source data make the characteristic-polynomial value at
54 one nonzero; it is the actual determinant used in the phase. -/
55 theorem characteristic_eval_one_ne_zero (hp : p ≠ 2)
56     (b : LinearMap.BilinForm (ZMod p) V) (hb : b.IsAlt) (hbn : b.Nondegenerate)
57     (g : V ≃ₗ[ZMod p] V) (hg : FixedPointFree g) : g.toLinearMap.charpoly.eval 1 ≠ 0 := by
58   rw [characteristic_determinant g (OddSymplectic.even_finrank_zmod hp b hb hbn)]
59   exact (fixedPointFree_iff_det_ne_zero g).mp hg
60 
61 end PaperXI.OddPhase

Back to source controls