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][marcus1977number].

since NormLeOne K is norm-stable, in the sense that normLeOne K = normAtAllPlaces⁻¹' (normAtAllPlaces '' (normLeOne K)), see normLeOne_eq_primeage_image, it's enough to study the subset normAtAllPlaces '' (normLeOne K) of realSpace K.
A description of normAtAllPlaces '' (normLeOne K) is given by normAtAllPlaces_normLeOne, it is the set of x : realSpace K, nonnegative at all places, whose norm is nonzero and ≤ 1 and such that logMap x is in the fundamentalDomain of basisUnitLattice K. Note that, here and elsewhere, we identify x with its image in mixedSpace K given by mixedSpaceOfRealSpace x.
In order to describe the inverse image in realSpace K of the fundamentalDomain of basisUnitLattice K, we define the map expMap : realSpace K → realSpace K that is, in some way, the right inverse of logMap, see logMap_expMap.

source

theorem NumberField.mixedEmbedding.logMap_normAtAllPlaces {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) :

logMap (mixedSpaceOfRealSpace (normAtAllPlaces x)) = logMap x

source

theorem NumberField.mixedEmbedding.norm_normAtAllPlaces {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) :

mixedEmbedding.norm (mixedSpaceOfRealSpace (normAtAllPlaces x)) = mixedEmbedding.norm x

source

theorem NumberField.mixedEmbedding.normAtAllPlaces_mem_fundamentalCone_iff {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} :

mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

source

@[reducible, inline]

abbrev NumberField.mixedEmbedding.normLeOne (K : Type u_1) [Field K] [NumberField K] :

Set (mixedSpace K)

The set of elements of the fundamentalCone of norm ≤ 1.

Equations

NumberField.mixedEmbedding.normLeOne K = {x : NumberField.mixedEmbedding.mixedSpace K | x ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ NumberField.mixedEmbedding.norm x ≤ 1}

Instances For

source

theorem NumberField.mixedEmbedding.mem_normLeOne {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} :

x ∈ normLeOne K ↔ x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1

source

theorem NumberField.mixedEmbedding.normLeOne_eq_primeage_image (K : Type u_1) [Field K] [NumberField K] :

normLeOne K = normAtAllPlaces ⁻¹' (normAtAllPlaces '' normLeOne K)

source

theorem NumberField.mixedEmbedding.normAtAllPlaces_normLeOne (K : Type u_1) [Field K] [NumberField K] :

normAtAllPlaces '' normLeOne K = ⇑mixedSpaceOfRealSpace ⁻¹' (logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (Units.unitLattice K) (Units.basisUnitLattice K))) ∩ {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩ {x : realSpace K | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0} ∩ {x : realSpace K | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}

source

def NumberField.mixedEmbedding.expMap_single {K : Type u_1} [Field K] (w : InfinitePlace K) :

PartialHomeomorph ℝ ℝ

The component of expMap at the place w.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem NumberField.mixedEmbedding.expMap_single_source {K : Type u_1} [Field K] (w : InfinitePlace K) :

(expMap_single w).source = Set.univ

source

@[simp]

theorem NumberField.mixedEmbedding.expMap_single_target {K : Type u_1} [Field K] (w : InfinitePlace K) :

(expMap_single w).target = Set.Ioi 0

source

@[simp]

theorem NumberField.mixedEmbedding.expMap_single_apply {K : Type u_1} [Field K] (w : InfinitePlace K) (x : ℝ) :

↑(expMap_single w) x = Real.exp ((↑w.mult)⁻¹ * x)

source

@[simp]

theorem NumberField.mixedEmbedding.expMap_single_symm_apply {K : Type u_1} [Field K] (w : InfinitePlace K) (x : ℝ) :

↑(expMap_single w).symm x = ↑w.mult * Real.log x

source

def NumberField.mixedEmbedding.expMap {K : Type u_1} [Field K] [NumberField K] :

PartialHomeomorph (realSpace K) (realSpace K)

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