The lattice of integral points of a rational subspace

For a subspace V of ℚ^ι, the integral points V ∩ ℤ^ι form a full lattice in the real span of V inside the Euclidean space ℝ^ι. The lattice is the whole intersection V ∩ ℤ^ι, which is saturated in ℤ^ι, and a ℤ-basis of it is a ℚ-basis of V and an ℝ-basis of the real span.

Main definitions

• Submodule.intPoints V: the integral points V ∩ ℤ^ι, as a ℤ-submodule of ℤ^ι.
• Submodule.realSpan V: the real span of V in the Euclidean space ℝ^ι.
• Submodule.intLattice V: the points of V.realSpan with integral coordinates, as a ℤ-submodule of V.realSpan.
• Submodule.intPointsEquivIntLattice V: the identification of the integral points of V with the points of V.intLattice.

Main results

• Matrix.intPoints_ker_mulVecLin: the integral points of a rational matrix kernel are its integral kernel.
• Submodule.toLp_mem_realSpan_iff: the rational points of V.realSpan are the points of V.
• Submodule.mem_intPoints_of_smul_mem: the integral points of V are saturated in ℤ^ι.
• Submodule.linearIndependent_intCast_basis_intPoints, Submodule.span_intCast_basis_intPoints: a ℤ-basis of the integral points of V is a ℚ-basis of V.
• Submodule.finrank_intPoints, Submodule.finrank_realSpan: the integral points form a free ℤ-module of rank dim V, and the real span has dimension dim V.
• The instances DiscreteTopology V.intLattice and IsZLattice ℝ V.intLattice: the integral points form a full lattice in the real span.

Implementation notes

The real span lives in EuclideanSpace ℝ ι because a lattice of rank smaller than #ι has a covolume only in its own real span, measured by the volume of the inner product it inherits.

References

• W. M. Schmidt, On heights of algebraic subspaces and diophantine approximations, Ann. of Math. 85 (1967), 430–472, §3.

The construction is adapted from Ralf Stephan's ArithmeticHeights/RationalLattice.lean in rwst/Subspace-Theorems, commit 9894a1c4baf805296b249e95575f0e16e8e1afa3 (Apache 2.0).

def Submodule.intPoints {ι : Type u_1} (V : Submodule ℚ (ι → ℚ)) : Submodule ℤ (ι → ℤ)

The integral points of a subspace V of ℚ^ι: the tuples z : ι → ℤ whose image in ℚ^ι lies in V.

@[simp]

theorem Submodule.mem_intPoints {ι : Type u_1} {V : Submodule ℚ (ι → ℚ)} {z : ι → ℤ} : z ∈ V.intPoints ↔ (fun (i : ι) => ↑(z i)) ∈ V

An integral tuple is an integral point of V when its image in ℚ^ι lies in V.

theorem Submodule.mem_intPoints_of_smul_mem {ι : Type u_1} {V : Submodule ℚ (ι → ℚ)} {c : ℤ} {z : ι → ℤ} (hc : c ≠ 0) (h : c • z ∈ V.intPoints) : z ∈ V.intPoints

The integral points of V form a saturated submodule of ℤ^ι: if a nonzero multiple of z is an integral point of V, so is z.

def Submodule.realSpan {ι : Type u_1} (V : Submodule ℚ (ι → ℚ)) : Submodule ℝ (EuclideanSpace ℝ ι)

The real span of a subspace V of ℚ^ι: the subspace of the Euclidean space ℝ^ι spanned by the points of V.

theorem Submodule.toLp_mem_realSpan {ι : Type u_1} {V : Submodule ℚ (ι → ℚ)} {v : ι → ℚ} (hv : v ∈ V) : (WithLp.toLp 2 fun (i : ι) => ↑(v i)) ∈ V.realSpan

The points of V lie in its real span.

def Submodule.intLattice {ι : Type u_1} (V : Submodule ℚ (ι → ℚ)) : Submodule ℤ ↥V.realSpan

The integral points of V as a lattice in the real span of V: the points of V.realSpan whose coordinates are integers.

@[simp]

theorem Submodule.mem_intLattice {ι : Type u_1} {V : Submodule ℚ (ι → ℚ)} {w : ↥V.realSpan} : w ∈ V.intLattice ↔ ∀ (i : ι), ∃ (z : ℤ), (↑w).ofLp i = ↑z

A point of the real span of V lies in V.intLattice when its coordinates are integers.

@[simp]

theorem Submodule.toLp_mem_realSpan_iff {ι : Type u_1} [Finite ι] {V : Submodule ℚ (ι → ℚ)} {v : ι → ℚ} : (WithLp.toLp 2 fun (i : ι) => ↑(v i)) ∈ V.realSpan ↔ v ∈ V

The rational points of the real span of V are the points of V.

theorem Submodule.linearIndependent_intCast_basis_intPoints {ι : Type u_1} [Finite ι] {V : Submodule ℚ (ι → ℚ)} {κ : Type u_2} (b : Module.Basis κ ℤ ↥V.intPoints) (S : Type u_3) [Field S] [CharZero S] : LinearIndependent S fun (i : κ) (j : ι) => ↑(↑(b i) j)

A basis of the integral points of V is linearly independent over every field of characteristic zero.

theorem Submodule.span_intCast_basis_intPoints {ι : Type u_1} [Finite ι] {V : Submodule ℚ (ι → ℚ)} {κ : Type u_2} (b : Module.Basis κ ℤ ↥V.intPoints) : span ℚ (Set.range fun (i : κ) (j : ι) => ↑(↑(b i) j)) = V

A basis of the integral points of V spans V over ℚ.

instance Submodule.discreteTopology_intLattice {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : DiscreteTopology ↥V.intLattice

The integral points of V form a discrete subgroup of its real span.

instance Submodule.isZLattice_intLattice {ι : Type u_1} [Finite ι] [Fintype ι] (V : Submodule ℚ (ι → ℚ)) : IsZLattice ℝ V.intLattice

The integral points of V span its real span: they form a full lattice in it.

theorem Submodule.finrank_intPoints {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : Module.finrank ℤ ↥V.intPoints = Module.finrank ℚ ↥V

The integral points of V form a free ℤ-module of rank dim V.

theorem Submodule.finrank_realSpan {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : Module.finrank ℝ ↥V.realSpan = Module.finrank ℚ ↥V

The real span of V has the dimension of V.

noncomputable def Submodule.intPointsEquivIntLattice {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : ↥V.intPoints ≃ₗ[ℤ] ↥V.intLattice

The identification of the integral points of V with the points of the lattice V.intLattice, sending z to the real point with the same coordinates. It transports a ℤ-basis of the lattice to a ℤ-basis of V ∩ ℤ^ι.

@[simp]

theorem Submodule.coe_intPointsEquivIntLattice_apply {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) (z : ↥V.intPoints) : ↑↑(V.intPointsEquivIntLattice z) = WithLp.toLp 2 fun (i : ι) => ↑(↑z i)

The point of V.intLattice attached to an integral point has the same coordinates.

@[simp]

theorem Submodule.intCast_intPointsEquivIntLattice_symm_apply {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) (w : ↥V.intLattice) (i : ι) : ↑(↑(V.intPointsEquivIntLattice.symm w) i) = (↑↑w).ofLp i

The integral point of V attached to a point of V.intLattice has the same coordinates.

@[simp]

theorem Matrix.intPoints_ker_mulVecLin {ι : Type u_1} [Fintype ι] {m : Type u_2} (A : Matrix m ι ℤ) : (A.map Int.cast).mulVecLin.ker.intPoints = A.mulVecLin.ker

The integral points of the rational kernel of an integer matrix are precisely its integral kernel.