Classification of unimodular localizations at odd primes

When the signed determinants of two integral lattices are units at an odd prime, their integral localizations are isometric exactly when they have equal ranks and their determinants agree modulo squares in ℤ_p. Global unimodularity is unnecessary: the hypotheses concern the local determinants alone. The isometry preserves the actual integral forms on ℤ_p ⊗[ℤ] L.

The forward implication holds at every prime and without any determinant-unit hypothesis.

Main results

• TauCeti.IntegralLattice.isPerfPair_localIntegralForm_of_isUnit_determinant: the localized integral form is a perfect pairing when the determinant is a unit at p.
• TauCeti.IntegralLattice.localIntegralForm_equivalent_imp: integral local isometry preserves the rank and determinant square class at every prime.
• TauCeti.IntegralLattice.exists_determinant_eq_unit_sq_mul_of_localIntegralForm_equivalent: the signed determinants of integrally isometric localizations differ by a unit square.
• TauCeti.IntegralLattice.localIntegralForm_equivalent_iff: for local unit determinants at an odd prime, these invariants classify the integral local forms.
• TauCeti.IntegralLattice.localIntegralForm_equivalent_of_not_dvd: equal rank and signed determinant give integral local isometry outside the prime factors of twice the determinant.

References

• O. T. O'Meara, Introduction to Quadratic Forms, 92:1--92:2.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8.

theorem TauCeti.IntegralLattice.isPerfPair_localIntegralForm_of_isUnit_determinant {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (hdet : IsUnit ↑L.determinant) : LinearMap.IsPerfPair (L.localIntegralForm p)

A lattice whose determinant is a unit at p has a unimodular localization. The localized integral form is then a perfect pairing on ℤ_p ⊗[ℤ] L.

theorem TauCeti.IntegralLattice.localIntegralForm_equivalent_imp {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (h : (L.localIntegralForm p).Equivalent (M.localIntegralForm p)) : Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier ∧ IsSquare (↑L.determinant * ↑M.determinant)

Integrally isometric localizations have equal ranks and determinant products that are squares, at every prime and without any determinant-unit hypothesis.

theorem TauCeti.IntegralLattice.exists_determinant_eq_unit_sq_mul_of_localIntegralForm_equivalent {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (h : (L.localIntegralForm p).Equivalent (M.localIntegralForm p)) : ∃ (u : ℤ_[p]ˣ), ↑L.determinant = ↑u ^ 2 * ↑M.determinant

Integrally isometric localizations have signed determinants differing by the square of a p-adic unit, at every prime and without any determinant-unit hypothesis.

theorem TauCeti.IntegralLattice.localIntegralForm_equivalent_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) (hL : IsUnit ↑L.determinant) (hM : IsUnit ↑M.determinant) : (L.localIntegralForm p).Equivalent (M.localIntegralForm p) ↔ Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier ∧ IsSquare (↑L.determinant * ↑M.determinant)

Localizations unimodular at an odd prime are integrally isometric exactly when their ranks and determinant square classes agree. The input lattices need not be globally unimodular.

theorem TauCeti.IntegralLattice.localIntegralForm_equivalent_of_not_dvd {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) {p : ℕ} [Fact (Nat.Prime p)] (hrank : Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier) (hdet : L.determinant = M.determinant) (hp : ¬p ∣ 2 * L.determinant.natAbs) : (L.localIntegralForm p).Equivalent (M.localIntegralForm p)

Lattices of equal rank and signed determinant have isometric integral localizations at every prime not dividing twice the absolute determinant.