Documentation

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Fundamental Cone #

Let K be a number field of signature (r₁, rβ‚‚). We define an action of the units (π“ž K)Λ£ on the mixed space ℝ^r₁ Γ— β„‚^rβ‚‚ via the mixedEmbedding. The fundamental cone is a cone in the mixed space that is a fundamental domain for the action of (π“ž K)Λ£ modulo torsion.

Main definitions and results #

Tags #

number field, canonical embedding, units, principal ideals

The action of (π“ž K)Λ£ on the mixed space ℝ^r₁ Γ— β„‚^rβ‚‚ defined, for u : (π“ž K)Λ£, by multiplication component by component with mixedEmbedding K u.

Equations
  • One or more equations did not get rendered due to their size.
theorem NumberField.mixedEmbedding.norm_unit_smul {K : Type u_1} [Field K] [NumberField K] (u : (NumberField.RingOfIntegers K)Λ£) (x : NumberField.mixedEmbedding.mixedSpace K) :
NumberField.mixedEmbedding.norm (u β€’ x) = NumberField.mixedEmbedding.norm x
def NumberField.mixedEmbedding.logMap {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K) :
{ w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ

The map from the mixed space to {w : InfinitePlace K // w β‰  wβ‚€} β†’ ℝ (with wβ‚€ the fixed place from the proof of Dirichlet Unit Theorem) defined in such way that: 1) it factors the map logEmbedding, see logMap_eq_logEmbedding; 2) it is constant on the sets {c β€’ x | c ∈ ℝ, c β‰  0} if norm x β‰  0, see logMap_real_smul.

Equations
Instances For
    @[simp]
    theorem NumberField.mixedEmbedding.logMap_apply {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) :
    NumberField.mixedEmbedding.logMap x w = ↑(↑w).mult * (Real.log ((NumberField.mixedEmbedding.normAtPlace ↑w) x) - Real.log (NumberField.mixedEmbedding.norm x) * (↑(Module.finrank β„š K))⁻¹)
    theorem NumberField.mixedEmbedding.logMap_apply_of_norm_one {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x = 1) (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) :

    The fundamental cone is a cone in the mixed space, ie. a subset fixed by multiplication by a nonzero real number, see smul_mem_of_mem, that is also a fundamental domain for the action of (π“ž K)Λ£ modulo torsion, see exists_unit_smul_mem and torsion_smul_mem_of_mem.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      If a is an integral point, then there is a unique algebraic integer in π“ž K such that mixedEmbedding K x = a.

      For a : fundamentalCone K, the unique nonzero algebraic integer x such that its image by mixedEmbedding is equal to a. Note that we state the fact that x β‰  0 by saying that x is a nonzero divisors since we will use later on the isomorphism Ideal.associatesNonZeroDivisorsEquivIsPrincipal, see integralPointEquiv.

      Equations
      Instances For

        If x : mixedSpace K is nonzero and the image of an algebraic integer, then there exists a unit such that u β€’ x ∈ integralPoint K.

        The action of torsion K on integralPoint K.

        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegralPoint = MulAction.mk β‹― β‹―

        The norm intNorm lifts to a function on integralPoint K modulo torsion K.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The map that sends an element of a : integralPoint K to the associates class of its preimage in (π“ž K)⁰. By quotienting by the kernel of the map, which is equal to the subgroup of torsion, we get the equivalence integralPointQuotEquivAssociates.

          Equations
          Instances For

            The equivalence between integralPoint K and the product of the set of nonzero principal ideals of K and the torsion of K.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              For an integer n, The equivalence between the integralPoint K of norm n and the product of the set of nonzero principal ideals of K of norm n and the torsion of K.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                For n positive, the number of principal ideals in π“ž K of norm n multiplied by the order of the torsion of K is equal to the number of integralPoint K of norm n.

                For s : ℝ, the number of principal nonzero ideals in π“ž K of norm ≀ s multiplied by the order of the torsion of K is equal to the number of integralPoint K of norm ≀ s.