DyadicAbstractOrthogonal.lean

1 import PaperXI.DyadicAbstract
2 import PaperXI.DyadicIsometry
3 import PaperXI.DyadicOrthogonal
4 
5 /-! Intrinsic Arf and Gauss-sign laws for actual orthogonal sums.
6 Symplectic coordinates are constructed from alternation and nondegeneracy. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DyadicAbstractOrthogonal
10 open scoped BigOperators Classical
11 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
12 
13 variable {V W X : Type*} [AddCommGroup V] [Module F2 V]
14   [AddCommGroup W] [Module F2 W] [AddCommGroup X] [Module F2 X]
15 variable (b : V →ₗ[F2] V →ₗ[F2] F2) (c : W →ₗ[F2] W →ₗ[F2] F2)
16 
17 theorem form_alternating (ha : ∀ x, b x x = 0) (hc : ∀ x, c x x = 0)
18     (x : V × W) : DyadicOrthogonal.form b c x x = 0 := by
19   simp [DyadicOrthogonal.form_apply, ha, hc]
20 
21 theorem form_nondegenerate
22     (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
23     (hm : ∀ x, (∀ y, c x y = 0) → x = 0)
24     (x : V × W) (hx : ∀ y, DyadicOrthogonal.form b c x y = 0) : x = 0 := by
25   apply Prod.ext
26   · apply hn x.1
27     intro y
28     simpa using hx (y, 0)
29   · apply hm x.2
30     intro y
31     simpa using hx (0, y)
32 
33 variable [FiniteDimensional F2 V] [FiniteDimensional F2 W]
34 variable (ha : ∀ x, b x x = 0) (hn : ∀ x, (∀ y, b x y = 0) → x = 0)
35   (hc : ∀ x, c x x = 0) (hm : ∀ x, (∀ y, c x y = 0) → x = 0)
36 
37 /-- Intrinsic Arf is preserved by an actual form-preserving linear equivalence. -/
38 theorem arf_transport (f : V ≃ₗ[F2] W)
39     (hf : ∀ x y, b x y = c (f x) (f y)) (q : Refinement b) :
40     DyadicAbstract.arf c hc hm (DyadicIsometry.transportRefinement f hf q) =
41       DyadicAbstract.arf b ha hn q := by
42   rw [DyadicAbstract.arf_eq_basis c hc hm (DyadicAbstract.coordinates c hc hm)
43     (DyadicAbstract.coordinates_form c hc hm),
44     DyadicAbstract.arf_eq_basis b ha hn (DyadicAbstract.coordinates b ha hn)
45     (DyadicAbstract.coordinates_form b ha hn)]
46   exact DyadicIsometry.basisArf_transport f hf
47     (DyadicAbstract.coordinates b ha hn) (DyadicAbstract.coordinates c hc hm)
48     (DyadicAbstract.coordinates_form b ha hn) (DyadicAbstract.coordinates_form c hc hm) q
49 
50 /-- Manuscript 13.6: Arf is additive on the actual product quadratic refinement,
51 without assuming any symplectic coordinate maps. -/
52 theorem arf_add (q : Refinement b) (r : Refinement c) :
53     DyadicAbstract.arf (DyadicOrthogonal.form b c)
54       (form_alternating b c ha hc) (form_nondegenerate b c hn hm)
55       (DyadicOrthogonal.refinement b c q r) =
56       DyadicAbstract.arf b ha hn q + DyadicAbstract.arf c hc hm r := by
57   let e := DyadicAbstract.coordinates b ha hn
58   let f := DyadicAbstract.coordinates c hc hm
59   let : Fintype V := Fintype.ofEquiv _ e.symm.toEquiv
60   let : Fintype W := Fintype.ofEquiv _ f.symm.toEquiv
61   have he := DyadicAbstract.coordinates_form b ha hn
62   have hf := DyadicAbstract.coordinates_form c hc hm
63   rw [DyadicAbstract.arf_eq_basis (DyadicOrthogonal.form b c)
64     (form_alternating b c ha hc) (form_nondegenerate b c hn hm)
65     (DyadicOrthogonal.coordinates e f) (DyadicOrthogonal.coordinates_form e f he hf),
66     DyadicAbstract.arf_eq_basis b ha hn e he,
67     DyadicAbstract.arf_eq_basis c hc hm f hf]
68   exact DyadicOrthogonal.arf_add e f he hf q r
69 
70 /-- The normalized Gauss signs multiply on an orthogonal sum. -/
71 theorem arf_sign_product (q : Refinement b) (r : Refinement c) :
72     sign (DyadicAbstract.arf (DyadicOrthogonal.form b c)
73       (form_alternating b c ha hc) (form_nondegenerate b c hn hm)
74       (DyadicOrthogonal.refinement b c q r)) =
75       sign (DyadicAbstract.arf b ha hn q) * sign (DyadicAbstract.arf c hc hm r) := by
76   rw [arf_add b c ha hn hc hm, sign_add]
77 
78 variable [FiniteDimensional F2 X]
79 variable (d : X →ₗ[F2] X →ₗ[F2] F2)
80   (hd : ∀ x, d x x = 0) (hk : ∀ x, (∀ y, d x y = 0) → x = 0)
81 
82 /-- An arbitrary orthogonal decomposition is represented by its actual linear
83 equivalence, the form identity, and the equality of quadratic-refinement values. -/
84 theorem arf_of_decomposition (f : X ≃ₗ[F2] V × W)
85     (hf : ∀ x y, d x y = DyadicOrthogonal.form b c (f x) (f y))
86     (q : Refinement d) (qV : Refinement b) (qW : Refinement c)
87     (hq : ∀ x, q.value x = qV.value (f x).1 + qW.value (f x).2) :
88     DyadicAbstract.arf d hd hk q =
89       DyadicAbstract.arf b ha hn qV + DyadicAbstract.arf c hc hm qW := by
90   have hq' : DyadicIsometry.transportRefinement f hf q =
91       DyadicOrthogonal.refinement b c qV qW := by
92     ext x
93     simp only [DyadicIsometry.transportRefinement_apply,
94       DyadicOrthogonal.refinement]
95     rw [hq]
96     simp
97   calc
98     DyadicAbstract.arf d hd hk q = DyadicAbstract.arf (DyadicOrthogonal.form b c)
99         (form_alternating b c ha hc) (form_nondegenerate b c hn hm)
100         (DyadicIsometry.transportRefinement f hf q) :=
101       (arf_transport d (DyadicOrthogonal.form b c) hd hk
102         (form_alternating b c ha hc) (form_nondegenerate b c hn hm) f hf q).symm
103     _ = DyadicAbstract.arf b ha hn qV + DyadicAbstract.arf c hc hm qW := by
104       rw [hq']
105       exact arf_add b c ha hn hc hm qV qW
106 
107 theorem arf_sign_of_decomposition (f : X ≃ₗ[F2] V × W)
108     (hf : ∀ x y, d x y = DyadicOrthogonal.form b c (f x) (f y))
109     (q : Refinement d) (qV : Refinement b) (qW : Refinement c)
110     (hq : ∀ x, q.value x = qV.value (f x).1 + qW.value (f x).2) :
111     sign (DyadicAbstract.arf d hd hk q) =
112       sign (DyadicAbstract.arf b ha hn qV) * sign (DyadicAbstract.arf c hc hm qW) := by
113   rw [arf_of_decomposition b c ha hn hc hm d hd hk f hf q qV qW hq, sign_add]
114 
115 /-- Multiplicativity of the actual Gauss sum divided by its positive power of two. -/
116 theorem normalized_sign_product (q : Refinement b) (r : Refinement c) :
117     DyadicAbstract.normalizedGaussSign (DyadicOrthogonal.form b c)
118       (form_alternating b c ha hc) (form_nondegenerate b c hn hm)
119       (DyadicOrthogonal.refinement b c q r) =
120       DyadicAbstract.normalizedGaussSign b ha hn q *
121         DyadicAbstract.normalizedGaussSign c hc hm r := by
122   rw [DyadicAbstract.normalizedGaussSign_eq_sign,
123     DyadicAbstract.normalizedGaussSign_eq_sign,
124     DyadicAbstract.normalizedGaussSign_eq_sign]
125   exact_mod_cast arf_sign_product b c ha hn hc hm q r
126 
127 /-- The actual normalized Gauss sum is multiplicative after any supplied
128 orthogonal decomposition of the quadratic space. -/
129 theorem normalized_sign_of_decomposition (f : X ≃ₗ[F2] V × W)
130     (hf : ∀ x y, d x y = DyadicOrthogonal.form b c (f x) (f y))
131     (q : Refinement d) (qV : Refinement b) (qW : Refinement c)
132     (hq : ∀ x, q.value x = qV.value (f x).1 + qW.value (f x).2) :
133     DyadicAbstract.normalizedGaussSign d hd hk q =
134       DyadicAbstract.normalizedGaussSign b ha hn qV *
135         DyadicAbstract.normalizedGaussSign c hc hm qW := by
136   rw [DyadicAbstract.normalizedGaussSign_eq_sign,
137     DyadicAbstract.normalizedGaussSign_eq_sign,
138     DyadicAbstract.normalizedGaussSign_eq_sign]
139   exact_mod_cast arf_sign_of_decomposition b c ha hn hc hm d hd hk f hf q qV qW hq
140 
141 end PaperXI.DyadicAbstractOrthogonal

Back to source controls