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_mul {K : Type u_1} [Field K] [NumberField K] {x y : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x โ‰  0) (hy : NumberField.mixedEmbedding.norm y โ‰  0) :
    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 in integerSet, then there is a unique algebraic integer in ๐“ž K such that mixedEmbedding K x = a.

      @[deprecated NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet]

      Alias of NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet.


      If a is in integerSet, then there is a unique algebraic integer in ๐“ž K such that mixedEmbedding K x = a.

      For a : integerSet 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 integerSetEquiv.

      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 โˆˆ integerSet K.

        The action of torsion K on integerSet K.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe {K : Type u_1} [Field K] [NumberField K] (xโœ : โ†ฅ(NumberField.Units.torsion K)) (xโœยน : โ†‘(NumberField.mixedEmbedding.fundamentalCone.integerSet K)) :
        โ†‘(xโœ โ€ข xโœยน) = โ†‘xโœ โ€ข โ†‘xโœยน
        Equations
        • NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet = MulAction.mk โ‹ฏ โ‹ฏ

        The norm intNorm lifts to a function on integerSet 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 : integerSet 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 integerSetQuotEquivAssociates.

          Equations
          Instances For

            The equivalence between integerSet 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
              def NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm (K : Type u_1) [Field K] [NumberField K] (n : โ„•) :
              { a : โ†‘(NumberField.mixedEmbedding.fundamentalCone.integerSet K) // NumberField.mixedEmbedding.norm โ†‘a = โ†‘n } โ‰ƒ { I : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // Submodule.IsPrincipal โ†‘I โˆง Ideal.absNorm โ†‘I = n } ร— โ†ฅ(NumberField.Units.torsion K)

              For an integer n, The equivalence between the elements of integerSet 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
                theorem NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion (K : Type u_1) [Field K] [NumberField K] (n : โ„•) :
                Nat.card โ†‘{I : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | Submodule.IsPrincipal โ†‘I โˆง Ideal.absNorm โ†‘I = n} * โ†‘(NumberField.Units.torsionOrder K) = Nat.card โ†‘{a : โ†‘(NumberField.mixedEmbedding.fundamentalCone.integerSet K) | NumberField.mixedEmbedding.norm โ†‘a = โ†‘n}

                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 elements in integerSet K of norm n.

                The intersection between the fundamental cone and the idealLattice defined by the image of the integral ideal J.

                Equations
                Instances For

                  The map that sends a : idealSet to an element of integerSet. This map exists because J is an integral ideal.

                  Equations
                  Instances For

                    The map idealSetMap is actually an equiv between idealSet K J and the elements of integerSet K whose preimage lies in J.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (n : โ„•) :
                      { a : โ†‘(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) // NumberField.mixedEmbedding.norm โ†‘a = โ†‘n } โ‰ƒ { I : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // โ†‘J โˆฃ โ†‘I โˆง Submodule.IsPrincipal โ†‘I โˆง Ideal.absNorm โ†‘I = n } ร— โ†ฅ(NumberField.Units.torsion K)

                      For an integer n, The equivalence between the elements of idealSet K of norm n and the product of the set of nonzero principal ideals of K divisible by J of norm n and the torsion of K.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (s : โ„) :
                        Nat.card { I : โ†ฅ(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // โ†‘J โˆฃ โ†‘I โˆง Submodule.IsPrincipal โ†‘I โˆง โ†‘(Ideal.absNorm โ†‘I) โ‰ค s } * โ†‘(NumberField.Units.torsionOrder K) = Nat.card { a : โ†‘(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) // NumberField.mixedEmbedding.norm โ†‘a โ‰ค s }

                        For s : โ„, the number of principal nonzero ideals in ๐“ž K divisible par J of norm โ‰ค s multiplied by the order of the torsion of K is equal to the number of elements in idealSet K J of norm โ‰ค s.