Lattices under a linear change of variables

A continuous linear automorphism A of a finite-dimensional real vector space carries a full ℤ-lattice L to the full lattice A L, which Mathlib writes as the pullback ZLattice.comap ℝ L A⁻¹. Pulling back along A divides the covolume by |det A| (ZLattice.covolume_comap_continuousLinearEquiv), so covolume (A L) = |det A| * covolume L, and the dual lattice transforms by the adjoint of A⁻¹ (ZLattice.dual_comap_continuousLinearEquiv).

In a finite-dimensional real inner product space this exhibits every full lattice as a linear image of the self-dual lattice spanned by an orthonormal basis: for every orthonormal basis there is an automorphism A carrying that lattice onto L, with (A⁻¹)ᵀ carrying it onto L^∨ and with |det A| = covolume L (ZLattice.exists_comap_span_orthonormalBasis_eq). With the Fourier change of variables ContinuousLinearEquiv.fourier_comp, this is what reduces a summation formula over a general lattice and its dual to the same formula over ℤⁿ, the constant |det A| becoming the covolume.

Main statement

• ZLattice.exists_comap_span_orthonormalBasis_eq: every full lattice in a finite-dimensional real inner product space is the image of the lattice spanned by a given orthonormal basis under an automorphism A with |det A| = covolume L, and its pullback along the adjoint of A is L^∨.

theorem ZLattice.exists_comap_span_orthonormalBasis_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (o : OrthonormalBasis ι ℝ E) : ∃ (A : E ≃L[ℝ] E), ZLattice.comap ℝ (Submodule.span ℤ (Set.range ⇑o)) ↑↑A.symm = L ∧ ZLattice.comap ℝ (Submodule.span ℤ (Set.range ⇑o)) ↑(ContinuousLinearMap.adjoint ↑A) = dual L ∧ |LinearMap.det ↑↑A| = covolume L MeasureTheory.volume

Every full lattice L in a finite-dimensional real inner product space is the image of the lattice spanned by an orthonormal basis o under a linear automorphism A with |det A| = covolume L. The adjoint of A pulls that self-dual lattice back to the dual L^∨; read through images, L^∨ = (A⁻¹)ᵀ (span ℤ (range o)).