Odd unimodular forms over `ℤ_[2]` #

A symmetric bilinear form over ℤ_[2] is odd unimodular when its Gram determinant is a unit and it represents a unit. Such a form has an orthogonal basis whose self-pairings are units (LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_of_exists_isUnit_apply_self). It has two invariants besides its rank: the square class of its determinant, and its oddity, the self-pairing of a characteristic vector modulo 8 (LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_sub_apply_self), which is also the trace modulo 8 of any unit diagonal Gram matrix. This file proves that the rank, the determinant square class and the oddity classify odd unimodular forms over ℤ_[2]. Together with LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_of_even for even forms, this classifies the unimodular forms over ℤ_[2]. The forms ⟨1, 1⟩ and ⟨3, 3⟩ show that the oddity cannot be dropped (TauCeti.not_equivalent_toBilin'_diagonal_one_one_three_three_padicInt_two).

Main results #

LinearMap.BilinForm.exists_isUnit_apply_self_of_not_forall_two_dvd: a form over ℤ_[2] that is not even represents a unit.
LinearMap.BilinForm.iIsOrtho.exists_basis_iIsOrtho_apply_self_eq: a form with a unit diagonal orthogonal basis has an orthogonal basis realizing any unit diagonal with the same determinant square class and oddity.
LinearMap.BilinForm.iIsOrtho.equivalent_iff_isSquare_prod_mul_prod_and_eight_dvd: two forms with unit diagonal orthogonal bases of the same size are isometric exactly when their diagonals have the same product up to a square and the same sum modulo 8.
LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_and_eight_dvd_of_odd: odd unimodular forms of the same rank are isometric exactly when the product of their Gram determinants is a square and characteristic vectors have the same self-pairing modulo 8.

Implementation notes #

A unit of ℤ_[2] is a square exactly when it is 1 modulo 8, so a diagonal entry matters only through its residue among 1, 3, 5, 7. If b is an orthogonal basis with self-pairings dᵢ, then b i represents dᵢ, and b i + 2 b k represents dᵢ + 4 dₖ ≡ 5 dᵢ and is orthogonal to -2 dₖ b i + dᵢ b k. These vectors never change how many diagonal entries are 3 modulo 4. When d₀, d₁, d₂ are all 1 or all 3 modulo 4, the vectors b₀ + b₁ + b₂ and b₀ + b₁ + b₂ + 2 b₃ represent units of the other kind; the invariants guarantee that a fourth basis vector exists whenever this move is needed (ZMod.four_le_of_forall_eq_or_eq). Given a target diagonal v with the same determinant class and oddity, one of these vectors represents some vⱼ up to a unit square and is orthogonal to a vector with unit self-pairing, so it splits off an odd unimodular complement, and induction on the rank applies.

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.

Realizing a prescribed diagonal #

source

theorem LinearMap.BilinForm.iIsOrtho.exists_basis_iIsOrtho_apply_self_eq {M : Type u_1} [AddCommGroup M] [Module ℤ_[2] M] {B : LinearMap.BilinForm ℤ_[2] M} {n : ℕ} {b : Module.Basis (Fin n) ℤ_[2] M} (hb : B.iIsOrtho ⇑b) (hbu : ∀ (i : Fin n), IsUnit ((B (b i)) (b i))) {v : Fin n → ℤ_[2]} (hv : ∀ (i : Fin n), IsUnit (v i)) (hsq : IsSquare ((∏ i : Fin n, (B (b i)) (b i)) * ∏ i : Fin n, v i)) (h8 : 8 ∣ ∑ i : Fin n, v i - ∑ i : Fin n, (B (b i)) (b i)) :

∃ (c : Module.Basis (Fin n) ℤ_[2] M), B.iIsOrtho ⇑c ∧ ∀ (i : Fin n), (B (c i)) (c i) = v i

Realizing a prescribed diagonal. Let B be a bilinear form over ℤ_[2] with an orthogonal basis b of size n whose self-pairings are units. If v is a family of n units whose product differs from ∏ i, B (b i) (b i) by a square and whose sum agrees with ∑ i, B (b i) (b i) modulo 8, then B has an orthogonal basis with self-pairings exactly v.

source

theorem LinearMap.BilinForm.iIsOrtho.equivalent_iff_isSquare_prod_mul_prod_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} {n : ℕ} {b : Module.Basis (Fin n) ℤ_[2] M} {c : Module.Basis (Fin n) ℤ_[2] N} (hb : B.iIsOrtho ⇑b) (hc : C.iIsOrtho ⇑c) (hbu : ∀ (i : Fin n), IsUnit ((B (b i)) (b i))) (hcu : ∀ (i : Fin n), IsUnit ((C (c i)) (c i))) :

B.Equivalent C ↔ IsSquare ((∏ i : Fin n, (B (b i)) (b i)) * ∏ i : Fin n, (C (c i)) (c i)) ∧ 8 ∣ ∑ i : Fin n, (C (c i)) (c i) - ∑ i : Fin n, (B (b i)) (b i)

Classification of forms with unit diagonal orthogonal bases over ℤ_[2]. Let B and C have orthogonal bases b and c of the same size whose self-pairings are units. Then B and C are isometric exactly when the products of their self-pairings differ by a square and their sums agree modulo 8.