DyadicBasis.lean

1 import PaperXI.DyadicCoordinates
2 
3 /-! Transfer to arbitrary vector spaces with supplied symplectic coordinates.
4 The existence of those coordinates is explicitly separate. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.DyadicBasis
8 open scoped BigOperators Classical
9 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
10 
11 variable {V ι : Type*} [AddCommGroup V] [Module F2 V] [Fintype ι]
12 variable {b : V →ₗ[F2] V →ₗ[F2] F2}
13 
14 def toCoordinates (e : V ≃ₗ[F2] (ι → F2 × F2))
15     (hb : ∀ x y, b x y = symplectic (e x) (e y))
16     (q : Refinement b) : Refinement (symplectic (ι := ι)) where
17   value x := q.value (e.symm x)
18   polar x y := by
19     rw [map_add, q.polar, hb]
20     simp
21 
22 def fromCoordinates (e : V ≃ₗ[F2] (ι → F2 × F2))
23     (hb : ∀ x y, b x y = symplectic (e x) (e y))
24     (q : Refinement (symplectic (ι := ι))) : Refinement b where
25   value x := q.value (e x)
26   polar x y := by rw [map_add, q.polar, hb]
27 
28 /-- Every refinement transfers in both directions through supplied symplectic
29 coordinates. No formula for the refinement is assumed. -/
30 def refinementEquiv (e : V ≃ₗ[F2] (ι → F2 × F2))
31     (hb : ∀ x y, b x y = symplectic (e x) (e y)) :
32     Refinement b ≃ Refinement (symplectic (ι := ι)) where
33   toFun := toCoordinates e hb
34   invFun := fromCoordinates e hb
35   left_inv q := by
36     ext x
37     simp [toCoordinates, fromCoordinates]
38   right_inv q := by
39     ext x
40     simp [toCoordinates, fromCoordinates]
41 
42 @[simp] theorem toCoordinates_apply (e : V ≃ₗ[F2] (ι → F2 × F2))
43     (hb : ∀ x y, b x y = symplectic (e x) (e y))
44     (q : Refinement b) (x : ι → F2 × F2) :
45     (toCoordinates e hb q).value x = q.value (e.symm x) := rfl
46 
47 @[simp] theorem fromCoordinates_apply (e : V ≃ₗ[F2] (ι → F2 × F2))
48     (hb : ∀ x y, b x y = symplectic (e x) (e y))
49     (q : Refinement (symplectic (ι := ι))) (x : V) :
50     (fromCoordinates e hb q).value x = q.value (e x) := rfl
51 
52 /-- Arf's basis-value formula on the transported paired basis. -/
53 def basisArf (e : V ≃ₗ[F2] (ι → F2 × F2)) (q : Refinement b) : F2 :=
54   ∑ i, q.value (e.symm (firstAxis i)) * q.value (e.symm (secondAxis i))
55 
56 theorem basisArf_eq_coordinate_arf (e : V ≃ₗ[F2] (ι → F2 × F2))
57     (hb : ∀ x y, b x y = symplectic (e x) (e y)) (q : Refinement b) :
58     basisArf e q = arf (refinementCoefficients (toCoordinates e hb q)) := by
59   rw [refinement_arf_basis_formula]
60   rfl
61 
62 theorem gauss_sum [Fintype V] (e : V ≃ₗ[F2] (ι → F2 × F2))
63     (hb : ∀ x y, b x y = symplectic (e x) (e y)) (q : Refinement b) :
64     (∑ x : V, sign (q.value x)) = sign (basisArf e q) * 2 ^ Fintype.card ι := by
65   calc
66     (∑ x : V, sign (q.value x)) =
67         ∑ x : ι → F2 × F2, sign (q.value (e.symm x)) :=
68       (e.symm.toEquiv.sum_comp (fun x => sign (q.value x))).symm
69     _ = sign (basisArf e q) * 2 ^ Fintype.card ι :=
70       refinement_gauss_sum (toCoordinates e hb q)
71 
72 /-- Changing a supplied symplectic coordinate map leaves the Arf value
73 unchanged, because both maps evaluate the same intrinsic Gauss sum. -/
74 theorem basisArf_independent [Fintype V]
75     (e f : V ≃ₗ[F2] (ι → F2 × F2))
76     (he : ∀ x y, b x y = symplectic (e x) (e y))
77     (hf : ∀ x y, b x y = symplectic (f x) (f y)) (q : Refinement b) :
78     basisArf e q = basisArf f q := by
79   apply sign_injective
80   have h := (gauss_sum e he q).symm.trans (gauss_sum f hf q)
81   exact mul_right_cancel₀ (pow_ne_zero _ (by norm_num : (2 : ℤ) ≠ 0)) h
82 
83 end PaperXI.DyadicBasis

Back to source controls