A rank criterion for discrete integer submodules

A finitely generated integer submodule of a real normed space is discrete if and only if its integer rank equals the dimension of its real span. The necessity direction follows from ZLattice.rank and extends the rank comparison in Mathlib's Real.finrank_eq_int_finrank_of_discrete to arbitrary ambient dimension.

This criterion allows logarithmic images of finitely generated unit groups to be proved discrete from their rank and real span, without a separate compactness argument.

Main results

• TauCeti.discreteTopology_iff_finrank_eq_finrank_span: discreteness of a finitely generated integer submodule is equivalent to equality of its integer rank and its real span's dimension.
• setFinrank_real_eq_setFinrank_int_of_subset_discreteTopology and setFinrank_real_eq_finrank_int: in finite dimension, a set of vectors of a discrete integer submodule has the same real and integer rank, and the real rank of the submodule itself is its integer rank. These two statements and their names follow Kevin H. Wilson's successive-minima proposal for Mathlib, Mathlib/Algebra/Module/ZLattice/Basic.lean at revision 8423d1c of https://github.com/khwilson/mathlib4.

Apply (TauCeti.discreteTopology_iff_finrank_eq_finrank_span (L := L)).mpr hr to obtain discreteness from a rank equality hr.

theorem TauCeti.discreteTopology_iff_finrank_eq_finrank_span {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [Module.Finite ℤ ↥L] : DiscreteTopology ↥L ↔ Module.finrank ℤ ↥L = Module.finrank ℝ ↥(Submodule.span ℝ ↑L)

A finitely generated integer submodule is discrete exactly when its integer rank is the dimension of its real span. The ambient space need not be finite-dimensional.

theorem setFinrank_real_eq_setFinrank_int_of_subset_discreteTopology {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {s : Set E} (hs : s ⊆ ↑L) : Set.finrank ℝ s = Set.finrank ℤ s

A set of vectors of a discrete integer submodule has the same rank over ℝ as over ℤ.

@[simp]

theorem setFinrank_real_eq_finrank_int {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : Set.finrank ℝ ↑L = Module.finrank ℤ ↥L

The real rank of a discrete integer submodule is its integer rank.