Orthogonal splitting of integral lattices

A sublattice with perfect restricted pairing is complementary to its orthogonal complement. A vector of unit norm spans such a summand. These specialize the corresponding results for symmetric bilinear forms over commutative rings. The lattice theorems expose these results on IntegralLattice without requiring callers to provide the symmetry of integralForm separately. The orthogonal complement of a vector with nonzero pairing functional has integral rank one less than the lattice.

The unimodular splitting theorem is from O. T. O'Meara, Introduction to Quadratic Forms, §82.

theorem TauCeti.IntegralLattice.isCompl_orthogonal_of_restrict_bijective {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (h : Function.Bijective ⇑(L.integralForm.restrict S)) : IsCompl S (L.integralForm.orthogonal S)

A sublattice with perfect restricted integral pairing is complementary to its orthogonal complement.

theorem TauCeti.IntegralLattice.isCompl_span_singleton_orthogonal_of_isUnit {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : IsUnit ((L.integralForm x) x)) : IsCompl (ℤ ∙ x) (L.integralForm.orthogonal (ℤ ∙ x))

A vector of unit norm spans an orthogonal direct summand of an integral lattice.

theorem TauCeti.IntegralLattice.finrank_orthogonal_span_singleton_add_one {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : L.integralForm x ≠ 0) : Module.finrank ℤ ↥(L.integralForm.orthogonal (ℤ ∙ x)) + 1 = Module.finrank ℤ ↥L.carrier

The orthogonal complement of a vector with nonzero pairing functional has integral rank one less than the lattice, without any assumption on the radical of the ambient form.