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 it 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 K
is 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≤ 1
and such thatlogMap x
is in thefundamentalDomain
ofbasisUnitLattice K
. Note that, here and elsewhere, we identifyx
with its image inmixedSpace K
given bymixedSpaceOfRealSpace x
.In order to describe the inverse image in
realSpace K
of thefundamentalDomain
ofbasisUnitLattice K
, we define the mapexpMap : realSpace K → realSpace K
that is, in some way, the right inverse oflogMap
, seelogMap_expMap
.Denote by
ηᵢ
(withi ≠ w₀
wherew₀
is the distinguished infinite place, see the description oflogSpace
below) the fundamental system of units given byfundSystem
and let|ηᵢ|
denotenormAtAllPlaces (mixedEmbedding ηᵢ))
, that is the vector(w (ηᵢ))_w
inrealSpace K
. Then, the image of|ηᵢ|
byexpMap.symm
form a basis of the subspace{x : realSpace K | ∑ w, x w = 0}
. We complete by adding the vector(mult w)_w
to get a basis, calledcompleteBasis
, ofrealSpace K
. The basiscompleteBasis K
has the property that, fori ≠ w₀
, the image ofcompleteBasis K i
by the natural restriction maprealSpace K → logSpace K
isbasisUnitLattice K
.At this point, we can construct the map
expMapBasis
that plays a crucial part in the proof. It is the map that sendsx : realSpace K
toReal.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i
, seeexpMapBasis_apply'
. Then, we prove a change of variable formula forexpMapBasis
, seesetLIntegral_expMapBasis_image
.We define a set
paramSet
inrealSpace K
and prove thatnormAtAllPlaces '' (normLeOne K) = expMapBasis (paramSet K)
, seenormAtAllPlaces_normLeOne_eq_image
. Using this,setLIntegral_expMapBasis_image
and the results frommixedEmbedding.polarCoord
, we can then compute the volume ofnormLeOne K
, seevolume_normLeOne
.Finally, we need to prove that the frontier of
normLeOne K
has zero-volume (we will prove in passing thatnormLeOne K
is bounded.) For that we prove thatvolume (interior (normLeOne K)) = volume (closure (normLeOne K))
, seevolume_interior_eq_volume_closure
. Since we now that the volume ofinterior (normLeOne K)
is finite since it is bounded by the volume ofnormLeOne K
, the result follows, seevolume_frontier_normLeOne
. We proceed in several steps.
7.1. We prove first that
normAtAllPlaces⁻¹' (expMapBasis '' interior (paramSet K)) ⊆ interior (normLeOne K)
, see
subset_interior_normLeOne
(Note that here again we identify realSpace K
with its image
in mixedSpace K
). The main argument is that expMapBasis
is a partial homeomorphism
and that interior (paramSet K)
is a subset of its source, so its image by expMapBasis
is still open.
7.2. The same kind of argument does not work with closure (paramSet)
since it is not contained
in the source of expMapBasis
. So we define a compact set, called compactSet K
, such that
closure (normLeOne K) ⊆ normAtAllPlaces⁻¹' (compactSet K)
, see closure_normLeOne_subset
,
and it is almost equal to expMapBasis '' closure (paramSet K)
, see compactSet_ae
.
7.3. We get from the above that normLeOne K ⊆ normAtAllPlaces⁻¹' (compactSet K)
, from which
it follows easily that normLeOne K
is bounded, see isBounded_normLeOne
.
7.4. Finally, we prove that volume (normAtAllPlaces ⁻¹' compactSet K) = volume (normAtAllPlaces ⁻¹' (expMapBasis '' interior (paramSet K)))
, which implies that
volume (interior (normLeOne K)) = volume (closure (normLeOne K))
by the above and the fact
that volume (interior (normLeOne K)) ≤ volume (closure (normLeOne K))
, which boils down to
the fact that the interior and closure of paramSet K
are almost equal, see
closure_paramSet_ae_interior
.
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 → ℂ)
wherew
denote the infinite places ofK
.realSpace
: the setw → ℝ
wherew
denote the infinite places ofK
logSpace
: 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 : K
toφ_w(x)
where, for all infinite placew
,φ_w : K → ℝ
orℂ
, resp. ifw
is real or ifw
is complex, denote a complex embedding associated tow
.logEmbedding : (𝓞 K)ˣ → logSpace K
: the map that sends the unitu : (𝓞 K)ˣ
to(mult w * log (w u))_w
forw ≠ w₀
. Its image isunitLattice K
, aℤ
-lattice oflogSpace K
, that admitsbasisUnitLattice K
as 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 x
forc ≠ 0
andnorm x ≠ 0
. The inverse image of the fundamental domain ofbasisUnitLattice K
bylogMap
(minus the elements of norm zero) isfundamentalCone K
.expMap : realSpace K → realSpace K
: the right inverse oflogMap
in the sense thatlogMap (expMap x) = (x_w)_{w ≠ w₀}
.expMapBasis : realSpace K → realSpace K
: the map that sendsx : realSpace K
toReal.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i
where|ηᵢ|
denote the vector ofrealSpace K
given 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.
Instances For
The set that parametrizes normAtAllPlaces '' (normLeOne K)
, see
normAtAllPlaces_normLeOne_eq_image
.
Equations
Instances For
A compact set that contains expMapBasis '' closure (paramSet K)
and furthermore is almost
equal to it, see compactSet_ae
.
Equations
- One or more equations did not get rendered due to their size.