BreakDyadicPhase.lean

1 import PaperXI.BreakQuadratic
2 
3 /-! Paper XI 15.3, characteristic two: finite-family products of actual
4 normalized Gauss sums, and transfer through the supplied quadratic decomposition. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.BreakDyadicPhase
8 open scoped BigOperators Classical
9 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.BreakQuadratic
10 
11 variable {ι : Type*} [Fintype ι] {V : ι → Type*}
12   [∀ i, AddCommGroup (V i)] [∀ i, Module F2 (V i)]
13   [∀ i, FiniteDimensional F2 (V i)]
14 variable (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
15   (ha : ∀ i x, b i x x = 0)
16   (hn : ∀ i x, (∀ y, b i x y = 0) → x = 0)
17 
18 /-- The intrinsic Gauss sums use the same literal finite product sum,
19 independently of the internally chosen finite enumerations. -/
20 theorem gaussSum_product (q : ∀ i, Refinement (b i)) :
21     DyadicAbstract.gaussSum (form b) (form_alternating b ha)
22       (form_nondegenerate b hn) (refinement b q) =
23       ∏ i, DyadicAbstract.gaussSum (b i) (ha i) (hn i) (q i) := by
24   let (i : ι) : Fintype (V i) := Fintype.ofEquiv _
25     (DyadicAbstract.coordinates (b i) (ha i) (hn i)).symm.toEquiv
26   simp_rw [DyadicAbstract.gaussSum_eq_sum]
27   exact gauss_sum_product b q
28 
29 /-- Source 15.3: the normalized Gauss sign of the actual finite orthogonal
30 refinement is the product of the component normalized Gauss signs. -/
31 theorem normalizedGaussSign_product (q : ∀ i, Refinement (b i)) :
32     DyadicAbstract.normalizedGaussSign (form b) (form_alternating b ha)
33       (form_nondegenerate b hn) (refinement b q) =
34       ∏ i, DyadicAbstract.normalizedGaussSign (b i) (ha i) (hn i) (q i) := by
35   simp only [DyadicAbstract.normalizedGaussSign]
36   rw [half_finrank_product b ha hn, gaussSum_product b ha hn]
37   push_cast
38   rw [Finset.prod_div_distrib, Finset.prod_pow_eq_pow_sum]
39 
40 /-- The corresponding intrinsic Arf invariant is additive over the actual
41 finite orthogonal family. -/
42 theorem arf_sum (q : ∀ i, Refinement (b i)) :
43     DyadicAbstract.arf (form b) (form_alternating b ha)
44       (form_nondegenerate b hn) (refinement b q) =
45       ∑ i, DyadicAbstract.arf (b i) (ha i) (hn i) (q i) := by
46   apply sign_injective
47   have h := normalizedGaussSign_product b ha hn q
48   simp_rw [DyadicAbstract.normalizedGaussSign_eq_sign] at h
49   rw [sign_sum]
50   exact_mod_cast h
51 
52 /-- The empty family contributes the multiplicative unit. -/
53 theorem normalizedGaussSign_empty [IsEmpty ι] (q : ∀ i, Refinement (b i)) :
54     DyadicAbstract.normalizedGaussSign (form b) (form_alternating b ha)
55       (form_nondegenerate b hn) (refinement b q) = 1 := by
56   rw [normalizedGaussSign_product b ha hn]
57   simp
58 
59 variable {X : Type*} [AddCommGroup X] [Module F2 X] [FiniteDimensional F2 X]
60 variable (d : X →ₗ[F2] X →ₗ[F2] F2)
61   (hd : ∀ x, d x x = 0) (hk : ∀ x, (∀ y, d x y = 0) → x = 0)
62 
63 omit [∀ i, FiniteDimensional F2 (V i)] [FiniteDimensional F2 X] in
64 /-- Exact refinement compatibility is the value equation on the supplied
65 decomposition; preserving only the polar form is insufficient. -/
66 theorem transport_refinement (f : X ≃ₗ[F2] (∀ i, V i))
67     (hf : ∀ x y, d x y = form b (f x) (f y))
68     (q : Refinement d) (qs : ∀ i, Refinement (b i))
69     (hq : ∀ x, q.value x = ∑ i, (qs i).value (f x i)) :
70     DyadicIsometry.transportRefinement f hf q = refinement b qs := by
71   ext x
72   rw [DyadicIsometry.transportRefinement_apply, hq]
73   simp only [LinearEquiv.apply_symm_apply, refinement_apply]
74 
75 /-- Finite-family Arf additivity after an actual form- and refinement-preserving
76 break decomposition. -/
77 theorem arf_of_decomposition (f : X ≃ₗ[F2] (∀ i, V i))
78     (hf : ∀ x y, d x y = form b (f x) (f y))
79     (q : Refinement d) (qs : ∀ i, Refinement (b i))
80     (hq : ∀ x, q.value x = ∑ i, (qs i).value (f x i)) :
81     DyadicAbstract.arf d hd hk q =
82       ∑ i, DyadicAbstract.arf (b i) (ha i) (hn i) (qs i) := by
83   calc
84     DyadicAbstract.arf d hd hk q =
85         DyadicAbstract.arf (form b) (form_alternating b ha) (form_nondegenerate b hn)
86           (DyadicIsometry.transportRefinement f hf q) :=
87       (DyadicAbstractOrthogonal.arf_transport d (form b) hd hk
88         (form_alternating b ha) (form_nondegenerate b hn) f hf q).symm
89     _ = _ := by
90       rw [transport_refinement b d f hf q qs hq]
91       exact arf_sum b ha hn qs
92 
93 /-- Source 15.3 for supplied finite break data: the actual normalized total
94 Gauss sum factors into the actual normalized summand Gauss sums. -/
95 theorem normalizedGaussSign_of_decomposition (f : X ≃ₗ[F2] (∀ i, V i))
96     (hf : ∀ x y, d x y = form b (f x) (f y))
97     (q : Refinement d) (qs : ∀ i, Refinement (b i))
98     (hq : ∀ x, q.value x = ∑ i, (qs i).value (f x i)) :
99     DyadicAbstract.normalizedGaussSign d hd hk q =
100       ∏ i, DyadicAbstract.normalizedGaussSign (b i) (ha i) (hn i) (qs i) := by
101   simp_rw [DyadicAbstract.normalizedGaussSign_eq_sign]
102   rw [arf_of_decomposition b ha hn d hd hk f hf q qs hq, sign_sum]
103   push_cast
104   rfl
105 
106 include b ha hn in
107 omit [FiniteDimensional F2 X] in
108 /-- The displayed normalization exponent transports through the actual
109 decomposition, rather than being supplied as a numerical assumption. -/
110 theorem half_finrank_of_decomposition (f : X ≃ₗ[F2] (∀ i, V i)) :
111     Module.finrank F2 X / 2 = ∑ i, Module.finrank F2 (V i) / 2 := by
112   rw [f.finrank_eq]
113   exact half_finrank_product b ha hn
114 
115 end PaperXI.BreakDyadicPhase

Back to source controls