Classification of odd cyclic quadratic modules

Every finite quadratic module whose underlying group is cyclic of odd order is isometric to an oddCyclic module. For a nondegenerate module, the coefficient is prime to its order. Two such cyclic forms are isometric exactly when their coefficients differ by a unit square modulo the order. Both the presentation and the coefficient criterion apply to degenerate forms and to the trivial group. At an odd prime power p^e, coefficients prime to p with the same Legendre symbol therefore give isometric generators, since their product is then a square modulo p^e.

These results identify the cyclic constituents of odd-primary discriminant forms and their change-of-generator relation. They do not assert an orthogonal decomposition of a general odd-primary module.

References

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

theorem TauCeti.FiniteQuadraticModule.exists_oddCyclic_isometry_of_odd (A : FiniteQuadraticModule) [IsAddCyclic A.carrier] (hm : Odd (Nat.card A.carrier)) : ∃ (θ : ℤ), Nonempty ((oddCyclic (Nat.card A.carrier) hm θ).Isometry A)

Every quadratic module on an odd cyclic group has an odd cyclic presentation. No nondegeneracy hypothesis is needed, and the presentation includes the trivial group.

theorem TauCeti.FiniteQuadraticModule.exists_oddCyclic_isometry (A : FiniteQuadraticModule) [IsAddCyclic A.carrier] (hm : Odd (Nat.card A.carrier)) (hA : A.IsNondegenerate) : ∃ (θ : ℤ), IsCoprime (↑(Nat.card A.carrier)) θ ∧ Nonempty ((oddCyclic (Nat.card A.carrier) hm θ).Isometry A)

Every nondegenerate quadratic module on an odd cyclic group has an odd cyclic presentation with coefficient prime to the group order.

@[simp]

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_oddCyclic_iff (m : ℕ) (hm : Odd m) (θ η : ℤ) : Nonempty ((oddCyclic m hm θ).Isometry (oddCyclic m hm η)) ↔ ∃ (u : (ZMod m)ˣ), ↑θ = ↑η * ↑u ^ 2

Two odd cyclic quadratic modules of the same order are isometric exactly when their coefficients differ by a unit square modulo that order. No nondegeneracy hypothesis is needed; the criterion includes the trivial group ZMod 1.

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_oddCyclic_of_eq_zero {p : ℕ} (hp : Odd p) {e : ℕ} (he : e = 0) (a b : ℤ) : Nonempty ((oddCyclic (p ^ e) ⋯ a).Isometry (oddCyclic (p ^ e) ⋯ b))

Two odd cyclic generators of order p^0 = 1 are isometric: both are trivial.

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_oddCyclic_of_legendreSym_eq {p : ℕ} [Fact (Nat.Prime p)] (hp : Odd p) (e : ℕ) {a b : ℤ} (ha : IsCoprime (↑p) a) (hb : IsCoprime (↑p) b) (h : legendreSym p a = legendreSym p b) : Nonempty ((oddCyclic (p ^ e) ⋯ a).Isometry (oddCyclic (p ^ e) ⋯ b))

Odd cyclic generators q_a^{(p)}(p^e) and q_b^{(p)}(p^e) with the same Legendre symbol are isometric: ab is then a square modulo p^e.