DyadicIsometry.lean

1 import PaperXI.DyadicDimension
2 
3 /-! Quadratic refinements and their Arf values transport along actual isometries. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.DyadicIsometry
7 open scoped BigOperators Classical
8 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates PaperXI.DyadicBasis
9 
10 variable {V W ι κ : Type*} [AddCommGroup V] [Module F2 V]
11   [AddCommGroup W] [Module F2 W] [Fintype ι] [Fintype κ]
12 variable {b : V →ₗ[F2] V →ₗ[F2] F2} {c : W →ₗ[F2] W →ₗ[F2] F2}
13 
14 def transportRefinement (f : V ≃ₗ[F2] W)
15     (hf : ∀ x y, b x y = c (f x) (f y)) (q : Refinement b) : Refinement c where
16   value x := q.value (f.symm x)
17   polar x y := by
18     rw [map_add, q.polar, hf]
19     simp
20 
21 @[simp] theorem transportRefinement_apply (f : V ≃ₗ[F2] W)
22     (hf : ∀ x y, b x y = c (f x) (f y)) (q : Refinement b) (x : W) :
23     (transportRefinement f hf q).value x = q.value (f.symm x) := rfl
24 
25 def transportRefinementEquiv (f : V ≃ₗ[F2] W)
26     (hf : ∀ x y, b x y = c (f x) (f y)) : Refinement b ≃ Refinement c where
27   toFun := transportRefinement f hf
28   invFun := transportRefinement f.symm (fun x y => by simpa using (hf (f.symm x) (f.symm y)).symm)
29   left_inv q := by ext x; simp [transportRefinement]
30   right_inv q := by ext x; simp [transportRefinement]
31 
32 /-- Transport preserves the intrinsic Gauss sum by bijectivity. -/
33 theorem gauss_sum_transport [Fintype V] [Fintype W] (f : V ≃ₗ[F2] W)
34     (hf : ∀ x y, b x y = c (f x) (f y)) (q : Refinement b) :
35     (∑ x : W, sign ((transportRefinement f hf q).value x)) =
36       ∑ x : V, sign (q.value x) := by
37   exact f.symm.toEquiv.sum_comp (fun x => sign (q.value x))
38 
39 /-- An actual form-preserving linear equivalence preserves Arf, even when the
40 two supplied symplectic coordinate systems use different finite index types. -/
41 theorem basisArf_transport (f : V ≃ₗ[F2] W)
42     (hf : ∀ x y, b x y = c (f x) (f y))
43     (eV : V ≃ₗ[F2] (ι → F2 × F2)) (eW : W ≃ₗ[F2] (κ → F2 × F2))
44     (heV : ∀ x y, b x y = symplectic (eV x) (eV y))
45     (heW : ∀ x y, c x y = symplectic (eW x) (eW y)) (q : Refinement b) :
46     basisArf eW (transportRefinement f hf q) = basisArf eV q := by
47   change basisArf (f.trans eW) q = basisArf eV q
48   apply DyadicDimension.basisArf_independent (f.trans eW) eV _ heV q
49   intro x y
50   exact (hf x y).trans (heW (f x) (f y))
51 
52 end PaperXI.DyadicIsometry

Back to source controls