Characteristic vectors in unimodular lattices

The norm of an integral lattice is additive modulo two. For a unimodular lattice its mod-two character is represented by pairing with a lattice vector. All such representatives form one coset of twice the carrier, so their norms agree modulo eight.

References

• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.

theorem TauCeti.IntegralLattice.IsUnimodular.exists_isCharacteristicVector {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) : ∃ (w : ↥L.carrier), L.IsCharacteristicVector w

Every unimodular integral lattice has a characteristic vector.

theorem TauCeti.IntegralLattice.IsUnimodular.exists_characteristicVector_sub_eq_two_smul {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) {w₁ w₂ : ↥L.carrier} (h₁ : L.IsCharacteristicVector w₁) (h₂ : L.IsCharacteristicVector w₂) : ∃ (v : ↥L.carrier), w₁ - w₂ = 2 • v

Two characteristic vectors of a unimodular lattice differ by twice a lattice vector.

theorem TauCeti.IntegralLattice.IsUnimodular.isCharacteristicVector_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) {w₀ : ↥L.carrier} (hw₀ : L.IsCharacteristicVector w₀) (w : ↥L.carrier) : L.IsCharacteristicVector w ↔ ∃ (v : ↥L.carrier), w = w₀ + 2 • v

The characteristic vectors of a unimodular lattice form a single coset of twice its carrier.

theorem TauCeti.IntegralLattice.IsUnimodular.characteristicVector_integralNorm_modEq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) {w₁ w₂ : ↥L.carrier} (h₁ : L.IsCharacteristicVector w₁) (h₂ : L.IsCharacteristicVector w₂) : L.integralNorm w₁ ≡ L.integralNorm w₂ [ZMOD 8]

Characteristic vectors of a unimodular lattice have the same norm modulo eight.