Documentation

TauCeti.NumberTheory.IntegralLattice.Dyadic.Unimodular

Lattices unimodular at 2 #

A lattice whose determinant is a unit at 2 has a unimodular dyadic localization. Over ℤ_[2] such forms are classified by their rank, their type (even or odd), their determinant square class and their oddity, the norm of a characteristic vector modulo 8 (LinearMap.BilinForm.IsSymm.equivalent_iff_two_dvd_iff_and_isSquare_det_mul_det_and_eight_dvd). This file transfers that classification to lattices: evenness of a lattice is evenness of its dyadic localization (TauCeti.IntegralLattice.isEven_iff_forall_two_dvd_localIntegralForm_apply_self), and characteristic vectors of the lattice stay characteristic after localization (TauCeti.IntegralLattice.IsCharacteristicVector.isCharacteristic_localIntegralForm), so the invariants can be read off the lattice itself. For even lattices the oddity is automatically 0, and the localizations are classified by rank and determinant square class, as at odd primes (TauCeti.IntegralLattice.localIntegralForm_equivalent_iff). The oddity cannot be dropped: the lattices ⟨1, 1⟩ and ⟨3, 3⟩ are odd, with the same rank and square determinants, but only the first represents 1 over ℤ_[2]. Nor can the type: the hyperbolic plane and ⟨1, -1⟩ have rank two, determinant -1 and oddity 0, but only the second is odd.

An even lattice unimodular at 2 has even rank and splits off a rank-two perfect summand orthogonally after localization.

Main results #

References #

source
theorem TauCeti.IntegralLattice.IsEven.even_finrank_of_isUnit_determinant {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (heven : L.IsEven) (hdet : IsUnit ↑L.determinant) :
Even (Module.finrank ℤ ↥L.carrier)

An even lattice of odd determinant has even rank. Its dyadic localization is a perfect pairing whose self-pairings are all divisible by 2, and such a form has even rank.

source
theorem TauCeti.IntegralLattice.exists_binary_isPerfPair_isCompl_orthogonal_localIntegralForm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hrank : 2 ≤ Module.finrank ℤ ↥L.carrier) (heven : L.IsEven) (hdet : IsUnit ↑L.determinant) :
∃ (S : Submodule ℤ_[2] (L.LocalCarrier 2)), Module.finrank ℤ_[2] ↥S = 2 ∧ LinearMap.IsPerfPair ((L.localIntegralForm 2).restrict S) ∧ IsCompl S ((L.localIntegralForm 2).orthogonal S)

An even lattice unimodular at 2 splits off a perfect binary summand. If the rank is at least two, the dyadic localization has a rank-two submodule carrying a perfect restriction of the local integral form and complementary to its orthogonal complement.

source
theorem TauCeti.IntegralLattice.localIntegralForm_two_equivalent_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (hL : IsUnit ↑L.determinant) (hM : IsUnit ↑M.determinant) {w : L.LocalCarrier 2} {w' : M.LocalCarrier 2} (hw : (L.localIntegralForm 2).IsCharacteristic w) (hw' : (M.localIntegralForm 2).IsCharacteristic w') :
(L.localIntegralForm 2).Equivalent (M.localIntegralForm 2) ↔ Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier ∧ (L.IsEven ↔ M.IsEven) ∧ IsSquare (↑L.determinant * ↑M.determinant) ∧ 8 ∣ ((M.localIntegralForm 2) w') w' - ((L.localIntegralForm 2) w) w

Classification of localizations unimodular at 2. Let L and M be lattices whose determinants are units at 2, and let w and w' be characteristic vectors of their dyadic localizations. The localizations are integrally isometric exactly when the ranks agree, L is even if and only if M is, the product of the determinants is a square in ℤ_[2], and B(w, w) ≡ B(w', w') modulo 8, that is, the oddities agree. The lattices need not be globally unimodular.

source
theorem TauCeti.IntegralLattice.localIntegralForm_two_equivalent_iff_of_isCharacteristicVector {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (hL : IsUnit ↑L.determinant) (hM : IsUnit ↑M.determinant) {w : ↥L.carrier} {w' : ↥M.carrier} (hw : L.IsCharacteristicVector w) (hw' : M.IsCharacteristicVector w') :
(L.localIntegralForm 2).Equivalent (M.localIntegralForm 2) ↔ Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier ∧ (L.IsEven ↔ M.IsEven) ∧ IsSquare (↑L.determinant * ↑M.determinant) ∧ L.integralNorm w ≡ M.integralNorm w' [ZMOD 8]

Classification of localizations unimodular at 2, with integral characteristic vectors. If w and w' are characteristic vectors of L and M, whose determinants are units at 2, then the dyadic localizations are integrally isometric exactly when the ranks agree, L is even if and only if M is, the product of the determinants is a square in ℤ_[2], and the norms of w and w' agree modulo 8.

source
theorem TauCeti.IntegralLattice.localIntegralForm_two_equivalent_iff_of_isEven {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (hLeven : L.IsEven) (hMeven : M.IsEven) (hL : IsUnit ↑L.determinant) (hM : IsUnit ↑M.determinant) :
(L.localIntegralForm 2).Equivalent (M.localIntegralForm 2) ↔ Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier ∧ IsSquare (↑L.determinant * ↑M.determinant)

Classification of even localizations unimodular at 2. Even lattices whose determinants are units at 2 have integrally isometric dyadic localizations exactly when their ranks agree and the product of their determinants is a square in ℤ_[2]. The lattices need not be globally unimodular.