Unimodular forms over ℤ_[2]

A symmetric bilinear form over ℤ_[2] with unit Gram determinant is either even, when 2 divides every self-pairing B x x (type II), or odd, when some B x x is a unit (type I). Its oddity is the self-pairing of a characteristic vector modulo 8, which is well defined (LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_sub_apply_self) and is 0 for even forms (LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_of_forall_two_dvd).

This file proves that the rank, the type, the determinant square class and the oddity classify unimodular forms over ℤ_[2]. It assembles the even classification LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_of_even and the odd one LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_and_eight_dvd_of_odd; the type is an isometry invariant by LinearMap.BilinForm.Equivalent.forall_two_dvd_apply_self_iff. The type is not determined by the other three: the hyperbolic plane !![0, 1; 1, 0] and the diagonal form ⟨1, -1⟩ both have rank two, determinant -1 and oddity 0, and only the second represents a unit.

Main results

• LinearMap.BilinForm.IsSymm.equivalent_iff_two_dvd_iff_and_isSquare_det_mul_det_and_eight_dvd: two unimodular forms of the same rank over ℤ_[2] are isometric exactly when they have the same type, the product of their Gram determinants is a square, and their characteristic vectors have the same self-pairing modulo 8.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §93.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8, §4.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 15, §7.

theorem LinearMap.BilinForm.IsSymm.equivalent_iff_two_dvd_iff_and_isSquare_det_mul_det_and_eight_dvd {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℤ_[2] M] [AddCommGroup N] [Module ℤ_[2] N] {B : LinearMap.BilinForm ℤ_[2] M} {C : LinearMap.BilinForm ℤ_[2] N} (hB : B.IsSymm) (hC : C.IsSymm) {n : ℕ} (b : Module.Basis (Fin n) ℤ_[2] M) (c : Module.Basis (Fin n) ℤ_[2] N) (hBdet : IsUnit ((toMatrix b) B).det) (hCdet : IsUnit ((toMatrix c) C).det) {w : M} {w' : N} (hw : B.IsCharacteristic w) (hw' : C.IsCharacteristic w') : B.Equivalent C ↔ ((∀ (x : M), 2 ∣ (B x) x) ↔ ∀ (y : N), 2 ∣ (C y) y) ∧ IsSquare (((toMatrix b) B).det * ((toMatrix c) C).det) ∧ 8 ∣ (C w') w' - (B w) w

Classification of unimodular forms over ℤ_[2]. Let B and C be symmetric forms over ℤ_[2] with unit Gram determinants in bases of the same size, and let w and w' be characteristic vectors for B and C. Then B and C are isometric exactly when

• B is even if and only if C is even,
• the product of their Gram determinants is a square, and
• B w w ≡ C w' w' modulo 8, that is, their oddities agree.