SymplecticAssembly.lean

1 import PaperXI.DyadicCoordinates
2 import Mathlib.LinearAlgebra.Dimension.Finrank
3 
4 /-! Adding one hyperbolic plane to an existing symplectic coordinate system. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.SymplecticAssembly
8 open scoped BigOperators Classical
9 open PaperXI.Dyadic PaperXI.DyadicCoordinates
10 
11 def prepend (r : ℕ) : ((F2 × F2) × (Fin r → F2 × F2)) ≃ₗ[F2]
12     (Fin (r + 1) → F2 × F2) where
13   toFun x := Fin.cons x.1 x.2
14   invFun x := (x 0, fun i => x i.succ)
15   left_inv x := by rfl
16   right_inv x := by
17     funext i
18     refine Fin.cases ?_ (fun j => ?_) i <;> simp
19   map_add' x y := by
20     funext i
21     refine Fin.cases ?_ (fun j => ?_) i <;> simp
22   map_smul' a x := by
23     funext i
24     refine Fin.cases ?_ (fun j => ?_) i <;> simp
25 
26 theorem prepend_form (r : ℕ) (x y : (F2 × F2) × (Fin r → F2 × F2)) :
27     symplectic (prepend r x) (prepend r y) =
28       x.1.1 * y.1.2 + x.1.2 * y.1.1 + symplectic x.2 y.2 := by
29   change symplectic (Fin.cons x.1 x.2) (Fin.cons y.1 y.2) = _
30   simp [symplectic_apply, Fin.sum_univ_succ]
31 
32 variable {V W : Type*} [AddCommGroup V] [Module F2 V]
33   [AddCommGroup W] [Module F2 W]
34 
35 def assemble (r : ℕ) (e : V ≃ₗ[F2] ((F2 × F2) × W))
36     (f : W ≃ₗ[F2] (Fin r → F2 × F2)) :
37     V ≃ₗ[F2] (Fin (r + 1) → F2 × F2) :=
38   e.trans (((LinearEquiv.refl F2 (F2 × F2)).prodCongr f).trans (prepend r))
39 
40 theorem assemble_form (r : ℕ) (b : V →ₗ[F2] V →ₗ[F2] F2)
41     (c : W →ₗ[F2] W →ₗ[F2] F2)
42     (e : V ≃ₗ[F2] ((F2 × F2) × W)) (f : W ≃ₗ[F2] (Fin r → F2 × F2))
43     (he : ∀ x y, b x y = (e x).1.1 * (e y).1.2 +
44       (e x).1.2 * (e y).1.1 + c (e x).2 (e y).2)
45     (hf : ∀ x y, c x y = symplectic (f x) (f y)) (x y : V) :
46     b x y = symplectic (assemble r e f x) (assemble r e f y) := by
47   change b x y = symplectic (prepend r ((e x).1, f (e x).2))
48     (prepend r ((e y).1, f (e y).2))
49   rw [prepend_form, he, hf]
50 
51 end PaperXI.SymplecticAssembly

Back to source controls