DyadicBasisConsequences.lean

1 import PaperXI.DyadicBasis
2 import PaperXI.DyadicRefinement
3 
4 /-! Translation and opposite Arf phases on arbitrary spaces with supplied
5 symplectic coordinates. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.DyadicBasisConsequences
9 open scoped BigOperators Classical
10 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
11 open PaperXI.DyadicBasis
12 
13 variable {V ι : Type*} [AddCommGroup V] [Module F2 V] [Fintype ι]
14 variable {b : V →ₗ[F2] V →ₗ[F2] F2}
15 
16 theorem toCoordinates_addLinear (e : V ≃ₗ[F2] (ι → F2 × F2))
17     (hb : ∀ x y, b x y = symplectic (e x) (e y))
18     (q : Refinement b) (v : V) :
19     toCoordinates e hb (addLinear q (b v)) =
20       addLinear (toCoordinates e hb q) (symplectic (e v)) := by
21   ext x
22   simp [toCoordinates, addLinear, hb]
23 
24 /-- Translation by the actual bilinear functional b(v,-) changes Arf by q(v). -/
25 theorem arf_translation (e : V ≃ₗ[F2] (ι → F2 × F2))
26     (hb : ∀ x y, b x y = symplectic (e x) (e y))
27     (q : Refinement b) (v : V) :
28     basisArf e (addLinear q (b v)) = basisArf e q + q.value v := by
29   calc
30     basisArf e (addLinear q (b v)) =
31         PaperXI.DyadicRefinement.basisArf
32           (toCoordinates e hb (addLinear q (b v))) := rfl
33     _ = PaperXI.DyadicRefinement.basisArf
34         (addLinear (toCoordinates e hb q) (symplectic (e v))) := by
35       rw [toCoordinates_addLinear]
36     _ = PaperXI.DyadicRefinement.basisArf (toCoordinates e hb q) +
37         (toCoordinates e hb q).value (e v) :=
38       PaperXI.DyadicRefinement.arf_translation _ _
39     _ = basisArf e q + q.value v := by
40       simp [PaperXI.DyadicRefinement.basisArf, basisArf, toCoordinates]
41 
42 theorem basisArf_fromCoordinates (e : V ≃ₗ[F2] (ι → F2 × F2))
43     (hb : ∀ x y, b x y = symplectic (e x) (e y))
44     (q : Refinement (symplectic (ι := ι))) :
45     basisArf e (fromCoordinates e hb q) = PaperXI.DyadicRefinement.basisArf q := by
46   simp [basisArf, fromCoordinates, PaperXI.DyadicRefinement.basisArf]
47 
48 theorem gauss_fromCoordinates [Fintype V] (e : V ≃ₗ[F2] (ι → F2 × F2))
49     (hb : ∀ x y, b x y = symplectic (e x) (e y))
50     (q : Refinement (symplectic (ι := ι))) :
51     (∑ v : V, sign ((fromCoordinates e hb q).value v)) =
52       ∑ x : ι → F2 × F2, sign (q.value x) :=
53   e.toEquiv.sum_comp (fun x => sign (q.value x))
54 
55 /-- A nonzero number of symplectic pairs gives actual refinements with
56 opposite Arf values and opposite nonzero Gauss phases. -/
57 theorem opposite_refinements [Fintype V] (e : V ≃ₗ[F2] (ι → F2 × F2))
58     (hb : ∀ x y, b x y = symplectic (e x) (e y)) (i : ι) :
59     ∃ q r : Refinement b,
60       basisArf e q = 0 ∧ basisArf e r = 1 ∧
61       (∑ x : V, sign (r.value x)) = -(∑ x : V, sign (q.value x)) := by
62   obtain ⟨q, r, hq, hr, hs⟩ := PaperXI.DyadicRefinement.opposite_refinements i
63   refine ⟨fromCoordinates e hb q, fromCoordinates e hb r, ?_, ?_, ?_⟩
64   · simpa only [basisArf_fromCoordinates] using hq
65   · simpa only [basisArf_fromCoordinates] using hr
66   · simpa only [gauss_fromCoordinates] using hs
67 
68 end PaperXI.DyadicBasisConsequences

Back to source controls