Orthogonal decomposition of nondegenerate quadratic modules of odd order

Every nondegenerate finite quadratic module of odd order is an orthogonal sum of Nikulin's odd cyclic generators q_θ^{(p)}(p^k): cyclic groups of odd prime-power order p^k with the quadratic form q(x) = θ(p^k + 1)x²/(2p^k) of the pairing b(x, y) = θxy/p^k, for θ prime to p.

The decomposition splits off one cyclic summand at a time. In a nondegenerate module A and for an odd prime p dividing #A, let x have the largest order p^k among elements of p-power order. Since b(x, ·) is a character of order p^k, some y has p^{k-1} b(x, y) ≠ 0, and y may be replaced by its p-primary part. One of x, y and x + y then has p^{k-1} b(z, z) ≠ 0, because

b(x + y, x + y) = b(x, x) + 2 b(x, y) + b(y, y)

and 2 is invertible on the p-torsion of ℚ/ℤ. For such a z the self-pairing b(z, z) has the same order p^k as z, so the cyclic subgroup ⟨z⟩ is nondegenerate and splits off orthogonally. Its orthogonal complement is nondegenerate of smaller order, and ⟨z⟩ is an odd cyclic module by the cyclic classification.

At p = 2 the argument fails at the last step, and indeed the forms u^{(2)}(2^k) and v^{(2)}(2^k) have no nondegenerate cyclic subgroup: the 2-primary part needs the rank-two generators as well.

Main declarations

• TauCeti.FiniteBilinearModule.exists_isNondegenerate_restrict_zmultiples: a nondegenerate finite bilinear module whose order is divisible by an odd prime p has an element of order p^k, k ≥ 1, generating a nondegenerate cyclic subgroup.
• TauCeti.FiniteQuadraticModule.exists_isometry_pi_oddCyclic: a nondegenerate finite quadratic module of odd order is isometric to an orthogonal sum of odd cyclic modules of prime-power order with coefficients prime to that order.

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.FiniteBilinearModule.exists_isNondegenerate_restrict_zmultiples {A : FiniteBilinearModule} {p : ℕ} [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hA : A.IsNondegenerate) (hpA : p ∣ Nat.card A.carrier) : ∃ (z : A.carrier) (k : ℕ), 0 < k ∧ addOrderOf z = p ^ k ∧ (A.restrict (AddSubgroup.zmultiples z)).IsNondegenerate

A nondegenerate cyclic summand of odd prime-power order. In a nondegenerate finite bilinear module whose order is divisible by an odd prime p, some element of order p^k, k ≥ 1, generates a cyclic subgroup on which the pairing is nondegenerate.

The hypothesis p ≠ 2 is necessary: in u^{(2)}(2), the hyperbolic pairing on (ℤ/2)², every element is isotropic, so no cyclic subgroup is nondegenerate.

theorem TauCeti.FiniteQuadraticModule.exists_isometry_pi_oddCyclic (A : FiniteQuadraticModule) (hA : A.IsNondegenerate) (hodd : Odd (Nat.card A.carrier)) : ∃ (n : ℕ) (m : Fin n → ℕ) (hm : ∀ (i : Fin n), Odd (m i)) (θ : Fin n → ℤ), (∀ (i : Fin n), IsPrimePow (m i) ∧ IsCoprime (↑(m i)) (θ i)) ∧ Nonempty ((pi fun (i : Fin n) => oddCyclic (m i) ⋯ (θ i)).Isometry A)

Nikulin's decomposition of nondegenerate quadratic modules of odd order. A nondegenerate finite quadratic module of odd order is isometric to an orthogonal sum of odd cyclic modules q_θ^{(p)}(p^k), each of odd prime-power order m = p^k with coefficient θ prime to m.