Lattices in a rational vector space are determined by their localizations

Let V be a vector space over ℚ and N a ℤ-submodule of V. At a prime p its localization is the ℤ_p-submodule N_p of the completed space V_p = ℚ_p ⊗[ℚ] V spanned by the vectors 1 ⊗ v, v ∈ N. When N is a full lattice, that is, finitely generated and spanning V, then N_p is a full ℤ_p-lattice in V_p.

This file proves the local–global principle for lattices: a full lattice is determined by its localizations, and any family of local lattices which is the family of localizations of a fixed lattice at almost every prime is the family of localizations of exactly one lattice.

• A vector v ∈ V lies in the full lattice N exactly when 1 ⊗ v ∈ N_p at every prime p (Submodule.mem_iff_forall_one_tmul_mem_padicLocalization). In the rational basis of a basis of N, both sides say that the coordinates of v are integers, respectively p-adic integers at every prime. In particular M ≤ N exactly when M_p ≤ N_p for every p.
• Two full lattices have the same localization at almost every prime (Submodule.eventually_padicLocalization_eq): a nonzero integer d multiplies each into the other, and d is a p-adic unit at almost every prime.
• Given a full lattice N and full ℤ_p-lattices X_p ⊆ V_p with X_p = N_p for almost every p, the lattice M = {v ∈ V | 1 ⊗ v ∈ X_p for every p} is the unique full lattice with M_p = X_p at every prime (Submodule.existsUnique_isLattice_padicLocalization_eq).

The last statement is what turns a finite adelic point g = (g_p) of the orthogonal group of V into a lattice g L with (g L)_p = g_p L_p, on which the description of the classes in the genus of an integral lattice by finite adelic double cosets rests.

Main definitions

• Submodule.padicLocalization: the localization N_p ⊆ ℚ_p ⊗[ℚ] V of a ℤ-submodule N.

Main results

• Submodule.padicLocalization_le_iff: N_p is the least ℤ_p-submodule containing every 1 ⊗ v, v ∈ N.
• Submodule.isLattice_padicLocalization: the localization of a full lattice is a full ℤ_p-lattice.
• Submodule.mem_padicLocalization_iff_repr_mem: in the scalar extension of the rational basis of a basis of N, the localization N_p consists of the vectors with p-adic integral coordinates.
• Submodule.mem_iff_forall_one_tmul_mem_padicLocalization, Submodule.le_iff_forall_padicLocalization_le, Submodule.eq_iff_forall_padicLocalization_eq: a full lattice is determined by its localizations.
• Submodule.eventually_padicLocalization_eq: two full lattices have equal localizations at almost every prime.
• Submodule.exists_eq_one_tmul_add_pow_smul: N is dense in N_p.
• Submodule.IsLattice.exists_forall_pow_smul_mem: a power of p multiplies a finitely generated ℤ_p-submodule into a full ℤ_p-lattice.
• Submodule.existsUnique_isLattice_padicLocalization_eq: a family of full local lattices agreeing almost everywhere with the localizations of a full lattice is the family of localizations of a unique full lattice.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §81E, Theorems 81:14 and 81:18.
• M. Kneser, Quadratische Formen (2002), §21.

noncomputable def Submodule.padicLocalization {V : Type u_1} [AddCommGroup V] [Module ℚ V] (N : Submodule ℤ V) (p : ℕ) [Fact (Nat.Prime p)] : Submodule ℤ_[p] (TensorProduct ℚ ℚ_[p] V)

The localization N_p of a ℤ-submodule N of a rational vector space V at a prime p: the ℤ_p-submodule of the completed space ℚ_p ⊗[ℚ] V spanned by the vectors 1 ⊗ v with v ∈ N.

theorem Submodule.padicLocalization_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] (N : Submodule ℤ V) (p : ℕ) [Fact (Nat.Prime p)] : N.padicLocalization p = span ℤ_[p] ((fun (v : V) => 1 ⊗ₜ[ℚ] v) '' ↑N)

The localization N_p is the ℤ_p-span of the vectors 1 ⊗ v with v ∈ N.

theorem Submodule.one_tmul_mem_padicLocalization {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} {p : ℕ} [Fact (Nat.Prime p)] {v : V} (hv : v ∈ N) : 1 ⊗ₜ[ℚ] v ∈ N.padicLocalization p

For v ∈ N, the vector 1 ⊗ v lies in the localization N_p.

theorem Submodule.padicLocalization_le_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} {p : ℕ} [Fact (Nat.Prime p)] {X : Submodule ℤ_[p] (TensorProduct ℚ ℚ_[p] V)} : N.padicLocalization p ≤ X ↔ ∀ v ∈ N, 1 ⊗ₜ[ℚ] v ∈ X

Universal property of the localization. N_p is contained in a ℤ_p-submodule X of ℚ_p ⊗[ℚ] V exactly when X contains 1 ⊗ v for every v ∈ N.

theorem Submodule.padicLocalization_mono {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} {p : ℕ} [Fact (Nat.Prime p)] {M : Submodule ℤ V} (h : M ≤ N) : M.padicLocalization p ≤ N.padicLocalization p

Localization is monotone: M ≤ N gives M_p ≤ N_p.

theorem Submodule.padicLocalization_span {V : Type u_1} [AddCommGroup V] [Module ℚ V] {p : ℕ} [Fact (Nat.Prime p)] (s : Set V) : (span ℤ s).padicLocalization p = span ℤ_[p] ((fun (v : V) => 1 ⊗ₜ[ℚ] v) '' s)

The localization of the span of a set s is the ℤ_p-span of the vectors 1 ⊗ v, v ∈ s.

instance Submodule.isLattice_padicLocalization {V : Type u_1} [AddCommGroup V] [Module ℚ V] (N : Submodule ℤ V) (p : ℕ) [Fact (Nat.Prime p)] [IsLattice ℚ N] : IsLattice ℚ_[p] (N.padicLocalization p)

The localization of a full lattice is a full ℤ_p-lattice in ℚ_p ⊗[ℚ] V.

theorem Submodule.padicLocalization_eq_span_range {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} {p : ℕ} [Fact (Nat.Prime p)] [IsLattice ℚ N] {ι : Type u_2} (e : Module.Basis ι ℤ ↥N) : N.padicLocalization p = span ℤ_[p] (Set.range ⇑(Module.Basis.baseChange ℚ_[p] (Module.Basis.extendOfIsLattice ℚ e)))

The localization of a full lattice N is the ℤ_p-span of the scalar extension of the rational basis of a basis of N.

theorem Submodule.mem_padicLocalization_iff_repr_mem {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} {p : ℕ} [Fact (Nat.Prime p)] [IsLattice ℚ N] {ι : Type u_2} (e : Module.Basis ι ℤ ↥N) (x : TensorProduct ℚ ℚ_[p] V) : x ∈ N.padicLocalization p ↔ ∀ (i : ι), ‖((Module.Basis.baseChange ℚ_[p] (Module.Basis.extendOfIsLattice ℚ e)).repr x) i‖ ≤ 1

The localization in coordinates. In the scalar extension of the rational basis of a basis e of a full lattice N, the localization N_p consists of the vectors whose coordinates are p-adic integers.

theorem Submodule.mem_iff_forall_one_tmul_mem_padicLocalization {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [IsLattice ℚ N] (v : V) : v ∈ N ↔ ∀ (p : Nat.Primes), 1 ⊗ₜ[ℚ] v ∈ N.padicLocalization ↑p

A full lattice is determined by its localizations. A vector v lies in a full lattice N exactly when 1 ⊗ v lies in the localization N_p at every prime p.

theorem Submodule.le_iff_forall_padicLocalization_le {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [IsLattice ℚ N] (M : Submodule ℤ V) : M ≤ N ↔ ∀ (p : Nat.Primes), M.padicLocalization ↑p ≤ N.padicLocalization ↑p

A submodule M is contained in a full lattice N exactly when every localization of M is contained in the corresponding localization of N.

theorem Submodule.eq_iff_forall_padicLocalization_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [IsLattice ℚ N] (M : Submodule ℤ V) [IsLattice ℚ M] : M = N ↔ ∀ (p : Nat.Primes), M.padicLocalization ↑p = N.padicLocalization ↑p

Two full lattices are equal exactly when their localizations are equal at every prime.

theorem Submodule.eventually_padicLocalization_le {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [IsLattice ℚ N] {M : Submodule ℤ V} (hM : M.FG) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, M.padicLocalization ↑p ≤ N.padicLocalization ↑p

If M is finitely generated and N is a full lattice, then M_p ≤ N_p at almost every prime: a nonzero integer r multiplies M into N, and r is a p-adic unit at almost every prime.

theorem Submodule.eventually_padicLocalization_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [IsLattice ℚ N] (M : Submodule ℤ V) [IsLattice ℚ M] : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, M.padicLocalization ↑p = N.padicLocalization ↑p

Two full lattices have the same localization at almost every prime.

theorem Submodule.exists_eq_one_tmul_add_pow_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} {p : ℕ} [Fact (Nat.Prime p)] {x : TensorProduct ℚ ℚ_[p] V} (hx : x ∈ N.padicLocalization p) (m : ℕ) : ∃ w ∈ N, ∃ t ∈ N.padicLocalization p, x = 1 ⊗ₜ[ℚ] w + ↑p ^ m • t

N is dense in its localization. Every vector of N_p is congruent to a vector 1 ⊗ w, w ∈ N, modulo p ^ m • N_p.

theorem Submodule.IsLattice.exists_forall_pow_smul_mem (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_2} [AddCommGroup W] [Module ℚ_[p] W] [Module ℤ_[p] W] [IsScalarTower ℤ_[p] ℚ_[p] W] (Z : Submodule ℤ_[p] W) [IsLattice ℚ_[p] Z] {Y : Submodule ℤ_[p] W} (hY : Y.FG) : ∃ (k : ℕ), ∀ x ∈ Y, ↑p ^ k • x ∈ Z

Commensurability over ℤ_p. A power of p multiplies a finitely generated ℤ_p-submodule of a ℚ_p-vector space into a full ℤ_p-lattice.

theorem Submodule.existsUnique_isLattice_padicLocalization_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [IsLattice ℚ N] (X : (p : Nat.Primes) → Submodule ℤ_[↑p] (TensorProduct ℚ ℚ_[↑p] V)) [∀ (p : Nat.Primes), IsLattice ℚ_[↑p] (X p)] (hX : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, X p = N.padicLocalization ↑p) : ∃! M : Submodule ℤ V, IsLattice ℚ M ∧ ∀ (p : Nat.Primes), M.padicLocalization ↑p = X p

The local–global correspondence for lattices. Let N be a full lattice in V and, for every prime p, let X p be a full ℤ_p-lattice in ℚ_p ⊗[ℚ] V, with X p = N_p at almost every prime. Then exactly one full lattice M has M_p = X p at every prime.