DyadicBasisCounts.lean

1 import PaperXI.DyadicBasis
2 import PaperXI.DyadicRefinementCounts
3 
4 /-! Counts of every actual refinement on an arbitrary space, conditional on
5 supplied symplectic coordinates. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.DyadicBasisCounts
9 open scoped BigOperators Classical
10 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
11 variable {V ι : Type*} [AddCommGroup V] [Module F2 V] [Fintype ι]
12 variable {b : V →ₗ[F2] V →ₗ[F2] F2}
13 
14 def arfFiberEquiv (e : V ≃ₗ[F2] (ι → F2 × F2))
15     (hb : ∀ x y, b x y = symplectic (e x) (e y)) (t : F2) :
16     {q : Refinement b // PaperXI.DyadicBasis.basisArf e q = t} ≃
17       {q : Refinement (symplectic (ι := ι)) //
18         PaperXI.DyadicRefinementCounts.basisArf q = t} :=
19   (PaperXI.DyadicBasis.refinementEquiv e hb).subtypeEquiv (fun q => by rfl)
20 
21 theorem even_count (e : V ≃ₗ[F2] (ι → F2 × F2))
22     (hb : ∀ x y, b x y = symplectic (e x) (e y)) :
23     (Nat.card {q : Refinement b // PaperXI.DyadicBasis.basisArf e q = 0} : ℚ) =
24       (2 : ℚ) ^ ((Fintype.card ι : ℤ) - 1) * ((2 : ℚ) ^ Fintype.card ι + 1) := by
25   rw [Nat.card_congr (arfFiberEquiv e hb 0), Nat.card_eq_fintype_card]
26   exact PaperXI.DyadicRefinementCounts.even_refinement_count
27 
28 theorem odd_count (e : V ≃ₗ[F2] (ι → F2 × F2))
29     (hb : ∀ x y, b x y = symplectic (e x) (e y)) :
30     (Nat.card {q : Refinement b // PaperXI.DyadicBasis.basisArf e q = 1} : ℚ) =
31       (2 : ℚ) ^ ((Fintype.card ι : ℤ) - 1) * ((2 : ℚ) ^ Fintype.card ι - 1) := by
32   rw [Nat.card_congr (arfFiberEquiv e hb 1), Nat.card_eq_fintype_card]
33   exact PaperXI.DyadicRefinementCounts.odd_refinement_count
34 
35 end PaperXI.DyadicBasisCounts

Back to source controls