A dyadic generator splits off every nondegenerate module of even order

Let A be a nondegenerate finite quadratic module of even order. This file finds a nonzero subgroup H ≤ A whose restricted form is one of Nikulin's dyadic generators: a cyclic module q_θ^{(2)}(2^{k+1}) with θ odd, or one of the rank-two modules u^{(2)}(2^{k+1}) and v^{(2)}(2^{k+1}). Each of these is nondegenerate, so H splits off A orthogonally through TauCeti.FiniteQuadraticModule.restrictProdOrthogonalComplementIsometry.

Take x and y, both killed by 2^{k+1}, with 2^k b(x, y) ≠ 0; they exist by TauCeti.FiniteBilinearModule.exists_nsmul_pairing_ne_zero_of_dvd_card. If 2^k b(x, x) ≠ 0, then b(x, x) has the same order 2^{k+1} as x, so ⟨x⟩ is a nondegenerate cyclic summand, and likewise for y. Otherwise both self-pairings are killed by 2^k, so q(x) and q(y) are killed by 2^{k+1} because 2q(w) = b(w, w), and ⟨x, y⟩ is a rank-two block u or v. Unlike at an odd prime, x + y does not help in the last case: b(x + y, x + y) differs from b(x, x) + b(y, y) by 2b(x, y), which 2^k kills.

Main declaration

• TauCeti.FiniteQuadraticModule.exists_dyadic_summand: a nondegenerate finite quadratic module of even order has a nonzero subgroup isometric to q_θ^{(2)}(2^{k+1}) with θ odd, to u^{(2)}(2^{k+1}), or to v^{(2)}(2^{k+1}).

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Proposition 1.8.1.
• C. T. C. Wall, Quadratic forms on finite groups, and related topics, Topology 2 (1963), 281–298.

theorem TauCeti.FiniteQuadraticModule.exists_dyadic_summand {A : FiniteQuadraticModule} (hA : A.IsNondegenerate) (h2 : 2 ∣ Nat.card A.carrier) : ∃ (H : AddSubgroup A.carrier) (k : ℕ), H ≠ ⊥ ∧ ((∃ (θ : ℤ), Odd θ ∧ Nonempty ((dyadicCyclic (k + 1) θ).Isometry (A.restrict H))) ∨ Nonempty ((dyadicU (k + 1)).Isometry (A.restrict H)) ∨ Nonempty ((dyadicV (k + 1)).Isometry (A.restrict H)))

A dyadic generator splits off. A nondegenerate finite quadratic module of even order has a nonzero subgroup H whose restricted form is isometric to one of Nikulin's dyadic generators: q_θ^{(2)}(2^{k+1}) with θ odd, u^{(2)}(2^{k+1}), or v^{(2)}(2^{k+1}). All three are nondegenerate, so H is an orthogonal summand of A.