Lattice bases adapted to a flag

Let L be a discrete subgroup of a finite-dimensional real normed space E, and let a 0, …, a (n - 1) be lattice vectors forming an ℝ-basis of E. They need not span L: they span a sublattice of finite index. This file constructs a ℤ-basis b of L adapted to the flag of subspaces span ℝ {a i | i ≤ j}: each b j is a combination of a 0, …, a j, and it is reduced, being either a j itself or a combination all of whose coefficients have absolute value at most 1 / 2 (ZLattice.exists_basis_triangular). In particular b and a define the same flag: for every k, the first k vectors of b span over ℝ the same subspace as a 0, …, a (k - 1) (ZLattice.exists_basis_span_image_eq_flag).

The coordinate-level triangular basis is used by TauCeti.Algebra.Module.ZLattice.GaugeBasis to prove the canonical gauge estimate. The lattice is not assumed to be full: this follows from the given basis.

Main results

• ZLattice.exists_basis_triangular: a reduced basis of L that is triangular with respect to an ℝ-basis of E consisting of lattice vectors.
• ZLattice.exists_basis_span_image_eq_flag: a basis of L with the same real flag as an ℝ-basis of E consisting of lattice vectors.
• ZLattice.equivFun_ofZLatticeBasis_apply_eq_zero: coordinates past an adapted flag vanish.

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter I, Theorem I and Corollary 1, and Chapter V, Lemma 8.

theorem ZLattice.le_span_of_triangular {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L : Submodule ℤ E} {n : ℕ} (e : Module.Basis (Fin n) ℝ E) {v : Fin n → E} (hv : ∀ (j : Fin n), v j ∈ L) (htri : ∀ (j i : Fin n), j < i → (e.repr (v j)) i = 0) (hgen : ∀ (j : Fin n), ∀ x ∈ L, (∀ (i : Fin n), j < i → (e.repr x) i = 0) → ∃ (m : ℤ), (e.repr x) j = ↑m * (e.repr (v j)) j) : L ≤ Submodule.span ℤ (Set.range v)

A family of lattice vectors, triangular with respect to e, whose diagonal coordinates generate the corresponding coordinates of the lattice, spans the lattice.

theorem ZLattice.exists_basis_triangular {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {n : ℕ} (e : Module.Basis (Fin n) ℝ E) (he : ∀ (i : Fin n), e i ∈ L) : ∃ (b : Module.Basis (Fin n) ℤ ↥L), ∀ (j : Fin n), (∀ (i : Fin n), j < i → (e.repr ↑(b j)) i = 0) ∧ (↑(b j) = e j ∨ ∀ (i : Fin n), |(e.repr ↑(b j)) i| ≤ 1 / 2)

Adapted basis. Let e be an ℝ-basis of E consisting of vectors of a discrete subgroup L. Then L has a ℤ-basis b that is triangular with respect to e, in that b j ∈ span ℝ {e i | i ≤ j}, and reduced: each b j is either e j or has all its coordinates with respect to e of absolute value at most 1 / 2.

theorem ZLattice.exists_basis_span_image_eq_flag {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {n : ℕ} (e : Module.Basis (Fin n) ℝ E) (he : ∀ (i : Fin n), e i ∈ L) : ∃ (b : Module.Basis (Fin n) ℤ ↥L), ∀ (k : Fin (n + 1)), Submodule.span ℝ ((fun (j : Fin n) => ↑(b j)) '' {j : Fin n | j.castSucc < k}) = e.flag k

Lattice basis with a prescribed flag. Let e be an ℝ-basis of E consisting of vectors of a discrete subgroup L. Then L has a ℤ-basis b with the same real flag as e: for every k, the vectors b 0, …, b (k - 1) span over ℝ the subspace e.flag k spanned by e 0, …, e (k - 1). The vectors b j and e j differ in general, since the e j need not span L over ℤ.

theorem ZLattice.equivFun_ofZLatticeBasis_apply_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {n : ℕ} [FiniteDimensional ℝ E] [IsZLattice ℝ L] {e : Module.Basis (Fin n) ℝ E} {b : Module.Basis (Fin n) ℤ ↥L} (hb : ∀ (k : Fin (n + 1)), Submodule.span ℝ ((fun (j : Fin n) => ↑(b j)) '' {j : Fin n | j.castSucc < k}) = e.flag k) (j : Fin n) {v : E} (hv : v ∈ Submodule.span ℝ (⇑e '' Set.Iio j)) : (Module.Basis.ofZLatticeBasis ℝ L b).equivFun v j = 0

In coordinates of a lattice basis adapted to the flag of e, the j-th coordinate vanishes on the span of the first j basis vectors of e.