A lattice basis adapted to a flag

Let L be a discrete ℤ-submodule of a finite-dimensional real normed space E, and let v 0, …, v (n - 1) be ℝ-linearly independent vectors of L, with n = finrank ℝ E. This file builds a ℤ-basis b 0, …, b (n - 1) of L adapted to the flag the v i span: for every j, the first j members of b are a ℤ-basis of L ∩ span ℝ (v 0, …, v (j - 1)).

Main definitions

• ZLattice.flagPart: the j-th step L ∩ span ℝ (v 0, …, v (j - 1)) of the flag, as a ℤ-submodule. The construction below is an induction along it, and so is the basis from the successive minima of Layer 4.6.

Main results

• ZLattice.exists_basis_adapted: the adapted basis, stated both integrally — the ℤ-span of the first j basis vectors is exactly the part of L in the span of the first j of the v i — and in the weaker ℝ-form, that the two flags of subspaces coincide.
• ZLattice.exists_basis_mem_span_int_of_mem_span_real: the consequence the geometry of numbers uses, that a lattice point in the span of the first j of the v i is an integer combination of the first j basis vectors.
• ZLattice.exists_extending: the induction step in isolation — across a saturated step of rank one, a single vector y generates the quotient, in the form Basis.mkFinSnocOfLE consumes.
• ZLattice.extending_congr: that generating vector is determined only modulo the smaller module, which is the freedom Layer 4.6 spends on making the new basis vector short.
• ZLattice.discreteTopology_of_le and ZLattice.finrank_int_eq_finrank_real: the two facts about a submodule of a discrete lattice that the construction rests on, stated at arbitrary rank — it is discrete, and its ℤ-rank is the ℝ-dimension of its span. Minkowski's second theorem needs both for the sublattices cut out by the flag.

Implementation notes

The construction is the modern one and not Cassels': the part flagPart L v j of L in the j-th subspace of the flag is saturated in flagPart L v (j + 1) — no nonzero multiple of a lattice point lies in it unless the point does, because the subspaces are ℝ-subspaces — so the quotient is finitely generated and torsion-free, hence free, and its rank is 1 by the rank-nullity theorem. A generator of that quotient extends a basis of flagPart L v j to a basis of flagPart L v (j + 1) through Mathlib's Basis.mkFinSnocOfLE, and n steps reach L itself.

⚠ All the analysis is in one rank computation. Discreteness is used twice: to know that the parts of L are finitely generated over ℤ, which is Mathlib's instModuleFinite_of_discrete_submodule, and — indispensably — for finrank ℤ (flagPart L v j) = finrank ℝ (span ℝ (flagPart L v j)), which is Mathlib's Real.finrank_eq_int_finrank_of_discrete. A non-discrete subgroup such as ℤ + ℤ √2 ⊆ ℝ is finitely generated but has ℤ-rank larger than the dimension of its span, and then the quotients above are free of rank > 1 and no single vector extends the basis. The induction step is therefore stated with no topology at all: it asks for the rank as a hypothesis.

⚠ IsZLattice ℝ L is not needed. The independent family already spans E over ℝ, so a lattice that contains it spans E; asking for the instance would be asking for a consequence of the hypotheses.

References

J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer (1959), Chapter I, Theorem I: for a sublattice Λ of a lattice M and a basis a 1, …, a n of Λ, a basis b 1, …, b n of M with a i = ∑_{j ≤ i} v i j • b j and v i i ≠ 0 (part B; part A is the converse, the Hermite normal form of a sublattice). That triangular shape is the ℝ-form below, and the integral form follows from it because the b i are a basis of M.

This is the lattice content of Chapter VIII, Lemma 2 — the basis such that F x < λ i forces x to be an integer combination of b 1, …, b (i - 1) — which is Cassels' Theorem I of Chapter I applied to the family of Lemma 1, the family realizing the successive minima.

This is infrastructure for Layers 4.2 and 4.6 of the ArithmeticHeights roadmap.

Discreteness and rank

theorem ZLattice.discreteTopology_of_le {E : Type u_1} [NormedAddCommGroup E] {L N : Submodule ℤ E} [DiscreteTopology ↥L] (h : N ≤ L) : DiscreteTopology ↥N

A ℤ-submodule of a discrete one is discrete: the inclusion is a continuous injection. This is stated for a submodule of arbitrary rank, which is what the sublattices cut out by a flag of subspaces need; Mathlib's instances for lattices assume full rank.

theorem ZLattice.finrank_int_eq_finrank_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L N : Submodule ℤ E} [DiscreteTopology ↥L] (h : N ≤ L) : Module.finrank ℤ ↥N = Module.finrank ℝ ↥(Submodule.span ℝ ↑N)

The ℤ-rank of a submodule of a discrete lattice is the ℝ-dimension of its span. This is the step discreteness is indispensable for: ℤ + ℤ √2 has ℤ-rank two inside a line.

The flag of an independent family

def ZLattice.flagPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) (j : ℕ) : Submodule ℤ E

The part of a lattice L inside the ℝ-span of the first j members of a family v: the j-th step of the flag along which an adapted basis is built.

Equations

• ZLattice.flagPart L v j = L ⊓ Submodule.restrictScalars ℤ (Submodule.span ℝ (v '' {i : Fin n | ↑i < j}))

theorem ZLattice.mem_flagPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) (j : ℕ) {x : E} : x ∈ flagPart L v j ↔ x ∈ L ∧ x ∈ Submodule.span ℝ (v '' {i : Fin n | ↑i < j})

theorem ZLattice.flagPart_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) (j : ℕ) : flagPart L v j ≤ L

theorem ZLattice.flagPart_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) : flagPart L v 0 = ⊥

theorem ZLattice.flagPart_mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) {j k : ℕ} (hjk : j ≤ k) : flagPart L v j ≤ flagPart L v k

theorem ZLattice.mem_flagPart_of_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) (hvL : ∀ (i : Fin n), v i ∈ L) {i : Fin n} {j : ℕ} (hij : ↑i < j) : v i ∈ flagPart L v j

theorem ZLattice.span_flagPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) (hvL : ∀ (i : Fin n), v i ∈ L) (j : ℕ) : Submodule.span ℝ ↑(flagPart L v j) = Submodule.span ℝ (v '' {i : Fin n | ↑i < j})

The steps of the flag span the subspaces they were cut out of: no ℝ-dimension is lost by intersecting with the lattice, because the lattice already contains a spanning family.

theorem ZLattice.flagPart_saturated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) {c : ℤ} (hc : c ≠ 0) {j : ℕ} {z : E} (hz : z ∈ L) (hcz : c • z ∈ flagPart L v j) : z ∈ flagPart L v j

The steps of the flag are saturated. A lattice point a nonzero multiple of which lies in flagPart L v j lies there itself: the j-th subspace is an ℝ-subspace, so it is closed under dividing by a nonzero integer.

theorem ZLattice.finrank_flagPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (L : Submodule ℤ E) [DiscreteTopology ↥L] (v : Fin n → E) (hv : LinearIndependent ℝ v) (hvL : ∀ (i : Fin n), v i ∈ L) {j : ℕ} (hj : j ≤ n) : Module.finrank ℤ ↥(flagPart L v j) = j

The j-th step of the flag has ℤ-rank j. This is where discreteness enters.

theorem ZLattice.flagPart_eq_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (L : Submodule ℤ E) (v : Fin n → E) (hn : n = Module.finrank ℝ E) (hv : LinearIndependent ℝ v) : flagPart L v n = L

The last step of the flag is the whole lattice.

The induction step

theorem ZLattice.exists_extending {E : Type u_1} [NormedAddCommGroup E] {N N' : Submodule ℤ E} (hle : N ≤ N') [Module.Finite ℤ ↥N'] (hsat : ∀ (c : ℤ), c ≠ 0 → ∀ z ∈ N', c • z ∈ N → z ∈ N) (hrank : Module.finrank ℤ ↥N' = Module.finrank ℤ ↥N + 1) : ∃ y ∈ N', (∀ (c : ℤ), ∀ x ∈ N, c • y + x = 0 → c = 0) ∧ ∀ z ∈ N', ∃ (c : ℤ), z + c • y ∈ N

A generator of a saturated rank-one step. If N ≤ N' are ℤ-submodules, N' has rank one more than N, and N is saturated in N' — a point of N' a nonzero multiple of which lies in N lies in N itself — then a single vector y of N' generates the quotient, in exactly the two clauses Basis.mkFinSnocOfLE asks for.

No topology enters: the geometric situation supplies the rank and the saturation, and the rest is that a finitely generated torsion-free ℤ-module of rank 1 is ℤ.

theorem ZLattice.extending_congr {E : Type u_1} [NormedAddCommGroup E] {N N' : Submodule ℤ E} {y y' : E} (hyy' : y' - y ∈ N) (hli : ∀ (c : ℤ), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ N', ∃ (c : ℤ), z + c • y ∈ N) : (∀ (c : ℤ), ∀ x ∈ N, c • y' + x = 0 → c = 0) ∧ ∀ z ∈ N', ∃ (c : ℤ), z + c • y' ∈ N

The generator is determined only modulo the smaller module. Moving y by an element of N preserves both clauses of ZLattice.exists_extending, so the basis vector added at each step may be shortened before it is added. This is the whole freedom Layer 4.6 has.

The adapted basis

theorem ZLattice.exists_basis_adapted {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {n : ℕ} (hn : n = Module.finrank ℝ E) {v : Fin n → E} (hvL : ∀ (i : Fin n), v i ∈ L) (hv : LinearIndependent ℝ v) : ∃ (b : Module.Basis (Fin n) ℤ ↥L), (∀ (j : ℕ), Submodule.span ℤ ((fun (i : Fin n) => ↑(b i)) '' {i : Fin n | ↑i < j}) = L ⊓ Submodule.restrictScalars ℤ (Submodule.span ℝ (v '' {i : Fin n | ↑i < j}))) ∧ ∀ (j : ℕ), Submodule.span ℝ ((fun (i : Fin n) => ↑(b i)) '' {i : Fin n | ↑i < j}) = Submodule.span ℝ (v '' {i : Fin n | ↑i < j})

A ℤ-basis adapted to the flag of an independent family. For ℝ-linearly independent lattice vectors v 0, …, v (n - 1) spanning E, some ℤ-basis b of L has, for every j, its first j members a ℤ-basis of the part of L in the span of v 0, …, v (j - 1); in particular the two flags of subspaces coincide.

This is Cassels' Chapter I, Theorem I, part B, in the form Chapter VIII, Lemma 2 uses it. Only discreteness of L is assumed: IsZLattice ℝ L follows from the hypotheses on v.

theorem ZLattice.exists_basis_mem_span_int_of_mem_span_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {n : ℕ} (hn : n = Module.finrank ℝ E) {v : Fin n → E} (hvL : ∀ (i : Fin n), v i ∈ L) (hv : LinearIndependent ℝ v) : ∃ (b : Module.Basis (Fin n) ℤ ↥L), ∀ (j : ℕ), ∀ x ∈ L, x ∈ Submodule.span ℝ (v '' {i : Fin n | ↑i < j}) → x ∈ Submodule.span ℤ ((fun (i : Fin n) => ↑(b i)) '' {i : Fin n | ↑i < j})

The integral form. With the basis of ZLattice.exists_basis_adapted, a lattice point in the ℝ-span of v 0, …, v (j - 1) is an integer combination of b 0, …, b (j - 1). This is the shape of Cassels' Chapter VIII, Lemma 2, and it is the shape the second theorem consumes.