Dense additive subgroups of finite-dimensional real spaces

An additive subgroup H of a finite-dimensional real normed space E is dense exactly when no nonzero real linear functional takes only integer values on H (AddSubgroup.dense_iff_forall_dual_eq_zero). This is the higher-dimensional analogue of the dichotomy for subgroups of ℝ (dense_addSubgroupClosure_pair_iff), and the abstract form of Kronecker's approximation theorem: for the subgroup of ℝⁿ generated by ℤⁿ and one vector α, an integer-valued functional is an integer relation between 1, α₁, …, αₙ. For a subgroup H spanning E the vectors α with H + ℤ α dense are themselves dense (AddSubgroup.dense_setOfPred_dense_sup): the others lie in countably many affine hyperplanes, the level sets of the functionals with integer coefficients in a basis of E taken inside H, and the Baire category theorem applies.

The proof uses the structure of closed subgroups. A closed subgroup G containing no line through the origin is discrete (AddSubgroup.discreteTopology_of_isClosed_of_forall_smul_mem). In general, the vectors v with ℝ v ⊆ G form a subspace V ⊆ G, and G is the sum of V and its trace on a complement W of V, which is discrete. If G ≠ E spans E, that trace is a lattice in W ≠ 0, and a coordinate functional of a lattice basis, composed with the projection onto W, is integer-valued on G (AddSubgroup.exists_dual_ne_zero_of_isClosed).

Main results

• ZLattice.exists_dual_ne_zero: a full lattice in a nonzero space admits a nonzero linear functional with integer values on it.
• AddSubgroup.discreteTopology_of_isClosed_of_forall_smul_mem: a closed subgroup containing no line through the origin is discrete.
• AddSubgroup.exists_dual_ne_zero_of_isClosed: a proper closed subgroup admits a nonzero linear functional with integer values on it.
• AddSubgroup.dense_iff_forall_dual_eq_zero: a subgroup is dense if and only if every linear functional with integer values on it vanishes.
• AddSubgroup.dense_setOfPred_dense_sup: for a subgroup H spanning E, the vectors x with H + ℤ x dense are dense.

References

• N. Bourbaki, General Topology, Chapter VII, § 1, no. 2, Theorem 2 (closed subgroups of ℝⁿ) and § 1, no. 3, Proposition 7 (dense subgroups of ℝⁿ).
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, Chapter XXIII.

theorem AddSubgroup.discreteTopology_of_isClosed_of_forall_smul_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {G : AddSubgroup E} (hG : IsClosed ↑G) (hline : ∀ (v : E), (∀ (t : ℝ), t • v ∈ G) → v = 0) : DiscreteTopology ↥G

A closed additive subgroup of a finite-dimensional real normed space that contains no line through the origin is discrete.

theorem ZLattice.exists_dual_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] : ∃ (f : Module.Dual ℝ E), f ≠ 0 ∧ ∀ x ∈ L, ∃ (k : ℤ), f x = ↑k

A full lattice L in a nonzero finite-dimensional real normed space admits a nonzero real linear functional taking integer values on L, for instance a coordinate functional of a ℤ-basis of L.

theorem AddSubgroup.exists_dual_ne_zero_of_isClosed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {G : AddSubgroup E} (hG : IsClosed ↑G) (hne : G ≠ ⊤) : ∃ (f : Module.Dual ℝ E), f ≠ 0 ∧ ∀ g ∈ G, ∃ (k : ℤ), f g = ↑k

Closed subgroups of a finite-dimensional real space. A proper closed additive subgroup G of a finite-dimensional real normed space admits a nonzero real linear functional taking integer values on G.

theorem AddSubgroup.dense_iff_forall_dual_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : AddSubgroup E} : Dense ↑H ↔ ∀ (f : Module.Dual ℝ E), (∀ h ∈ H, ∃ (k : ℤ), f h = ↑k) → f = 0

Dense subgroups of a finite-dimensional real space. An additive subgroup H of a finite-dimensional real normed space is dense if and only if every real linear functional taking integer values on H is zero.

theorem AddSubgroup.dense_setOfPred_dense_sup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : AddSubgroup E} (hH : Submodule.span ℝ ↑H = ⊤) : Dense {x : E | Dense ↑(H ⊔ zmultiples x)}

Generic vectors are dense: for an additive subgroup H spanning E, the vectors x such that H + ℤ x is dense form a dense set.