Duality and the Wall sign relation

The kernel-perpendicular identification and the final sign comparison.

See GQ2.GaussCount for the paper-facing overview, source citations, and deviations.

Duality and the kernel-perp identification

For the fiber computation we need K^⊥ = im N (K = ker N, N = 1 + U): the vectors pairing trivially with every U-fixed vector are exactly the image of N. The inclusion ⊇ is a direct computation; ⊆ is a counting argument through the duality #Hom(A, 𝔽₂) = #A for finite elementary abelian 2-groups.

theorem GQ2.QuadraticFp2.card_addHom_zmod2 (A : Type u_1) [AddCommGroup A] [Finite A] (h2 : ∀ (x : A), x + x = 0) : Nat.card (A →+ ZMod 2) = Nat.card A

Duality for finite elementary abelian 2-groups: #Hom(A, 𝔽₂) = #A.

theorem GQ2.QuadraticFp2.polar_ker_range {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) (hq : IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hUq : ∀ (v : V), q (U v) = q v) (N : V →+ V) (hN : ∀ (x : V), N x = x + U x) (s : V) (hs : N s = 0) (x : V) : polar q s (N x) = 0

Fixed vectors of U pair trivially with the image of N = 1 + U.

theorem GQ2.QuadraticFp2.perp_ker_iff_mem_range {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) [Finite V] (hq : IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (N : V →+ V) (hN : ∀ (x : V), N x = x + U x) (u : V) : (∀ (s : ↥N.ker), polar q (↑s) u = 0) ↔ u ∈ N.range

K^⊥ = im N: u pairs trivially with every U-fixed vector iff u ∈ im (1 + U). The forward inclusion is the duality counting (the pairing V → Hom(ker N, 𝔽₂) has kernel of the size of im N); the reverse is polar_ker_range.

Wall's sign relation

Assembling the pieces: grouping the twisted double Gauss sum over the fibers of N = 1 + U turns it into #ker N · (the Wall count of the Wall form ω(Nx, u) = B(x, u) on im N), whose monodromy is U⁻¹. With #im N = 2^k this gives

g(q_U) · g(q) = #K · (−2)^k = (−1)^k · #V = (−1)^k · g(q)²,

and cancelling g(q) ≠ 0 yields g(q_U) = (−1)^k g(q) — the sign relation of Lemma 6.6.

theorem GQ2.QuadraticFp2.gaussSum_qDouble {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (U : V ≃+ V) [Fintype V] (hq : IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ (n : ℕ), (⇑U)^[2 ^ n] = id) (N : V →+ V) (hN : ∀ (x : V), N x = x + U x) {k : ℕ} (hk : Nat.card ↥N.range = 2 ^ k) : gaussSum (qDouble q ⇑U) = (-1) ^ k * gaussSum q

Wall's sign relation (the last piece of Lemma 6.6, eq. (86)): for a nonsingular q and a 2-power-order isometry U, with N = 1 + U and #im N = 2^k,

g(q_U) = (−1)^k · g(q).