Localization and lattice operations

Localization commutes with orthogonal sums and integral form twists. The sum comparison is an isometry, both on the integral localizations and on the completed rational spaces. The two comparisons intertwine the canonical maps from localization to completion, so the integral and rational decompositions describe the same embedded local lattice.

Form twists keep the carrier and the canonical embedding fixed and multiply each local form by the image of the integer scalar. No nondegeneracy or invertibility of two is required: zero forms, rank zero, and the dyadic prime are included.

Main declarations

• TauCeti.IntegralLattice.localOrthogonalSumIsometry: the integral localization of an orthogonal sum is the product of the localized forms.
• TauCeti.IntegralLattice.completedOrthogonalSumIsometry: the analogous rational comparison.
• TauCeti.IntegralLattice.completedOrthogonalSumIsometry_localizationToCompletion: compatibility of the comparisons with the embeddings into the completed spaces.
• TauCeti.IntegralLattice.localIntegralForm_smul and TauCeti.IntegralLattice.completedRationalForm_smul: localization commutes with form twists.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Chapter VIII.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8.

noncomputable def TauCeti.IntegralLattice.localOrthogonalSumIsometry {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] : ((L.orthogonalSum M).localIntegralForm p).IsometryEquiv ((L.localIntegralForm p).prod (M.localIntegralForm p))

The localization of an orthogonal sum is isometric to the product of the localized forms. The underlying equivalence is scalar extension of the carrier-product equivalence followed by tensor-product distribution over products.

@[simp]

theorem TauCeti.IntegralLattice.localOrthogonalSumIsometry_tmul {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ_[p]) (x : ↥(L.orthogonalSum M).carrier) : (L.localOrthogonalSumIsometry M p) (a ⊗ₜ[ℤ] x) = (a ⊗ₜ[ℤ] (L.orthogonalSumFst M) x, a ⊗ₜ[ℤ] (L.orthogonalSumSnd M) x)

The integral sum comparison on a pure tensor.

@[simp]

theorem TauCeti.IntegralLattice.localOrthogonalSumIsometry_symm_tmul {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ_[p]) (x : ↥L.carrier) (y : ↥M.carrier) : (L.localOrthogonalSumIsometry M p).symm (a ⊗ₜ[ℤ] x, a ⊗ₜ[ℤ] y) = a ⊗ₜ[ℤ] ((L.orthogonalSumInl M) x + (L.orthogonalSumInr M) y)

The inverse integral sum comparison on a pair of pure tensors with a common scalar.

@[simp]

theorem TauCeti.IntegralLattice.localOrthogonalSumIsometry_symm_tmul_zero {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ_[p]) (x : ↥L.carrier) : (L.localOrthogonalSumIsometry M p).symm (a ⊗ₜ[ℤ] x, 0) = a ⊗ₜ[ℤ] (L.orthogonalSumInl M) x

The inverse integral sum comparison on a pure tensor in the first coordinate.

@[simp]

theorem TauCeti.IntegralLattice.localOrthogonalSumIsometry_symm_zero_tmul {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ_[p]) (y : ↥M.carrier) : (L.localOrthogonalSumIsometry M p).symm (0, a ⊗ₜ[ℤ] y) = a ⊗ₜ[ℤ] (L.orthogonalSumInr M) y

The inverse integral sum comparison on a pure tensor in the second coordinate.

noncomputable def TauCeti.IntegralLattice.completedOrthogonalSumIsometry {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] : ((L.orthogonalSum M).completedRationalForm p).IsometryEquiv ((L.completedRationalForm p).prod (M.completedRationalForm p))

The completion of an orthogonal sum is isometric to the product of the completed forms.

@[simp]

theorem TauCeti.IntegralLattice.completedOrthogonalSumIsometry_tmul {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℚ_[p]) (x : V × W) : (L.completedOrthogonalSumIsometry M p) (a ⊗ₜ[ℚ] x) = (a ⊗ₜ[ℚ] x.1, a ⊗ₜ[ℚ] x.2)

The rational sum comparison on a pure tensor.

@[simp]

theorem TauCeti.IntegralLattice.completedOrthogonalSumIsometry_symm_tmul {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℚ_[p]) (x : V) (y : W) : (L.completedOrthogonalSumIsometry M p).symm (a ⊗ₜ[ℚ] x, a ⊗ₜ[ℚ] y) = a ⊗ₜ[ℚ] (x, y)

The inverse rational sum comparison on a pair of pure tensors with a common scalar.

@[simp]

theorem TauCeti.IntegralLattice.completedOrthogonalSumIsometry_symm_tmul_zero {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℚ_[p]) (x : V) : (L.completedOrthogonalSumIsometry M p).symm (a ⊗ₜ[ℚ] x, 0) = a ⊗ₜ[ℚ] (x, 0)

The inverse rational sum comparison on a pure tensor in the first coordinate.

@[simp]

theorem TauCeti.IntegralLattice.completedOrthogonalSumIsometry_symm_zero_tmul {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (a : ℚ_[p]) (y : W) : (L.completedOrthogonalSumIsometry M p).symm (0, a ⊗ₜ[ℚ] y) = a ⊗ₜ[ℚ] (0, y)

The inverse rational sum comparison on a pure tensor in the second coordinate.

theorem TauCeti.IntegralLattice.completedOrthogonalSumIsometry_localizationToCompletion {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] (x : (L.orthogonalSum M).LocalCarrier p) : (L.completedOrthogonalSumIsometry M p) (((L.orthogonalSum M).localizationToCompletion p) x) = ((L.localizationToCompletion p) ((L.localOrthogonalSumIsometry M p) x).1, (M.localizationToCompletion p) ((L.localOrthogonalSumIsometry M p) x).2)

The integral and rational orthogonal-sum comparisons commute with the canonical embeddings from localization to completion.

theorem TauCeti.IntegralLattice.map_range_localizationToCompletion_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ℕ) [Fact (Nat.Prime p)] : Submodule.map (↑ℤ_[p] ↑(L.completedOrthogonalSumIsometry M p).toLinearEquiv) ((L.orthogonalSum M).localizationToCompletion p).range = (L.localizationToCompletion p).range.prod (M.localizationToCompletion p).range

The local carrier of an orthogonal sum, transported to the product completion, is the product of the two local carriers. This identifies the embedded lattices, not just their forms.

@[simp]

theorem TauCeti.IntegralLattice.localizationToCompletion_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (n : ℤ) : (n • L).localizationToCompletion p = L.localizationToCompletion p

Form twisting does not change the canonical map from the localization to the completion. The carrier is unchanged, so both maps have the same domain.

@[simp]

theorem TauCeti.IntegralLattice.localIntegralForm_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (n : ℤ) : (n • L).localIntegralForm p = ↑n • L.localIntegralForm p

An integral form twist localizes to the same scalar twist over ℤ_p.

@[simp]

theorem TauCeti.IntegralLattice.completedRationalForm_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] (n : ℤ) : (n • L).completedRationalForm p = ↑n • L.completedRationalForm p

An integral form twist completes to the same scalar twist over ℚ_p.