Two-elementary finite quadratic modules

A finite quadratic module is 2-elementary when its group is killed by 2, so that it is (ℤ/2)^a for some a. This file shows that a nondegenerate 2-elementary module is an orthogonal sum of Nikulin's generators of exponent one: the cyclic modules q_θ^{(2)}(2) on ℤ/2 with θ odd, whose quadratic form takes the value θ/4 on the generator, and the rank-two modules u^{(2)}(2) and v^{(2)}(2) on (ℤ/2)², whose quadratic forms take values in ½ℤ/ℤ.

Reading off the Gauss-sum invariants of the summands, ±1 for each q_θ^{(2)}(2), 0 for u^{(2)}(2) and 4 for v^{(2)}(2), constrains the Gauss-sum invariant sign q ∈ ℤ/8 of a nondegenerate 2-elementary module of order 2^a:

• sign q ≡ a (mod 2);
• if q takes values in ½ℤ/ℤ, that is, no q_θ^{(2)}(2) occurs, then sign q ∈ {0, 4};
• if a = 1, then sign q = ±1;
• if a = 2 and sign q = 4, then q takes values in ½ℤ/ℤ.

Through Milgram's theorem these become conditions on the signatures of even lattices with 2-elementary discriminant group, the arithmetic half of Nikulin's Theorem 3.6.2.

These three invariants are also complete: two nondegenerate 2-elementary modules are isometric exactly when their orders, Gauss signs and ½ℤ/ℤ-valuedness agree. Indeed their polar pairings, read over 𝔽₂, are classified by dimension and alternation. Nikulin's comparison theorem then recovers the quadratic form from the pairing and the Gauss sign.

Main results

• TauCeti.FiniteBilinearModule.nonempty_isometry_iff_of_two_nsmul_eq_zero: elementary two-group pairings are classified by their order and alternation type.
• TauCeti.FiniteQuadraticModule.nonempty_isometry_iff_of_two_nsmul_eq_zero: complete classification by order, Gauss sign and ½ℤ/ℤ-valuedness.
• TauCeti.FiniteQuadraticModule.exists_isometry_prod_pi_of_two_nsmul_eq_zero: a nondegenerate 2-elementary module is an orthogonal sum of copies of q_θ^{(2)}(2), u^{(2)}(2) and v^{(2)}(2).
• TauCeti.FiniteQuadraticModule.exists_gaussSign_eq_add_two_mul_of_two_nsmul_eq_zero: the parity of the Gauss-sum invariant.
• TauCeti.FiniteQuadraticModule.exists_gaussSign_eq_four_mul_of_quadratic_add_self_eq_zero: the Gauss-sum invariant of a nondegenerate module with values in ½ℤ/ℤ is 0 or 4.
• TauCeti.FiniteQuadraticModule.gaussSign_eq_one_or_eq_neg_one_of_natCard_eq_two: the Gauss-sum invariant of a nondegenerate module of order two is ±1.
• TauCeti.FiniteQuadraticModule.quadratic_add_self_eq_zero_of_gaussSign_eq_four: a nondegenerate 2-elementary module of order four with invariant 4 takes values in ½ℤ/ℤ.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Propositions 1.8.1 and 1.11.2, Theorem 1.11.3, and §3.6 for 2-elementary forms.

theorem TauCeti.FiniteBilinearModule.nonempty_isometry_iff_of_two_nsmul_eq_zero {A : FiniteBilinearModule} {B : FiniteBilinearModule} (hA : A.IsNondegenerate) (hB : B.IsNondegenerate) (h2A : ∀ (x : A.carrier), 2 • x = 0) (h2B : ∀ (x : B.carrier), 2 • x = 0) : Nonempty (A.Isometry B) ↔ Nat.card A.carrier = Nat.card B.carrier ∧ ((∀ (x : A.carrier), (A.pairing x) x = 0) ↔ ∀ (y : B.carrier), (B.pairing y) y = 0)

Nondegenerate pairings on elementary abelian two-groups are classified by their order and whether every self-pairing vanishes. This includes the trivial group.

The decomposition

theorem TauCeti.FiniteQuadraticModule.exists_isometry_prod_pi_of_two_nsmul_eq_zero (A : FiniteQuadraticModule) (hA : A.IsNondegenerate) (h2 : ∀ (x : A.carrier), 2 • x = 0) : ∃ (b : ℕ) (η : Fin b → ℤ) (c : ℕ) (d : ℕ), (∀ (i : Fin b), Odd (η i)) ∧ Nonempty (((pi fun (i : Fin b) => dyadicCyclic 1 (η i)).prod ((pi fun (x : Fin c) => dyadicU 1).prod (pi fun (x : Fin d) => dyadicV 1))).Isometry A)

A nondegenerate 2-elementary module is an orthogonal sum of generators of exponent one: of cyclic modules q_θ^{(2)}(2) with θ odd, and of copies of u^{(2)}(2) and v^{(2)}(2). This is the generator decomposition exists_isometry_prod_pi_generators in which 2 kills every summand.

Numerical invariants

theorem TauCeti.FiniteQuadraticModule.exists_gaussSign_eq_add_two_mul_of_two_nsmul_eq_zero {A : FiniteQuadraticModule} (hA : A.IsNondegenerate) (h2 : ∀ (x : A.carrier), 2 • x = 0) {a : ℕ} (ha : Nat.card A.carrier = 2 ^ a) : ∃ (k : ZMod 8), A.gaussSign = ↑a + 2 * k

The Gauss-sum invariant of a nondegenerate 2-elementary module of order 2^a has the parity of a: each cyclic summand q_θ^{(2)}(2) contributes ±1, and each rank-two summand contributes 0 or 4 while adding 2 to a.

theorem TauCeti.FiniteQuadraticModule.exists_gaussSign_eq_four_mul_of_quadratic_add_self_eq_zero {A : FiniteQuadraticModule} (hA : A.IsNondegenerate) (hq : ∀ (x : A.carrier), A.quadratic x + A.quadratic x = 0) : ∃ (k : ZMod 8), A.gaussSign = 4 * k

A nondegenerate module whose quadratic form takes values in ½ℤ/ℤ has Gauss-sum invariant 0 or 4: it is an orthogonal sum of copies of u^{(2)}(2) and v^{(2)}(2).

theorem TauCeti.FiniteQuadraticModule.gaussSign_eq_one_or_eq_neg_one_of_natCard_eq_two {A : FiniteQuadraticModule} (hA : A.IsNondegenerate) (hcard : Nat.card A.carrier = 2) : A.gaussSign = 1 ∨ A.gaussSign = -1

A nondegenerate module of order two has Gauss-sum invariant ±1: it is q_θ^{(2)}(2) for an odd θ.

theorem TauCeti.FiniteQuadraticModule.quadratic_add_self_eq_zero_of_gaussSign_eq_four {A : FiniteQuadraticModule} (hA : A.IsNondegenerate) (h2 : ∀ (x : A.carrier), 2 • x = 0) (hcard : Nat.card A.carrier = 4) (hsign : A.gaussSign = 4) (x : A.carrier) : A.quadratic x + A.quadratic x = 0

A nondegenerate 2-elementary module of order four with Gauss-sum invariant 4 takes values in ½ℤ/ℤ: two cyclic summands q_θ^{(2)}(2) would give an invariant in {-2, 0, 2}, so it is v^{(2)}(2).

Complete isometry invariants

theorem TauCeti.FiniteQuadraticModule.nonempty_isometry_iff_of_two_nsmul_eq_zero {A : FiniteQuadraticModule} {B : FiniteQuadraticModule} (hA : A.IsNondegenerate) (hB : B.IsNondegenerate) (h2A : ∀ (x : A.carrier), 2 • x = 0) (h2B : ∀ (x : B.carrier), 2 • x = 0) : Nonempty (A.Isometry B) ↔ Nat.card A.carrier = Nat.card B.carrier ∧ A.gaussSign = B.gaussSign ∧ ((∀ (x : A.carrier), A.quadratic x + A.quadratic x = 0) ↔ ∀ (y : B.carrier), B.quadratic y + B.quadratic y = 0)

Nondegenerate 2-elementary finite quadratic modules are classified by their order, their Gauss-sum invariant, and whether the quadratic form takes values in ½ℤ/ℤ. The last invariant is Nikulin's δ = 0 condition.