DyadicAbstract.lean

1 import PaperXI.SymplecticCoordinates
2 import PaperXI.DyadicBasisConsequences
3 import PaperXI.DyadicBasisCounts
4 
5 /-! Intrinsic Arf invariants and dyadic formulas under only the abstract
6 finite-dimensional alternating nondegenerate hypotheses. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DyadicAbstract
10 open scoped BigOperators Classical
11 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
12 
13 variable {V : Type*} [AddCommGroup V] [Module F2 V] [FiniteDimensional F2 V]
14 
15 def coordinates (b : V →ₗ[F2] V →ₗ[F2] F2)
16     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
17     V ≃ₗ[F2] (Fin (Module.finrank F2 V / 2) → F2 × F2) :=
18   Classical.choose (PaperXI.SymplecticCoordinates.exists_half_coordinates b ha hn)
19 
20 theorem coordinates_form (b : V →ₗ[F2] V →ₗ[F2] F2)
21     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
22     ∀ x y, b x y = symplectic (coordinates b ha hn x) (coordinates b ha hn y) :=
23   Classical.choose_spec (PaperXI.SymplecticCoordinates.exists_half_coordinates b ha hn)
24 
25 def arf (b : V →ₗ[F2] V →ₗ[F2] F2)
26     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
27     (q : Refinement b) : F2 :=
28   PaperXI.DyadicBasis.basisArf (coordinates b ha hn) q
29 
30 /-- The intrinsic Arf value agrees with the source's paired-basis definition
31 for every symplectic coordinate map and every finite index type. -/
32 theorem arf_eq_basis {ι : Type*} [Fintype ι]
33     (b : V →ₗ[F2] V →ₗ[F2] F2)
34     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
35     (e : V ≃ₗ[F2] (ι → F2 × F2))
36     (he : ∀ x y, b x y = symplectic (e x) (e y)) (q : Refinement b) :
37     arf b ha hn q = PaperXI.DyadicBasis.basisArf e q :=
38   PaperXI.DyadicDimension.basisArf_independent (coordinates b ha hn) e
39     (coordinates_form b ha hn) he q
40 
41 /-- The literal finite Gauss sum; a finite enumeration is constructed from
42 the proved coordinate equivalence. -/
43 def gaussSum (b : V →ₗ[F2] V →ₗ[F2] F2)
44     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
45     (q : Refinement b) : ℤ :=
46   let : Fintype V := Fintype.ofEquiv
47     (Fin (Module.finrank F2 V / 2) → F2 × F2) (coordinates b ha hn).symm.toEquiv
48   ∑ x : V, sign (q.value x)
49 
50 theorem gaussSum_eq_sum [Fintype V] (b : V →ₗ[F2] V →ₗ[F2] F2)
51     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
52     (q : Refinement b) : gaussSum b ha hn q = ∑ x : V, sign (q.value x) := by
53   unfold gaussSum
54   rw [show Fintype.ofEquiv (Fin (Module.finrank F2 V / 2) → F2 × F2)
55     (coordinates b ha hn).symm.toEquiv = ‹Fintype V› from Subsingleton.elim _ _]
56 
57 /-- Paper XI 13.5, with no supplied coordinate hypothesis. -/
58 theorem gauss_sum (b : V →ₗ[F2] V →ₗ[F2] F2)
59     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
60     (q : Refinement b) :
61     gaussSum b ha hn q = sign (arf b ha hn q) * 2 ^ (Module.finrank F2 V / 2) := by
62   let : Fintype V := Fintype.ofEquiv
63     (Fin (Module.finrank F2 V / 2) → F2 × F2) (coordinates b ha hn).symm.toEquiv
64   rw [gaussSum_eq_sum]
65   simpa only [Fintype.card_fin, arf] using
66     PaperXI.DyadicBasis.gauss_sum (coordinates b ha hn) (coordinates_form b ha hn) q
67 
68 def normalizedGaussSign (b : V →ₗ[F2] V →ₗ[F2] F2)
69     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
70     (q : Refinement b) : ℚ :=
71   (gaussSum b ha hn q : ℚ) / (2 : ℚ) ^ (Module.finrank F2 V / 2)
72 
73 theorem normalizedGaussSign_eq_sign (b : V →ₗ[F2] V →ₗ[F2] F2)
74     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
75     (q : Refinement b) :
76     normalizedGaussSign b ha hn q = (sign (arf b ha hn q) : ℚ) := by
77   unfold normalizedGaussSign
78   rw [gauss_sum]
79   push_cast
80   exact mul_div_cancel_right₀ _ (pow_ne_zero _ (by norm_num : (2 : ℚ) ≠ 0))
81 
82 /-- Paper XI 13.8 for the actual refinement q + b(v,-). -/
83 theorem arf_translation (b : V →ₗ[F2] V →ₗ[F2] F2)
84     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
85     (q : Refinement b) (v : V) :
86     arf b ha hn (addLinear q (b v)) = arf b ha hn q + q.value v := by
87   exact PaperXI.DyadicBasisConsequences.arf_translation
88     (coordinates b ha hn) (coordinates_form b ha hn) q v
89 
90 /-- Paper XI 13.7: both Arf invariants and opposite normalized Gauss signs
91 occur for the same polar form on every nonzero symplectic space. -/
92 theorem opposite_refinements [Nontrivial V] (b : V →ₗ[F2] V →ₗ[F2] F2)
93     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
94     ∃ q r : Refinement b,
95       arf b ha hn q = 0 ∧ arf b ha hn r = 1 ∧
96       normalizedGaussSign b ha hn q = 1 ∧ normalizedGaussSign b ha hn r = -1 := by
97   let : Fintype V := Fintype.ofEquiv
98     (Fin (Module.finrank F2 V / 2) → F2 × F2) (coordinates b ha hn).symm.toEquiv
99   have hp : 0 < Module.finrank F2 V / 2 := by
100     simpa only [Fintype.card_fin] using
101       PaperXI.DyadicDimension.card_pos (coordinates b ha hn)
102   obtain ⟨q, r, hq, hr, _⟩ := PaperXI.DyadicBasisConsequences.opposite_refinements
103     (coordinates b ha hn) (coordinates_form b ha hn) ⟨0, hp⟩
104   have hq' : arf b ha hn q = 0 := hq
105   have hr' : arf b ha hn r = 1 := hr
106   refine ⟨q, r, hq', hr', ?_, ?_⟩
107   · rw [normalizedGaussSign_eq_sign, hq']
108     norm_num [sign]
109   · rw [normalizedGaussSign_eq_sign, hr']
110     norm_num [sign]
111 
112 /-- Paper XI 13.9, counting the complete even Arf fiber, including rank zero. -/
113 theorem even_count (b : V →ₗ[F2] V →ₗ[F2] F2)
114     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
115     (Nat.card {q : Refinement b // arf b ha hn q = 0} : ℚ) =
116       (2 : ℚ) ^ (((Module.finrank F2 V / 2 : ℕ) : ℤ) - 1) *
117         ((2 : ℚ) ^ (Module.finrank F2 V / 2) + 1) := by
118   have h := PaperXI.DyadicBasisCounts.even_count
119     (coordinates b ha hn) (coordinates_form b ha hn)
120   simpa [arf] using h
121 
122 /-- Paper XI 13.9, counting the complete odd Arf fiber, including rank zero. -/
123 theorem odd_count (b : V →ₗ[F2] V →ₗ[F2] F2)
124     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0) :
125     (Nat.card {q : Refinement b // arf b ha hn q = 1} : ℚ) =
126       (2 : ℚ) ^ (((Module.finrank F2 V / 2 : ℕ) : ℤ) - 1) *
127         ((2 : ℚ) ^ (Module.finrank F2 V / 2) - 1) := by
128   have h := PaperXI.DyadicBasisCounts.odd_count
129     (coordinates b ha hn) (coordinates_form b ha hn)
130   simpa [arf] using h
131 
132 /-- The displayed 13.5 formula with the paper's explicit dimension 2r. -/
133 theorem gauss_sum_of_finrank [Fintype V] (b : V →ₗ[F2] V →ₗ[F2] F2)
134     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
135     (q : Refinement b) (r : ℕ) (hdim : Module.finrank F2 V = 2 * r) :
136     (∑ x : V, sign (q.value x)) = sign (arf b ha hn q) * 2 ^ r := by
137   rw [← gaussSum_eq_sum b ha hn q, gauss_sum]
138   have hr : Module.finrank F2 V / 2 = r := by omega
139   rw [hr]
140 
141 /-- The displayed even-refinement count with the paper's dimension parameter. -/
142 theorem even_count_of_finrank (b : V →ₗ[F2] V →ₗ[F2] F2)
143     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
144     (r : ℕ) (hdim : Module.finrank F2 V = 2 * r) :
145     (Nat.card {q : Refinement b // arf b ha hn q = 0} : ℚ) =
146       (2 : ℚ) ^ ((r : ℤ) - 1) * ((2 : ℚ) ^ r + 1) := by
147   have hr : Module.finrank F2 V / 2 = r := by omega
148   simpa only [hr] using even_count b ha hn
149 
150 /-- The displayed odd-refinement count with the paper's dimension parameter. -/
151 theorem odd_count_of_finrank (b : V →ₗ[F2] V →ₗ[F2] F2)
152     (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
153     (r : ℕ) (hdim : Module.finrank F2 V = 2 * r) :
154     (Nat.card {q : Refinement b // arf b ha hn q = 1} : ℚ) =
155       (2 : ℚ) ^ ((r : ℤ) - 1) * ((2 : ℚ) ^ r - 1) := by
156   have hr : Module.finrank F2 V / 2 = r := by omega
157   simpa only [hr] using odd_count b ha hn
158 
159 end PaperXI.DyadicAbstract

Back to source controls