Definitions/Def_NumberField_EuclideanIdealLattice.lean

Throughout, K is a number field. Two total definitions are made, with no side conditions on their arguments.

For a unit I of the monoid of fractional ideals of \mathcal{O}_K in K, Deep.Analytic.euclideanIdealLattice K I is the \mathbb{Z}-submodule of the Euclidean model euclidean.mixedSpace K of the mixed space \mathbb{R}^{r_1}\times\mathbb{C}^{r_2} obtained by transporting Mathlib's ideal lattice NumberField.mixedEmbedding.idealLattice K I — the image of I under the canonical (mixed) embedding of K — along the linear map underlying euclidean.toMixed K, using ZLattice.comap over \mathbb{R}. Thus a point of the Euclidean model lies in euclideanIdealLattice K I exactly when its image in the mixed space belongs to the image of I; the ZLattice.comap construction records this preimage as a \mathbb{Z}-submodule, so that the lattice structure of the ideal is available in the space carrying the Euclidean inner product rather than in the mixed space itself.

M4aP2.heckeScale K I is the real number \bigl(|d_K|\cdot \mathrm{N}(I)^2\bigr)^{-1/n}, formed with the real power function, where d_K is the discriminant of K cast to \mathbb{R}, \mathrm{N}(I) is the absolute norm FractionalIdeal.absNorm of the underlying fractional ideal of I cast to \mathbb{R}, and n=[K:\mathbb{Q}] is Module.finrank ℚ K cast to \mathbb{R} (so the exponent is -1/n as a real exponent). This is the scaling factor by which Gaussians are dilated in the theta series attached to I, normalised so that the factors attached to I and to the inverse of \mathfrak{d}_K I are mutually inverse.