Nikulin's generators decompose every nondegenerate finite quadratic module

Every nondegenerate finite quadratic module is isometric to an orthogonal sum of Nikulin's generators:

• the odd cyclic modules q_θ^{(p)}(p^k) on ℤ/p^k, for an odd prime p, k ≥ 1 and θ prime to p, with b(x, y) = θxy / p^k;
• the dyadic cyclic modules q_θ^{(2)}(2^k) on ℤ/2^k, for k ≥ 1 and θ odd, with q(x) = θx² / 2^{k+1};
• the rank-two modules u^{(2)}(2^k) and v^{(2)}(2^k) on (ℤ/2^k)², for k ≥ 1, with q(x) = x₁x₂ / 2^k and q(x) = (x₁² + x₁x₂ + x₂²) / 2^k.

This is the generator half of Nikulin's Proposition 1.8.1. The orthogonal sum is written as a product of four orthogonal sums, one for each family, each indexed by Fin n.

The proof splits off one generator at a time. A nontrivial nondegenerate module A has a prime p dividing its order. For odd p some cyclic subgroup of p-power order is nondegenerate (TauCeti.FiniteBilinearModule.exists_isNondegenerate_restrict_zmultiples), and it is an odd cyclic generator; for p = 2 some nonzero subgroup is a dyadic generator (TauCeti.FiniteQuadraticModule.exists_dyadic_summand). Such a summand H is nondegenerate, so A ≅ H ⊥ H⊥ with H⊥ nondegenerate of smaller order, and induction on the order applies to H⊥.

The decomposition is not unique: Nikulin's Proposition 1.8.2 lists the relations among the generators, and they are not treated here.

Main declaration

• TauCeti.FiniteQuadraticModule.exists_isometry_prod_pi_generators: a nondegenerate finite quadratic module is isometric to an orthogonal sum of odd cyclic, dyadic cyclic, u and v generators.

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_isometry_prod_pi_generators (A : FiniteQuadraticModule) (hA : A.IsNondegenerate) : ∃ (a : ℕ) (m : Fin a → ℕ) (hm : ∀ (i : Fin a), Odd (m i)) (θ : Fin a → ℤ) (b : ℕ) (k : Fin b → ℕ) (η : Fin b → ℤ) (c : ℕ) (ku : Fin c → ℕ) (d : ℕ) (kv : Fin d → ℕ), (∀ (i : Fin a), IsPrimePow (m i) ∧ IsCoprime (↑(m i)) (θ i)) ∧ (∀ (i : Fin b), Odd (η i)) ∧ Nonempty (((pi fun (i : Fin a) => oddCyclic (m i) ⋯ (θ i)).prod ((pi fun (i : Fin b) => dyadicCyclic (k i + 1) (η i)).prod ((pi fun (i : Fin c) => dyadicU (ku i + 1)).prod (pi fun (i : Fin d) => dyadicV (kv i + 1))))).Isometry A)

Nikulin's generator decomposition. A nondegenerate finite quadratic module is isometric to an orthogonal sum of Nikulin's generators: odd cyclic modules q_θ^{(p)}(p^k) of odd prime-power order m = p^k with θ prime to m, dyadic cyclic modules q_η^{(2)}(2^{k+1}) with η odd, and rank-two modules u^{(2)}(2^{k+1}) and v^{(2)}(2^{k+1}).