DyadicDimension.lean

1 import PaperXI.DyadicBasis
2 import Mathlib.LinearAlgebra.Dimension.Constructions
3 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
4 
5 /-! Dimensions and Arf comparison for arbitrary finite symplectic index types.
6 All coordinate maps in this module are explicit inputs. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DyadicDimension
10 open scoped BigOperators Classical
11 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates PaperXI.DyadicBasis
12 
13 variable {V ι κ : Type*} [AddCommGroup V] [Module F2 V] [Fintype ι] [Fintype κ]
14 
15 theorem finrank_eq_twice_card (e : V ≃ₗ[F2] (ι → F2 × F2)) :
16     Module.finrank F2 V = 2 * Fintype.card ι := by
17   rw [e.finrank_eq, Module.finrank_pi_fintype]
18   simp [Module.finrank_prod, Nat.mul_comm]
19 
20 theorem card_eq_finrank_div_two (e : V ≃ₗ[F2] (ι → F2 × F2)) :
21     Fintype.card ι = Module.finrank F2 V / 2 := by
22   rw [finrank_eq_twice_card e]
23   omega
24 
25 theorem card_pos [Nontrivial V] (e : V ≃ₗ[F2] (ι → F2 × F2)) :
26     0 < Fintype.card ι := by
27   let : FiniteDimensional F2 V := e.symm.finiteDimensional
28   have h := Module.finrank_pos (R := F2) (M := V)
29   rw [finrank_eq_twice_card e] at h
30   omega
31 
32 theorem coordinate_card_eq (e : V ≃ₗ[F2] (ι → F2 × F2))
33     (f : V ≃ₗ[F2] (κ → F2 × F2)) : Fintype.card ι = Fintype.card κ := by
34   rw [card_eq_finrank_div_two e, card_eq_finrank_div_two f]
35 
36 /-- Arf is independent of both the coordinate map and its finite index type.
37 The finite enumeration of the underlying space is derived from the map. -/
38 theorem basisArf_independent {b : V →ₗ[F2] V →ₗ[F2] F2}
39     (e : V ≃ₗ[F2] (ι → F2 × F2)) (f : V ≃ₗ[F2] (κ → F2 × F2))
40     (he : ∀ x y, b x y = symplectic (e x) (e y))
41     (hf : ∀ x y, b x y = symplectic (f x) (f y)) (q : Refinement b) :
42     basisArf e q = basisArf f q := by
43   let : Fintype V := Fintype.ofEquiv (ι → F2 × F2) e.symm.toEquiv
44   apply sign_injective
45   have h := (gauss_sum e he q).symm.trans (gauss_sum f hf q)
46   rw [coordinate_card_eq e f] at h
47   exact mul_right_cancel₀ (pow_ne_zero _ (by norm_num : (2 : ℤ) ≠ 0)) h
48 
49 end PaperXI.DyadicDimension

Back to source controls