Documentation

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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.

  1. 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.

  2. 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.

  3. 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.

  4. Denote by ηᵢ (with i ≠ w₀ where w₀ is the distinguished infinite place, see the description of logSpace below) the fundamental system of units given by fundSystem and let |ηᵢ| denote normAtAllPlaces (mixedEmbedding ηᵢ)), that is the vector (w (ηᵢ))_w in realSpace K. Then, the image of |ηᵢ| by expMap.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, called completeBasis, of realSpace K. The basis completeBasis K has the property that, for i ≠ w₀, the image of completeBasis K i by the natural restriction map realSpace K → logSpace K is basisUnitLattice K.

  5. At this point, we can construct the map expMapBasis that plays a crucial part in the proof. It is the map that sends x : realSpace K to Real.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i, see expMapBasis_apply'. Then, we prove a change of variable formula for expMapBasis, see setLIntegral_expMapBasis_image.

  6. We define a set paramSet in realSpace K and prove that normAtAllPlaces '' (normLeOne K) = expMapBasis (paramSet K), see normAtAllPlaces_normLeOne_eq_image. Using this, setLIntegral_expMapBasis_image and the results from mixedEmbedding.polarCoord, we can then compute the volume of normLeOne K, see volume_normLeOne.

  7. Finally, we need to prove that the frontier of normLeOne K has zero-volume (we will prove in passing that normLeOne K is bounded.) For that we prove that volume (interior (normLeOne K)) = volume (closure (normLeOne K)), see volume_interior_eq_volume_closure. Since we now that the volume of interior (normLeOne K) is finite since it is bounded by the volume of normLeOne K, the result follows, see volume_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).

The component of expMap at the place w.

Equations
  • One or more equations did not get rendered due to their size.
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
      theorem NumberField.mixedEmbedding.fundamentalCone.expMap_sum {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (f : ιrealSpace K) :
      expMap (∑ is, f i) = is, expMap (f i)
      @[reducible, inline]

      The derivative of expMap, see hasFDerivAt_expMap.

      Equations
      • One or more equations did not get rendered due to their size.
      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
                @[reducible, inline]

                The derivative of expMapBasis, see hasFDerivAt_expMapBasis.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[reducible, inline]

                  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.
                  Instances For