Fundamental Cone: set of elements of norm ≤ 1 #
In this file, we study the subset NormLeOne of the fundamentalCone of elements x with
mixedEmbedding.norm x ≤ 1.
Mainly, we prove that this is bounded, its frontier has volume zero and compute its volume.
Strategy of proof #
The proof is loosely based on the strategy given in D. Marcus, Number Fields.
since
NormLeOne Kis norm-stable, in the sense thatnormLeOne K = normAtAllPlaces⁻¹' (normAtAllPlaces '' (normLeOne K)), seenormLeOne_eq_primeage_image, it's enough to study the subsetnormAtAllPlaces '' (normLeOne K)ofrealSpace K.A description of
normAtAllPlaces '' (normLeOne K)is given bynormAtAllPlaces_normLeOne, it is the set ofx : realSpace K, nonnegative at all places, whose norm is nonzero and≤ 1and such thatlogMap xis in thefundamentalDomainofbasisUnitLattice K. Note that, here and elsewhere, we identifyxwith its image inmixedSpace Kgiven bymixedSpaceOfRealSpace x.In order to describe the inverse image in
realSpace Kof thefundamentalDomainofbasisUnitLattice K, we define the mapexpMap : realSpace K → realSpace Kthat is, in some way, the right inverse oflogMap, seelogMap_expMap.Denote by
ηᵢ(withi ≠ w₀wherew₀is the distinguished infinite place, see the description oflogSpacebelow) the fundamental system of units given byfundSystemand let|ηᵢ|denotenormAtAllPlaces (mixedEmbedding ηᵢ)), that is the vector(w (ηᵢ))_winrealSpace K. Then, the image of|ηᵢ|byexpMap.symmform a basis of the subspace{x : realSpace K | ∑ w, x w = 0}. We complete by adding the vector(mult w)_wto get a basis, calledcompleteBasis, ofrealSpace K. The basiscompleteBasis Khas the property that, fori ≠ w₀, the image ofcompleteBasis K iby the natural restriction maprealSpace K → logSpace KisbasisUnitLattice K.At this point, we can construct the map
expMapBasisthat plays a crucial part in the proof. It is the map that sendsx : realSpace KtoReal.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i, seeexpMapBasis_apply'. Then, we prove a change of variable formula forexpMapBasis, seesetLIntegral_expMapBasis_image.
Spaces and maps #
To help understand the proof, we make a list of (almost) all the spaces and maps used and
their connections (as hinted above, we do not mention the map mixedSpaceOfRealSpace since we
identify realSpace K with its image in mixedSpace K).
mixedSpace: the set({w // IsReal w} → ℝ) × (w // IsComplex w → ℂ)wherewdenote the infinite places ofK.realSpace: the setw → ℝwherewdenote the infinite places ofKlogSpace: the set{w // w ≠ w₀} → ℝwherew₀is a distinguished place ofK. It is the set used in the proof of Dirichlet Unit Theorem.mixedEmbedding : K → mixedSpace K: the map that sendsx : Ktoφ_w(x)where, for all infinite placew,φ_w : K → ℝorℂ, resp. ifwis real or ifwis complex, denote a complex embedding associated tow.logEmbedding : (𝓞 K)ˣ → logSpace K: the map that sends the unitu : (𝓞 K)ˣto(mult w * log (w u))_wforw ≠ w₀. Its image isunitLattice K, aℤ-lattice oflogSpace K, that admitsbasisUnitLattice Kas a basis.logMap : mixedSpace K → logSpace K: this map is defined such that it factorslogEmbedding, that is, foru : (𝓞 K)ˣ,logMap (mixedEmbedding x) = logEmbedding x, and thatlogMap (c • x) = logMap xforc ≠ 0andnorm x ≠ 0. The inverse image of the fundamental domain ofbasisUnitLattice KbylogMap(minus the elements of norm zero) isfundamentalCone K.expMap : realSpace K → realSpace K: the right inverse oflogMapin the sense thatlogMap (expMap x) = (x_w)_{w ≠ w₀}.expMapBasis : realSpace K → realSpace K: the map that sendsx : realSpace KtoReal.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x iwhere|ηᵢ|denote the vector ofrealSpace Kgiven byw (ηᵢ)andηᵢdenote the units infundSystem K.
The set of elements of the fundamentalCone of norm ≤ 1.
Equations
Instances For
The component of expMap at the place w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The derivative of expMap_single, see hasDerivAt_expMap_single.
Equations
Instances For
The map from realSpace K → realSpace K whose components is given by expMap_single. It is, in
some respect, a right inverse of logMap, see logMap_expMap.
Equations
Instances For
A fixed equiv between Fin (rank K) and {w : InfinitePlace K // w ≠ w₀}.
Instances For
A family of elements in the realSpace K formed of the image of the fundamental units
and the vector (mult w)_w. This family is in fact a basis of realSpace K, see completeBasis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An auxiliary map from realSpace K to logSpace K used to prove that completeFamily is
linearly independent, see linearIndependent_completeFamily.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A basis of realSpace K formed by the image of the fundamental units
(which form a basis of a subspace {x : realSpace K | ∑ w, x w = 0}) and the vector (mult w)_w.
For i ≠ w₀, the image of completeBasis K i by the natural restriction map
realSpace K → logSpace K is basisUnitLattice K
Equations
Instances For
The map that sends x : realSpace K to
Real.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i where |ηᵢ| denote the vector of realSpace K given
by w (ηᵢ) and ηᵢ denote the units in fundSystem K, see expMapBasis_apply'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The derivative of expMapBasis, see hasFDerivAt_expMapBasis.
Equations
- One or more equations did not get rendered due to their size.