The dyadic cyclic generators q_θ^{(2)}(2^k)

For k ≥ 1 and an integer θ, this file constructs the cyclic group ℤ/2^k with

q(x) = θx² / 2^{k+1},   b(x, y) = θxy / 2^k.

For odd θ, this is Nikulin's dyadic cyclic generator q_θ^{(2)}(2^k). In the half-norm convention it is the discriminant form of the 2-adic lattice of rank one with Gram matrix (θ·2^k), and it is one of the generators of Nikulin's classification of nondegenerate finite quadratic modules, alongside the odd-primary cyclic forms and the two forms u^{(2)}(2^k), v^{(2)}(2^k) on (ℤ/2^k)². For even θ, it is the degenerate extension of the same formula.

This file constructs it from the cyclic presentation TauCeti.FiniteQuadraticModule.cyclic and proves it nondegenerate exactly for odd θ (Nikulin, Proposition 1.8.1).

Main declarations

• TauCeti.FiniteQuadraticModule.dyadicCyclic: the finite quadratic module q_θ^{(2)}(2^k).
• TauCeti.FiniteQuadraticModule.isNondegenerate_dyadicCyclic_iff: it is nondegenerate exactly when θ is odd.
• TauCeti.FiniteQuadraticModule.dyadicCyclicBilinearIsometryOfModEq: coefficient congruence modulo 2^k gives a bilinear isometry.
• TauCeti.FiniteQuadraticModule.dyadicCyclicOneBilinearIsometry: all odd coefficients at exponent one give the same bilinear form.
• TauCeti.FiniteQuadraticModule.dyadicCyclicTwoBilinearIsometryFiveMul: multiplication by five preserves the bilinear form at exponent two.

References

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

The generator

noncomputable def TauCeti.FiniteQuadraticModule.dyadicCyclic (k : ℕ) [NeZero k] (θ : ℤ) : FiniteQuadraticModule

The cyclic group ℤ/2^k, for k ≥ 1, with quadratic form q(x) = θx² / 2^{k+1} and pairing b(x, y) = θxy / 2^k. For odd θ, this is Nikulin's dyadic cyclic generator q_θ^{(2)}(2^k), the discriminant form of the rank-one 2-adic lattice with Gram matrix (θ·2^k). For even θ, it is the degenerate extension of the same formula. It is nondegenerate exactly when θ is odd.

@[simp]

theorem TauCeti.FiniteQuadraticModule.dyadicCyclic_quadratic_intCast (k : ℕ) [NeZero k] (θ j : ℤ) : (dyadicCyclic k θ).quadratic ↑j = ↑(↑θ * ↑j ^ 2 / 2 ^ (k + 1))

The quadratic form of q_θ^{(2)}(2^k) on the reduction of an integer j is θj² / 2^{k+1}.

@[simp]

theorem TauCeti.FiniteQuadraticModule.dyadicCyclic_pairing_intCast (k : ℕ) [NeZero k] (θ i j : ℤ) : ((dyadicCyclic k θ).pairing ↑i) ↑j = ↑(↑θ * ↑i * ↑j / 2 ^ k)

The pairing of q_θ^{(2)}(2^k) on the reductions of integers i and j is θij / 2^k.

@[simp]

theorem TauCeti.FiniteQuadraticModule.natCard_dyadicCyclic (k : ℕ) [NeZero k] (θ : ℤ) : Nat.card (dyadicCyclic k θ).carrier = 2 ^ k

q_θ^{(2)}(2^k) has 2^k elements. Its carrier is ℤ/2^k by definition.

theorem TauCeti.FiniteQuadraticModule.dyadicCyclic_one_quadratic_add_self_ne_zero {θ : ℤ} (hθ : Odd θ) : (dyadicCyclic 1 θ).quadratic 1 + (dyadicCyclic 1 θ).quadratic 1 ≠ 0

For odd θ, the quadratic form of q_θ^{(2)}(2) does not take values in ½ℤ/ℤ: on the generator it is θ/4, so q(1) + q(1) = θ/2 ≠ 0.

@[simp]

theorem TauCeti.FiniteQuadraticModule.isNondegenerate_dyadicCyclic_iff (k : ℕ) [NeZero k] (θ : ℤ) : (dyadicCyclic k θ).IsNondegenerate ↔ Odd θ

q_θ^{(2)}(2^k) is nondegenerate exactly when θ is odd. For even θ the nonzero element 2^{k-1} lies in the radical.

noncomputable def TauCeti.FiniteQuadraticModule.dyadicCyclicBilinearIsometryOfModEq {k : ℕ} [NeZero k] {θ η : ℤ} (h : θ ≡ η [ZMOD ↑(2 ^ k)]) : (dyadicCyclic k θ).Isometry (dyadicCyclic k η).toFiniteBilinearModule

Congruent coefficients modulo 2^k give cyclic bilinear forms related by the identity on their cyclic group. The quadratic coefficient need only agree modulo 2^k, since this statement concerns the polar pairing.

@[simp]

theorem TauCeti.FiniteQuadraticModule.dyadicCyclicBilinearIsometryOfModEq_apply {k : ℕ} [NeZero k] {θ η : ℤ} (h : θ ≡ η [ZMOD ↑(2 ^ k)]) (x : ZMod (2 ^ k)) : (dyadicCyclicBilinearIsometryOfModEq h) x = x

The coefficient-congruence bilinear isometry acts as the identity on the cyclic group.

noncomputable def TauCeti.FiniteQuadraticModule.dyadicCyclicOneBilinearIsometry {θ η : ℤ} (hθ : Odd θ) (hη : Odd η) : (dyadicCyclic 1 θ).Isometry (dyadicCyclic 1 η).toFiniteBilinearModule

All odd cyclic coefficients give isometric bilinear forms of order two, as in Nikulin's relation 1.8.2(j).

noncomputable def TauCeti.FiniteQuadraticModule.dyadicCyclicTwoBilinearIsometryFiveMul (θ : ℤ) : (dyadicCyclic 2 θ).Isometry (dyadicCyclic 2 (5 * θ)).toFiniteBilinearModule

Multiplication by five preserves the cyclic bilinear form of order four. This is Nikulin's relation 1.8.2(j) for odd coefficients, and also holds for even ones.

@[simp]

theorem TauCeti.FiniteQuadraticModule.dyadicCyclicOneBilinearIsometry_apply {θ η : ℤ} (hθ : Odd θ) (hη : Odd η) (x : (dyadicCyclic 1 θ).carrier) : (dyadicCyclicOneBilinearIsometry hθ hη) x ≍ x

The odd-coefficient bilinear isometry at exponent one fixes every element. Heterogeneous equality accommodates the two bundled carrier types.

@[simp]

theorem TauCeti.FiniteQuadraticModule.dyadicCyclicTwoBilinearIsometryFiveMul_apply (θ : ℤ) (x : (dyadicCyclic 2 θ).carrier) : (dyadicCyclicTwoBilinearIsometryFiveMul θ) x ≍ x

The coefficient-five bilinear isometry at exponent two fixes every element. Heterogeneous equality accommodates the two bundled carrier types.