A subgroup with compact quotient spans a finite-dimensional real space #
An additive subgroup L of a finite-dimensional Hausdorff real topological vector space V
whose quotient V ⧸ L is compact spans V over ℝ. Otherwise a nonzero linear functional
vanishes on the span of L; it is continuous because V is finite-dimensional, so it descends to
a continuous surjection V ⧸ L → ℝ, whose range would be compact, and ℝ is not.
This is the half of the characterisation of lattices that produces the spanning condition of
IsZLattice from compactness of the quotient; the other half, that a discrete subgroup is
closed and that a lattice has compact quotient, is Mathlib's.
Main results #
AddSubgroup.span_eq_top_of_compactSpace_quotient: an additive subgroup with compact quotient spans the space.
References #
- N. Bourbaki, General Topology, Chapters 5–10, Springer (1989), Chapter VII (The additive
groups
ℝⁿ), § 1 (Subgroups and quotient groups ofℝⁿ).
theorem
AddSubgroup.span_eq_top_of_compactSpace_quotient
{V : Type u_1}
[AddCommGroup V]
[Module ℝ V]
[TopologicalSpace V]
[IsTopologicalAddGroup V]
[ContinuousSMul ℝ V]
[T2Space V]
[FiniteDimensional ℝ V]
(L : AddSubgroup V)
[CompactSpace (V ⧸ L)]
:
An additive subgroup of a finite-dimensional real space with compact quotient spans the space.