Characteristic vectors of a localized lattice #
A characteristic vector w of an integral lattice L satisfies B(x, x) ≡ B(x, w) modulo 2
for every x ∈ L. At the dyadic prime this congruence persists after localization: 1 ⊗ w is a
characteristic vector of the integral form on ℤ_[2] ⊗[ℤ] L. Since squaring is the identity
modulo 2 in ℤ_[2], it suffices to test the characteristic condition on a basis, and there it
is the integral congruence cast into ℤ_[2].
Main results #
TauCeti.IntegralLattice.IsCharacteristicVector.isCharacteristic_localIntegralForm: a characteristic vector of a lattice is characteristic for its dyadic localization.
References #
- J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 15, §7.
theorem
TauCeti.IntegralLattice.IsCharacteristicVector.isCharacteristic_localIntegralForm
{V : Type u_1}
[AddCommGroup V]
[Module ℚ V]
{L : IntegralLattice V}
{w : ↥L.carrier}
(hw : L.IsCharacteristicVector w)
:
(L.localIntegralForm 2).IsCharacteristic (1 ⊗ₜ[ℤ] w)
Integral characteristic vectors stay characteristic at 2. If w is a characteristic
vector of L, then 1 ⊗ w is a characteristic vector of the dyadic localization of L.