DyadicRefinementCounts.lean

1 import PaperXI.DyadicCounts
2 import PaperXI.DyadicCoordinates
3 
4 /-! Cardinalities of the complete spaces of quadratic refinements with each
5 Arf invariant, including dimension zero. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.DyadicRefinementCounts
9 open scoped BigOperators Classical
10 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
11 variable {ι : Type*} [Fintype ι]
12 
13 instance refinementFintype : Fintype (Refinement (symplectic (ι := ι))) :=
14   Fintype.ofEquiv (ι → F2 × F2) coordinateEquiv
15 
16 def basisArf (q : Refinement (symplectic (ι := ι))) : F2 :=
17   ∑ i, q.value (firstAxis i) * q.value (secondAxis i)
18 
19 @[simp] theorem basisArf_coordinate (a : ι → F2 × F2) :
20     basisArf (coordinateEquiv a) = arf a := by
21   simp [basisArf, coordinateEquiv, coordinateRefinement, arf]
22 
23 /-- Restrict the complete coordinate equivalence to either Arf fiber. -/
24 def arfFiberEquiv (t : F2) :
25     {a : ι → F2 × F2 // arf a = t} ≃
26       {q : Refinement (symplectic (ι := ι)) // basisArf q = t} :=
27   coordinateEquiv.subtypeEquiv (fun a => by rw [basisArf_coordinate])
28 
29 theorem even_fiber_card :
30     Fintype.card {q : Refinement (symplectic (ι := ι)) // basisArf q = 0} =
31       PaperXI.DyadicCounts.evenCount ι := by
32   rw [← Fintype.card_congr (arfFiberEquiv (ι := ι) 0)]
33   exact Fintype.card_subtype _
34 
35 theorem odd_fiber_card :
36     Fintype.card {q : Refinement (symplectic (ι := ι)) // basisArf q = 1} =
37       PaperXI.DyadicCounts.oddCount ι := by
38   rw [← Fintype.card_congr (arfFiberEquiv (ι := ι) 1)]
39   exact Fintype.card_subtype _
40 
41 /-- The exact even Arf count for all ranks, with integer exponent r - 1. -/
42 theorem even_refinement_count :
43     (Fintype.card {q : Refinement (symplectic (ι := ι)) // basisArf q = 0} : ℚ) =
44       (2 : ℚ) ^ ((Fintype.card ι : ℤ) - 1) * ((2 : ℚ) ^ Fintype.card ι + 1) := by
45   rw [even_fiber_card]
46   exact PaperXI.DyadicCounts.even_factored_rational
47 
48 /-- The exact odd Arf count for all ranks, with integer exponent r - 1. -/
49 theorem odd_refinement_count :
50     (Fintype.card {q : Refinement (symplectic (ι := ι)) // basisArf q = 1} : ℚ) =
51       (2 : ℚ) ^ ((Fintype.card ι : ℤ) - 1) * ((2 : ℚ) ^ Fintype.card ι - 1) := by
52   rw [odd_fiber_card]
53   exact PaperXI.DyadicCounts.odd_factored_rational
54 
55 end PaperXI.DyadicRefinementCounts

Back to source controls