Odd unimodular forms over local rings

A symmetric unimodular form over a local ring is odd when it represents a unit. Such a form has an orthogonal basis whose self-pairings are all units. This is the diagonalization step for odd unimodular lattices over ℤ₂.

The key point in residue characteristic two is that splitting off an arbitrary unit-norm vector can leave an even orthogonal complement. When that happens, a unit off-diagonal entry in the complement lets us replace the vector by one whose orthogonal complement again represents a unit. Induction can therefore continue without assuming that two is invertible.

Main results

• LinearMap.BilinForm.IsSymm.exists_orthogonal_isUnit_pair: an odd unimodular form of rank at least two represents units on two orthogonal vectors.
• LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_of_exists_isUnit_apply_self: an odd unimodular form has a unit-diagonal orthogonal basis.
• LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_orthogonal_span_singleton: so does the orthogonal complement of a unit vector, once that complement represents a unit.
• LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_of_isUnit_det: when 2 is a unit, every symmetric form with unit Gram determinant has a unit-diagonal orthogonal basis, since a unit Gram entry gives a unit self-pairing.
• LinearMap.BilinForm.IsSymm.exists_equivalent_weightedSumSquares_of_isUnit_det: such a form is isometric to a unit diagonal quadratic form, with a determinant change-of-basis equation.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §93.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8.

theorem LinearMap.BilinForm.IsSymm.exists_orthogonal_isUnit_pair {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) {n : ℕ} (b : Module.Basis (Fin (n + 2)) R M) (hdet : IsUnit ((toMatrix b) B).det) (hodd : ∃ (x : M), IsUnit ((B x) x)) : ∃ (x : M) (y : M), IsUnit ((B x) x) ∧ IsUnit ((B y) y) ∧ (B x) y = 0

Two orthogonal unit values in an odd unimodular form. A symmetric form of rank at least two whose Gram determinant is a unit and which represents a unit has two orthogonal vectors with unit self-pairings. The result needs no inverse of two.

theorem LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_of_exists_isUnit_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) {n : ℕ} (b : Module.Basis (Fin n) R M) (hdet : IsUnit ((toMatrix b) B).det) (hodd : ∃ (x : M), IsUnit ((B x) x)) : ∃ (c : Module.Basis (Fin n) R M), B.iIsOrtho ⇑c ∧ ∀ (i : Fin n), IsUnit ((B (c i)) (c i))

Odd unimodular forms are diagonalizable over a local ring. If a symmetric form has a unit Gram determinant and represents a unit, then it has an orthogonal basis all of whose self-pairings are units.

This is the odd counterpart of binary-block decomposition for even forms. In particular it applies to type-I unimodular Jordan constituents over ℤ₂.

theorem LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_orthogonal_span_singleton {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) {n : ℕ} (b : Module.Basis (Fin (n + 1)) R M) (hdet : IsUnit ((toMatrix b) B).det) {x y : M} (hx : IsUnit ((B x) x)) (hy : IsUnit ((B y) y)) (hxy : (B x) y = 0) : ∃ (t : Module.Basis (Fin n) R ↥(B.orthogonal (R ∙ x))), (B.restrict (B.orthogonal (R ∙ x))).iIsOrtho ⇑t ∧ ∀ (i : Fin n), IsUnit ((B ↑(t i)) ↑(t i))

The orthogonal complement of a unit vector in an odd unimodular form. Let B be a symmetric form whose Gram determinant in a basis of size n + 1 is a unit over a local ring. If x has unit self-pairing and is orthogonal to a vector y with unit self-pairing, then the orthogonal complement of x has an orthogonal basis of size n all of whose self-pairings are units.

Together with LinearMap.BilinForm.IsRefl.exists_orthogonal_basis_isUnit_apply_self_eq_cons, this extends x to a unit-diagonal orthogonal basis of the whole module.

theorem LinearMap.BilinForm.IsSymm.exists_orthogonal_basis_isUnit_of_isUnit_det {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) (h2 : IsUnit 2) {n : ℕ} (b : Module.Basis (Fin n) R M) (hdet : IsUnit ((toMatrix b) B).det) : ∃ (c : Module.Basis (Fin n) R M), B.iIsOrtho ⇑c ∧ ∀ (i : Fin n), IsUnit ((B (c i)) (c i))

A symmetric form with unit Gram determinant over a local ring with two invertible has an orthogonal basis with unit self-pairings. The input basis is arbitrary.

theorem LinearMap.BilinForm.IsSymm.exists_equivalent_weightedSumSquares_of_isUnit_det {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) (h2 : IsUnit 2) {n : ℕ} (b : Module.Basis (Fin n) R M) (hdet : IsUnit ((toMatrix b) B).det) : ∃ (w : Fin n → Rˣ), (BilinMap.toQuadraticMap B).Equivalent (QuadraticMap.weightedSumSquares R w) ∧ ∃ (d : R), ∏ i : Fin n, ↑(w i) = d ^ 2 * ((toMatrix b) B).det

A symmetric form with unit Gram determinant over a local ring with two invertible is isometric to a unit diagonal form. The product of its coefficients equals the original Gram determinant times the square of a change-of-basis determinant.