Localizing an integral lattice at a prime

Let L be an integral lattice in a rational vector space V, with rational form B, and let p be a prime. Two p-adic objects are attached to L, and they are kept apart:

• the integral localization L_p = ℤ_p ⊗[ℤ] L, with the base change B_{L,p} = L.integralForm.baseChange ℤ_p of the integral form on the carrier;
• the completed rational space V_p = ℚ_p ⊗[ℚ] V, with the base change B_{V,p} = B.baseChange ℚ_p of the rational form.

The integral object is where scale, norm, Jordan splittings and integral duality live; the rational object is where dimension, determinant square class and Hasse invariant live. This file builds the canonical ℤ_p-linear map L_p → V_p, a ⊗ x ↦ a ⊗ x, and proves that it is the bridge between them:

• it is injective, and it becomes an isomorphism after extending scalars from ℤ_p to ℚ_p (isBaseChange_localizationToCompletion), so its image is a full ℤ_p-lattice in V_p;
• the localized integral form is the restriction of the completed rational form along it (completedRationalForm_localizationToCompletion).

Nothing here inverts 2: bilinear-form base change needs no such hypothesis, so the construction applies at p = 2 exactly as at odd p. The Gram matrix of L_p in a base-changed basis is the image of the integral Gram matrix of L, and both local forms are nondegenerate exactly when B is.

An isometry of the integral localizations of two lattices extends to an isometry of their completed rational spaces, so integral local isometry implies rational local isometry (completedRationalForm_equivalent_of_localIntegralForm_equivalent). This is what carries the local data of the genus over to the rational quadratic spaces.

Main definitions

• TauCeti.IntegralLattice.LocalCarrier: the integral localization ℤ_p ⊗[ℤ] L.
• TauCeti.IntegralLattice.localIntegralForm: its base-changed integral form.
• TauCeti.IntegralLattice.completedRationalForm: the rational form base-changed to the completed rational space ℚ_p ⊗[ℚ] V.
• TauCeti.IntegralLattice.localizationToCompletion: the canonical map L_p → V_p.
• TauCeti.IntegralLattice.Isometry.localCarrierIsometry and TauCeti.IntegralLattice.Isometry.completedIsometry: an isometry L ≅ M induces isometries L_p ≅ M_p and V_p ≅ W_p.
• TauCeti.IntegralLattice.completedRationalFormIsometryEquiv: the scalar extension of the localized integral form to ℚ_p is the completed rational form.
• TauCeti.IntegralLattice.completedIsometryEquiv: an isometry L_p ≅ M_p of the localized integral forms extends to an isometry V_p ≅ W_p of the completed rational forms.

Main results

• TauCeti.IntegralLattice.isBaseChange_localizationToCompletion: V_p is the scalar extension of L_p from ℤ_p to ℚ_p along the canonical map.
• TauCeti.IntegralLattice.localizationToCompletion_injective: the canonical map is injective.
• TauCeti.IntegralLattice.span_range_localizationToCompletion: its image spans V_p over ℚ_p.
• TauCeti.IntegralLattice.range_localizationToCompletion: its image is the localization Submodule.padicLocalization of the carrier of L, the ℤ_p-span of the vectors 1 ⊗ x.
• TauCeti.IntegralLattice.mem_range_localizationToCompletion_iff: in the rational basis of a basis of L, its image consists of the vectors with p-adic integral coordinates.
• TauCeti.IntegralLattice.completedRationalForm_localizationToCompletion: the localized integral form is the restriction of the completed rational form.
• TauCeti.IntegralLattice.toMatrix_localIntegralForm: the Gram matrix of L_p is the image of the Gram matrix of L.
• TauCeti.IntegralLattice.det_toMatrix_localIntegralForm: its determinant in any base-changed carrier basis is the image of the lattice's signed determinant.
• TauCeti.IntegralLattice.nondegenerate_localIntegralForm_iff and TauCeti.IntegralLattice.nondegenerate_completedRationalForm_iff: both local forms are nondegenerate exactly when the rational form of L is.
• TauCeti.IntegralLattice.Isometry.localizationToCompletion_localCarrierIsometry: the canonical map is natural in isometries.
• TauCeti.IntegralLattice.completedRationalForm_equivalent_of_localIntegralForm_equivalent: isometric integral localizations have isometric completed rational spaces.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Chapter VIII, for lattices in a quadratic space over the fraction field of a Dedekind domain, applied here to ℤ_p ⊂ ℚ_p.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8, for integral forms over ℤ_p.

@[reducible, inline]

abbrev TauCeti.IntegralLattice.LocalCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : Type u

The integral localization ℤ_p ⊗[ℤ] L of the carrier of an integral lattice.

noncomputable def TauCeti.IntegralLattice.localIntegralForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : LinearMap.BilinForm ℤ_[p] (L.LocalCarrier p)

The integral form of an integral lattice, base-changed from ℤ to ℤ_p. This is built from the integral form on the carrier, not from the rational form on the ambient space.

theorem TauCeti.IntegralLattice.localIntegralForm_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : L.localIntegralForm p = LinearMap.BilinForm.baseChange ℤ_[p] L.integralForm

The localized integral form is the base change of the integral carrier form.

noncomputable def TauCeti.IntegralLattice.completedRationalForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : LinearMap.BilinForm ℚ_[p] (TensorProduct ℚ ℚ_[p] V)

The rational form of an integral lattice, base-changed from ℚ to ℚ_p.

theorem TauCeti.IntegralLattice.completedRationalForm_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : L.completedRationalForm p = LinearMap.BilinForm.baseChange ℚ_[p] L.form

The completed rational form is the base change of the ambient rational form.

@[simp]

theorem TauCeti.IntegralLattice.localIntegralForm_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ_[p]) (x y : ↥L.carrier) : ((L.localIntegralForm p) (a ⊗ₜ[ℤ] x)) (b ⊗ₜ[ℤ] y) = a * b * ↑((L.integralForm x) y)

The localized integral form on pure tensors.

@[simp]

theorem TauCeti.IntegralLattice.completedRationalForm_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (a b : ℚ_[p]) (x y : V) : ((L.completedRationalForm p) (a ⊗ₜ[ℚ] x)) (b ⊗ₜ[ℚ] y) = a * b * ↑((L.form x) y)

The completed rational form on pure tensors.

theorem TauCeti.IntegralLattice.isSymm_localIntegralForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : (L.localIntegralForm p).IsSymm

The localized integral form is symmetric.

theorem TauCeti.IntegralLattice.isSymm_completedRationalForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : (L.completedRationalForm p).IsSymm

The completed rational form is symmetric.

noncomputable def TauCeti.IntegralLattice.localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : L.LocalCarrier p →ₗ[ℤ_[p]] TensorProduct ℚ ℚ_[p] V

The canonical ℤ_p-linear map from the integral localization of L to the completion of its ambient space, sending a ⊗ x to a ⊗ x.

@[simp]

theorem TauCeti.IntegralLattice.localizationToCompletion_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ_[p]) (x : ↥L.carrier) : (L.localizationToCompletion p) (a ⊗ₜ[ℤ] x) = ↑a ⊗ₜ[ℚ] ↑x

The canonical map on pure tensors.

theorem TauCeti.IntegralLattice.isBaseChange_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : IsBaseChange ℚ_[p] (L.localizationToCompletion p)

The completion is the scalar extension of the localization. Extending scalars along the canonical map L_p → V_p from ℤ_p to ℚ_p is an isomorphism ℚ_p ⊗[ℤ_p] L_p ≃ V_p.

theorem TauCeti.IntegralLattice.localizationToCompletion_injective {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : Function.Injective ⇑(L.localizationToCompletion p)

The canonical map L_p → V_p is injective.

theorem TauCeti.IntegralLattice.span_range_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : Submodule.span ℚ_[p] (Set.range ⇑(L.localizationToCompletion p)) = ⊤

The image of L_p spans V_p over ℚ_p, so L_p is full in the completion.

instance TauCeti.IntegralLattice.isLattice_range_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : Submodule.IsLattice ℚ_[p] (L.localizationToCompletion p).range

The image of the integral localization is a full ℤ_p-lattice in the completion.

theorem TauCeti.IntegralLattice.range_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : (L.localizationToCompletion p).range = L.carrier.padicLocalization p

The image of L_p in V_p is the localization of the carrier of L, the ℤ_p-span of the vectors 1 ⊗ x with x ∈ L.

theorem TauCeti.IntegralLattice.localizationToCompletion_basis_baseChange {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] {ι : Type u_1} (e : Module.Basis ι ℤ ↥L.carrier) (i : ι) : (L.localizationToCompletion p) ((Module.Basis.baseChange ℤ_[p] e) i) = (Module.Basis.baseChange ℚ_[p] (Module.Basis.extendOfIsLattice ℚ e)) i

The canonical map L_p → V_p carries the scalar extension of a basis of L to the scalar extension of the corresponding rational basis of V.

theorem TauCeti.IntegralLattice.repr_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] {ι : Type u_1} (e : Module.Basis ι ℤ ↥L.carrier) (x : L.LocalCarrier p) (i : ι) : ((Module.Basis.baseChange ℚ_[p] (Module.Basis.extendOfIsLattice ℚ e)).repr ((L.localizationToCompletion p) x)) i = ↑(((Module.Basis.baseChange ℤ_[p] e).repr x) i)

The coordinates of a vector of L_p, read in V_p, are the images of its ℤ_p-coordinates: in the rational basis of a basis e of L, the image of L_p has p-adic integral coordinates.

theorem TauCeti.IntegralLattice.mem_range_localizationToCompletion_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] {ι : Type u_1} (e : Module.Basis ι ℤ ↥L.carrier) (x : TensorProduct ℚ ℚ_[p] V) : x ∈ (L.localizationToCompletion p).range ↔ ∀ (i : ι), ‖((Module.Basis.baseChange ℚ_[p] (Module.Basis.extendOfIsLattice ℚ e)).repr x) i‖ ≤ 1

In the rational basis of a basis e of L, the image of L_p in V_p consists of the vectors whose coordinates are p-adic integers.

@[simp]

theorem TauCeti.IntegralLattice.completedRationalForm_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (x y : L.LocalCarrier p) : ((L.completedRationalForm p) ((L.localizationToCompletion p) x)) ((L.localizationToCompletion p) y) = (algebraMap ℤ_[p] ℚ_[p]) (((L.localIntegralForm p) x) y)

The localized integral form is the restriction of the completed rational form along the canonical map L_p → V_p.

@[simp]

theorem TauCeti.IntegralLattice.toMatrix_localIntegralForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : (LinearMap.BilinForm.toMatrix (Module.Basis.baseChange ℤ_[p] e)) (L.localIntegralForm p) = (L.gramMatrix e).map Int.cast

The Gram matrix of the localized integral form in a base-changed carrier basis is the image of the integral Gram matrix of the lattice.

theorem TauCeti.IntegralLattice.det_toMatrix_localIntegralForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : ((LinearMap.BilinForm.toMatrix (Module.Basis.baseChange ℤ_[p] e)) (L.localIntegralForm p)).det = ↑L.determinant

The determinant of the localized integral form in any base-changed carrier basis is the image of the lattice's basis-independent signed determinant.

theorem TauCeti.IntegralLattice.nondegenerate_localIntegralForm_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : (L.localIntegralForm p).Nondegenerate ↔ L.form.Nondegenerate

The localized integral form is nondegenerate exactly when the rational form of the lattice is.

theorem TauCeti.IntegralLattice.nondegenerate_completedRationalForm_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : (L.completedRationalForm p).Nondegenerate ↔ L.form.Nondegenerate

The completed rational form is nondegenerate exactly when the rational form of the lattice is.

noncomputable def TauCeti.IntegralLattice.completedRationalFormIsometryEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] : (LinearMap.BilinForm.baseChange ℚ_[p] (L.localIntegralForm p)).IsometryEquiv (L.completedRationalForm p)

The scalar extension from ℤ_p to ℚ_p of the localized integral form is the completed rational form, through the canonical isomorphism ℚ_p ⊗[ℤ_p] L_p ≃ V_p.

@[simp]

theorem TauCeti.IntegralLattice.completedRationalFormIsometryEquiv_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (a : ℚ_[p]) (x : L.LocalCarrier p) : (L.completedRationalFormIsometryEquiv p) (a ⊗ₜ[ℤ_[p]] x) = a • (L.localizationToCompletion p) x

The isomorphism ℚ_p ⊗[ℤ_p] L_p ≃ V_p sends a ⊗ x to a times the image of x in the completion.

noncomputable def TauCeti.IntegralLattice.completedIsometryEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : (L.localIntegralForm p).IsometryEquiv (M.localIntegralForm p)) : (L.completedRationalForm p).IsometryEquiv (M.completedRationalForm p)

An isometry of integral localizations extends to the completed rational spaces. An isometry L_p ≃ M_p of the localized integral forms extends ℚ_p-linearly to an isometry V_p ≃ W_p of the completed rational forms.

@[simp]

theorem TauCeti.IntegralLattice.completedIsometryEquiv_localizationToCompletion {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : (L.localIntegralForm p).IsometryEquiv (M.localIntegralForm p)) (x : L.LocalCarrier p) : (completedIsometryEquiv p e) ((L.localizationToCompletion p) x) = (M.localizationToCompletion p) (e x)

The completed isometry extends the integral one along the canonical maps L_p → V_p and M_p → W_p.

theorem TauCeti.IntegralLattice.completedRationalForm_equivalent_of_localIntegralForm_equivalent {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (h : (L.localIntegralForm p).Equivalent (M.localIntegralForm p)) : (L.completedRationalForm p).Equivalent (M.completedRationalForm p)

Integral local isometry implies rational local isometry: if the integral localizations of L and M at p are isometric, then so are their completed rational spaces.

noncomputable def TauCeti.IntegralLattice.Isometry.localCarrierIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) : (L.localIntegralForm p).IsometryEquiv (M.localIntegralForm p)

An isometry of integral lattices localizes to an isometry of the localized integral forms: the base change to ℤ_p of its carrier equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.localCarrierIsometry_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) (a : ℤ_[p]) (x : ↥L.carrier) : (localCarrierIsometry p e) (a ⊗ₜ[ℤ] x) = a ⊗ₜ[ℤ] e.carrierEquiv x

The localized isometry on pure tensors.

noncomputable def TauCeti.IntegralLattice.Isometry.completedIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) : (L.completedRationalForm p).IsometryEquiv (M.completedRationalForm p)

An isometry of integral lattices extends to an isometry of the completed rational forms.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.completedIsometry_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) (a : ℚ_[p]) (v : V) : (completedIsometry p e) (a ⊗ₜ[ℚ] v) = a ⊗ₜ[ℚ] e v

The completed isometry on pure tensors.

theorem TauCeti.IntegralLattice.Isometry.localizationToCompletion_localCarrierIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) (x : L.LocalCarrier p) : (M.localizationToCompletion p) ((localCarrierIsometry p e) x) = (completedIsometry p e) ((L.localizationToCompletion p) x)

Localization is natural in isometries: the canonical maps L_p → V_p and M_p → W_p intertwine the localized and the completed isometries.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.completedIsometryEquiv_localCarrierIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [Fact (Nat.Prime p)] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) : completedIsometryEquiv p (localCarrierIsometry p e) = completedIsometry p e

Extending the localized isometry of a lattice isometry to the completions recovers the completed isometry.