HyperbolicPhase.lean

1 import PaperXI.HyperbolicDeterminant
2 import PaperXI.OddPhase
3 
4 /-! Source 12.8 for the literal hyperbolic action. The calculation also holds
5 for the defined determinant phase in characteristic two; no Weil trace
6 interpretation or normalization is asserted here. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HyperbolicPhase
10 
11 variable {p : ℕ} [Fact p.Prime]
12 variable {U : Type*} [AddCommGroup U] [Module (ZMod p) U]
13 variable [FiniteDimensional (ZMod p) U]
14 
15 /-- The actual constructed hyperbolic action satisfies the phase-domain condition. -/
16 theorem fixedPointFree (a : U ≃ₗ[ZMod p] U) (ha : OddPhase.FixedPointFree a) :
17     OddPhase.FixedPointFree (HyperbolicSpace.action a) :=
18   HyperbolicSpace.action_fixedPointFree a ha
19 
20 /-- Source 12.8: the determinant phase of the actual hyperbolic action is the
21 quadratic character of the determinant on the original space. -/
22 theorem source (a : U ≃ₗ[ZMod p] U) (ha : OddPhase.FixedPointFree a) :
23     OddPhase.phase (HyperbolicSpace.action a) =
24       quadraticChar (ZMod p) (LinearMap.det a.toLinearMap) := by
25   have hd : LinearMap.det (a.toLinearMap - 1) ≠ 0 :=
26     (OddPhase.fixedPointFree_iff_det_ne_zero a).mp ha
27   have hdim : Module.finrank (ZMod p) (HyperbolicSpace.Space (ZMod p) U) / 2 =
28       Module.finrank (ZMod p) U := by
29     rw [HyperbolicSpace.finrank]
30     omega
31   rw [OddPhase.phase, hdim]
32   change quadraticChar (ZMod p) (-1) ^ Module.finrank (ZMod p) U *
33       quadraticChar (ZMod p) (LinearMap.det ((HyperbolicSpace.action a).toLinearMap - 1)) = _
34   rw [HyperbolicDeterminant.total_difference_det, map_mul, map_mul,
35     quadraticChar_sq_one' hd, map_pow, ← MulChar.inv_apply',
36     (quadraticChar_isQuadratic (ZMod p)).inv, mul_one]
37   have hsign : (quadraticChar (ZMod p) (-1) ^ Module.finrank (ZMod p) U) ^ 2 = 1 := by
38     rw [← pow_mul, Nat.mul_comm _ 2, pow_mul,
39       quadraticChar_sq_one (neg_ne_zero.mpr one_ne_zero), one_pow]
40   calc
41     _ = (quadraticChar (ZMod p) (-1) ^ Module.finrank (ZMod p) U) ^ 2 *
42         quadraticChar (ZMod p) (LinearMap.det a.toLinearMap) := by ring
43     _ = _ := by rw [hsign, one_mul]
44 
45 /-- All symplectic and fixed-point-free hypotheses are proved for the same
46 carrier and action appearing in the source phase formula. -/
47 theorem symplectic_fixedPointFree (a : U ≃ₗ[ZMod p] U) (ha : OddPhase.FixedPointFree a) :
48     (HyperbolicSpace.form (ZMod p) U).IsAlt ∧
49     (HyperbolicSpace.form (ZMod p) U).Nondegenerate ∧
50     (∀ x y, HyperbolicSpace.form (ZMod p) U (HyperbolicSpace.action a x)
51       (HyperbolicSpace.action a y) = HyperbolicSpace.form (ZMod p) U x y) ∧
52     OddPhase.FixedPointFree (HyperbolicSpace.action a) :=
53   ⟨HyperbolicSpace.form_isAlt (ZMod p) U, HyperbolicSpace.form_nondegenerate (ZMod p) U,
54     HyperbolicSpace.action_form a, fixedPointFree a ha⟩
55 
56 end PaperXI.HyperbolicPhase

Back to source controls