A full lattice as an integral form of its ambient space

Let L be a ℤ-lattice in a finite-dimensional vector space E over a normed ordered field K, that is, a discrete subgroup spanning E. Every ℤ-basis of L is a K-basis of E (Module.Basis.ofZLatticeBasis), so E is the base change K ⊗[ℤ] L through the inclusion of L. This is the analogue, for a normed field such as ℝ in place of the field of fractions ℚ, of Submodule.isBaseChange_subtype.

In this form a lattice can be fed to statements about integral forms of a representation, such as the comparison of the Herbrand quotients of two Galois-stable lattices in one real representation (TauCeti.TateCohomology.herbrandQuotient_eq_of_isBaseChange).

Main results

• ZLattice.isBaseChange_subtype: the inclusion of a full ℤ-lattice exhibits the ambient space as its base change to K.

theorem ZLattice.isBaseChange_subtype (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice K L] : IsBaseChange K L.subtype

A full lattice is an integral form of its ambient space: the inclusion of a discrete ℤ-submodule L spanning E over K exhibits E as the base change K ⊗[ℤ] L.