Binary decomposition of even unimodular forms

Over a local ring, a symmetric perfect pairing on a finite free module whose diagonal values are all nonunits is an orthogonal sum of binary perfect pairings. This includes even forms when two is not a unit. Each summand comes with a two-element basis, so this is a decomposition of the actual module, not just an equality of ranks. In particular its rank is even. The empty decomposition covers the zero module.

An isotropic vector pairing to 1 with a vector of even norm completes to a hyperbolic pair (LinearMap.BilinForm.IsSymm.exists_hyperbolic_of_apply_self_eq_zero).

These binary constituents are the inputs to the classification of even unimodular dyadic lattices. No inverse of two, domain hypothesis, or completeness assumption is used here.

The binary splitting step reuses LinearMap.BilinForm.IsSymm.exists_binary_isPerfPair_isCompl_orthogonal_of_dual_apply_eq_one from the local-ring API. The construction uses the unit-Gram criterion LinearMap.BilinForm.isModular_restrict_span_range and the perfect-restriction splitting theorem LinearMap.BilinForm.isCompl_orthogonal_of_restrict_bijective.

References

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

theorem LinearMap.BilinForm.IsSymm.exists_hyperbolic_of_apply_self_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) {u w : M} {d : R} (hu : (B u) u = 0) (huw : (B u) w = 1) (hw : (B w) w = 2 * d) : ∃ (e : M) (f : M), (B e) f = 1 ∧ (B e) e = 0 ∧ (B f) f = 0

An isotropic vector u with B u w = 1 completes to a hyperbolic pair when B w w is even: subtract d • u from w when B w w = 2 * d.

theorem LinearMap.BilinForm.IsSymm.exists_binary_orthogonal_decomposition {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) [IsPerfPair B] [Module.Free R M] [Module.Finite R M] (hB : B.IsSymm) (hdiag : ∀ (x : M), ¬IsUnit ((B x) x)) : ∃ (k : ℕ) (N : Fin k → Submodule R M), DirectSum.IsInternal N ∧ (∀ (i j : Fin k), i ≠ j → ∀ x ∈ N i, ∀ y ∈ N j, (B x) y = 0) ∧ ∀ (i : Fin k), Nonempty (Module.Basis (Fin 2) R ↥(N i)) ∧ IsPerfPair (B.restrict (N i))

A symmetric perfect pairing with nonunit diagonal values over a local ring is an internal orthogonal sum of binary perfect pairings. Each constituent has a two-element basis.

theorem LinearMap.BilinForm.IsSymm.even_finrank_of_isPerfPair {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) [IsPerfPair B] [Module.Free R M] [Module.Finite R M] (hB : B.IsSymm) (hdiag : ∀ (x : M), ¬IsUnit ((B x) x)) : Even (Module.finrank R M)

A symmetric perfect pairing with nonunit diagonal values on a finite free module over a local ring has even rank. In particular this holds for even forms when two is not a unit.