Classification of cyclic dyadic quadratic modules

Every finite quadratic module whose underlying group is cyclic of order 2^k, with k ≥ 1, is isometric to a dyadic cyclic module q_θ^{(2)}(2^k). If the module is nondegenerate, the coefficient θ is odd. This identifies the cyclic constituents in the dyadic part of Nikulin's generator decomposition; unlike the odd-primary case, general dyadic modules also require the rank-two generators u^{(2)}(2^k) and v^{(2)}(2^k).

The change-of-generator criterion is also explicit. An additive automorphism of ℤ/2^k is multiplication by a unit u, and it identifies the coefficients θ and η exactly when

θ / 2^{k+1} = η u² / 2^{k+1}  in ℚ/ℤ.

The representative u.val.val in the theorem below is the canonical natural representative of the unit modulo 2^k. Changing that representative by a multiple of 2^k does not change its square modulo 2^{k+1}.

For odd coefficients, the criterion reduces to congruence modulo four at order two and modulo eight at every higher order. Thus the nondegenerate cyclic classes have unique coefficient representatives 1, 3 at order two and 1, 3, 5, 7 at order 2^k for k ≥ 2. The uniqueness concerns the isometry class, not the isometry itself. The modulus four exception is essential: coefficients 1 and 5 agree at order two but not at order four.

Main declarations

• TauCeti.FiniteQuadraticModule.exists_dyadicCyclic_isometry_of_card_eq_two_pow: every quadratic module on a cyclic group of order 2^k has a dyadic cyclic presentation.
• TauCeti.FiniteQuadraticModule.exists_dyadicCyclic_isometry: in the nondegenerate case the coefficient can be taken odd.
• TauCeti.FiniteQuadraticModule.dyadicCyclicIsometryOfModEqEight: odd coefficients congruent modulo eight yield isometric cyclic modules at every positive exponent.
• TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicCyclic_iff: the unit-square coefficient criterion modulo 2^{k+1}.
• TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicCyclic_one_iff: the coefficient criterion modulo four at order two, including even coefficients.
• TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicCyclic_iff_modEq_eight: the coefficient criterion modulo eight at higher orders, for an odd source coefficient.
• TauCeti.FiniteQuadraticModule.existsUnique_dyadicCyclic_one_isometry: unique coefficient representatives 1, 3 for nondegenerate modules of order two, which are automatically cyclic.
• TauCeti.FiniteQuadraticModule.existsUnique_dyadicCyclic_isometry_of_two_le: unique coefficient representatives 1, 3, 5, 7 for nondegenerate cyclic modules of higher order.

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_dyadicCyclic_isometry_of_card_eq_two_pow (A : FiniteQuadraticModule) [IsAddCyclic A.carrier] {k : ℕ} [NeZero k] (hcard : Nat.card A.carrier = 2 ^ k) : ∃ (θ : ℤ), Nonempty ((dyadicCyclic k θ).Isometry A)

Every quadratic module on a cyclic group of order 2^k, for k ≥ 1, has a dyadic cyclic presentation. No nondegeneracy hypothesis is needed.

theorem TauCeti.FiniteQuadraticModule.exists_dyadicCyclic_isometry (A : FiniteQuadraticModule) [IsAddCyclic A.carrier] {k : ℕ} [NeZero k] (hcard : Nat.card A.carrier = 2 ^ k) (hA : A.IsNondegenerate) : ∃ (θ : ℤ), Odd θ ∧ Nonempty ((dyadicCyclic k θ).Isometry A)

Every nondegenerate quadratic module on a cyclic group of order 2^k, for k ≥ 1, is isometric to q_θ^{(2)}(2^k) for an odd coefficient θ.

@[simp]

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicCyclic_iff {k : ℕ} [NeZero k] (θ η : ℤ) : Nonempty ((dyadicCyclic k θ).Isometry (dyadicCyclic k η)) ↔ ∃ (u : (ZMod (2 ^ k))ˣ), ↑θ = ↑(η * ↑(↑u).val ^ 2)

The dyadic cyclic isometry criterion: q_θ^{(2)}(2^k) and q_η^{(2)}(2^k) are isometric exactly when θ and ηu² agree modulo 2^{k+1} for some unit u modulo 2^k. The unit is represented by its canonical natural representative u.val.val; changing that representative by a multiple of 2^k leaves its square unchanged modulo 2^{k+1}.

noncomputable def TauCeti.FiniteQuadraticModule.dyadicCyclicIsometryOfModEqEight (k : ℕ) [NeZero k] {θ η : ℤ} (hθ : Odd θ) (h : θ ≡ η [ZMOD 8]) : (dyadicCyclic k θ).Isometry (dyadicCyclic k η)

Odd coefficients congruent modulo eight give isometric cyclic dyadic quadratic forms at every positive exponent.

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicCyclic_one_iff (θ η : ℤ) : Nonempty ((dyadicCyclic 1 θ).Isometry (dyadicCyclic 1 η)) ↔ θ ≡ η [ZMOD 4]

At order two, cyclic dyadic quadratic modules are isometric exactly when their coefficients agree modulo four. This also holds for even coefficients.

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_dyadicCyclic_iff_modEq_eight {k : ℕ} [NeZero k] (hk : 2 ≤ k) {θ η : ℤ} (hθ : Odd θ) : Nonempty ((dyadicCyclic k θ).Isometry (dyadicCyclic k η)) ↔ θ ≡ η [ZMOD 8]

At order at least four, nondegenerate cyclic dyadic quadratic modules are isometric exactly when their coefficients agree modulo eight. Only the source coefficient needs to be assumed odd; the congruence forces the target coefficient to be odd as well.

theorem TauCeti.FiniteQuadraticModule.existsUnique_dyadicCyclic_one_isometry (A : FiniteQuadraticModule) (hcard : Nat.card A.carrier = 2) (hA : A.IsNondegenerate) : ∃! i : Fin 2, Nonempty ((dyadicCyclic 1 (2 * ↑↑i + 1)).Isometry A)

Every nondegenerate quadratic module of order two, necessarily cyclic, has exactly one of the coefficient representatives 1, 3. The unique index selects the coefficient 2i + 1.

theorem TauCeti.FiniteQuadraticModule.existsUnique_dyadicCyclic_isometry_of_two_le (A : FiniteQuadraticModule) [IsAddCyclic A.carrier] {k : ℕ} [NeZero k] (hk : 2 ≤ k) (hcard : Nat.card A.carrier = 2 ^ k) (hA : A.IsNondegenerate) : ∃! i : Fin 4, Nonempty ((dyadicCyclic k (2 * ↑↑i + 1)).Isometry A)

At each order 2^k ≥ 4, every nondegenerate cyclic quadratic module has exactly one of the coefficient representatives 1, 3, 5, 7. The unique index selects 2i + 1.