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

source
instance NumberField.mixedEmbedding.unitSMul (K : Type u_1) [Field K] :
SMul (RingOfIntegers K)หฃ (mixedSpace K)

The action of (๐“ž K)หฃ on the mixed space โ„^rโ‚ ร— โ„‚^rโ‚‚ defined, for u : (๐“ž K)หฃ, by multiplication component by component with mixedEmbedding K u.

Equations
    source
    @[simp]
    theorem NumberField.mixedEmbedding.unitSMul_smul (K : Type u_1) [Field K] (u : (RingOfIntegers K)หฃ) (x : mixedSpace K) :
    u โ€ข x = (mixedEmbedding K) ((algebraMap (RingOfIntegers K) K) โ†‘u) * x
    source
    instance NumberField.mixedEmbedding.instMulActionUnitsRingOfIntegersMixedSpace (K : Type u_1) [Field K] :
    MulAction (RingOfIntegers K)หฃ (mixedSpace K)
    Equations
      source
      instance NumberField.mixedEmbedding.instSMulZeroClassUnitsRingOfIntegersMixedSpace (K : Type u_1) [Field K] :
      SMulZeroClass (RingOfIntegers K)หฃ (mixedSpace K)
      Equations
        source
        theorem NumberField.mixedEmbedding.unit_smul_eq_zero {K : Type u_1} [Field K] (u : (RingOfIntegers K)หฃ) (x : mixedSpace K) :
        u โ€ข x = 0 โ†” x = 0
        source
        theorem NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq {K : Type u_1} [Field K] [NumberField K] {x y : RingOfIntegers K} {u : (RingOfIntegers K)หฃ} :
        u โ€ข (mixedEmbedding K) โ†‘x = (mixedEmbedding K) โ†‘y โ†” โ†‘u * x = y
        source
        theorem NumberField.mixedEmbedding.norm_unit_smul {K : Type u_1} [Field K] [NumberField K] (u : (RingOfIntegers K)หฃ) (x : mixedSpace K) :
        mixedEmbedding.norm (u โ€ข x) = mixedEmbedding.norm x
        source
        def NumberField.mixedEmbedding.logMap {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) :
        Units.dirichletUnitTheorem.logSpace K

        The map from the mixed space to logSpace K 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
            source
            @[simp]
            theorem NumberField.mixedEmbedding.logMap_apply {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) (w : { w : InfinitePlace K // w โ‰  Units.dirichletUnitTheorem.wโ‚€ }) :
            logMap x w = โ†‘(โ†‘w).mult * (Real.log ((normAtPlace โ†‘w) x) - Real.log (mixedEmbedding.norm x) * (โ†‘(Module.finrank โ„š K))โปยน)
            source
            @[simp]
            theorem NumberField.mixedEmbedding.logMap_zero {K : Type u_1} [Field K] [NumberField K] :
            logMap 0 = 0
            source
            @[simp]
            theorem NumberField.mixedEmbedding.logMap_one {K : Type u_1} [Field K] [NumberField K] :
            logMap 1 = 0
            source
            theorem NumberField.mixedEmbedding.logMap_mul {K : Type u_1} [Field K] [NumberField K] {x y : mixedSpace K} (hx : mixedEmbedding.norm x โ‰  0) (hy : mixedEmbedding.norm y โ‰  0) :
            logMap (x * y) = logMap x + logMap y
            source
            theorem NumberField.mixedEmbedding.logMap_apply_of_norm_one {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : mixedEmbedding.norm x = 1) (w : { w : InfinitePlace K // w โ‰  Units.dirichletUnitTheorem.wโ‚€ }) :
            logMap x w = โ†‘(โ†‘w).mult * Real.log ((normAtPlace โ†‘w) x)
            source
            @[simp]
            theorem NumberField.mixedEmbedding.logMap_eq_logEmbedding {K : Type u_1} [Field K] [NumberField K] (u : (RingOfIntegers K)หฃ) :
            logMap ((mixedEmbedding K) ((algebraMap (RingOfIntegers K) K) โ†‘u)) = (Units.logEmbedding K) (Additive.ofMul u)
            source
            theorem NumberField.mixedEmbedding.logMap_unit_smul {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (u : (RingOfIntegers K)หฃ) (hx : mixedEmbedding.norm x โ‰  0) :
            logMap (u โ€ข x) = (Units.logEmbedding K) (Additive.ofMul u) + logMap x
            source
            theorem NumberField.mixedEmbedding.logMap_torsion_smul {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) {ฮถ : (RingOfIntegers K)หฃ} (hฮถ : ฮถ โˆˆ Units.torsion K) :
            logMap (ฮถ โ€ข x) = logMap x
            source
            theorem NumberField.mixedEmbedding.logMap_real {K : Type u_1} [Field K] [NumberField K] (c : โ„) :
            logMap (c โ€ข 1) = 0
            source
            theorem NumberField.mixedEmbedding.logMap_real_smul {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : mixedEmbedding.norm x โ‰  0) {c : โ„} (hc : c โ‰  0) :
            logMap (c โ€ข x) = logMap x
            source
            theorem NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq {K : Type u_1} [Field K] [NumberField K] {x y : mixedSpace K} (h : โˆ€ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y) :
            logMap x = logMap y
            source
            def NumberField.mixedEmbedding.fundamentalCone (K : Type u_1) [Field K] [NumberField K] :
            Set (mixedSpace K)

            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
              Instances For
                source
                theorem NumberField.mixedEmbedding.measurableSet_fundamentalCone (K : Type u_1) [Field K] [NumberField K] :
                MeasurableSet (fundamentalCone K)
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : x โˆˆ fundamentalCone K) :
                0 < mixedEmbedding.norm x
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : x โˆˆ fundamentalCone K) (w : InfinitePlace K) :
                0 < (normAtPlace w) x
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.mem_of_normAtPlace_eq {K : Type u_1} [Field K] [NumberField K] {x y : mixedSpace K} (hx : x โˆˆ fundamentalCone K) (hy : โˆ€ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x) :
                y โˆˆ fundamentalCone K
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} {c : โ„} (hx : x โˆˆ fundamentalCone K) (hc : c โ‰  0) :
                c โ€ข x โˆˆ fundamentalCone K
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} {c : โ„} (hc : c โ‰  0) :
                c โ€ข x โˆˆ fundamentalCone K โ†” x โˆˆ fundamentalCone K
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.exists_unit_smul_mem {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : mixedEmbedding.norm x โ‰  0) :
                โˆƒ (u : (RingOfIntegers K)หฃ), u โ€ข x โˆˆ fundamentalCone K
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : x โˆˆ fundamentalCone K) {ฮถ : (RingOfIntegers K)หฃ} (hฮถ : ฮถ โˆˆ Units.torsion K) :
                ฮถ โ€ข x โˆˆ fundamentalCone K
                source
                theorem NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : x โˆˆ fundamentalCone K) (u : (RingOfIntegers K)หฃ) :
                u โ€ข x โˆˆ fundamentalCone K โ†” u โˆˆ Units.torsion K
                source
                def NumberField.mixedEmbedding.fundamentalCone.integerSet (K : Type u_1) [Field K] [NumberField K] :
                Set (mixedSpace K)

                The intersection between the fundamental cone and the integerLattice.

                Equations
                  Instances For
                    source
                    theorem NumberField.mixedEmbedding.fundamentalCone.mem_integerSet {K : Type u_1} [Field K] [NumberField K] {a : mixedSpace K} :
                    a โˆˆ integerSet K โ†” a โˆˆ fundamentalCone K โˆง โˆƒ (x : RingOfIntegers K), (mixedEmbedding K) โ†‘x = a
                    source
                    theorem NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet {K : Type u_1} [Field K] [NumberField K] {a : mixedSpace K} (ha : a โˆˆ integerSet K) :
                    โˆƒ! x : RingOfIntegers K, (mixedEmbedding K) โ†‘x = a

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

                    source
                    theorem NumberField.mixedEmbedding.fundamentalCone.ne_zero_of_mem_integerSet {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                    โ†‘a โ‰  0
                    source
                    def NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                    โ†ฅ(nonZeroDivisors (RingOfIntegers K))

                    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
                        source
                        @[simp]
                        theorem NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                        (mixedEmbedding K) โ†‘โ†‘(preimageOfMemIntegerSet a) = โ†‘a
                        source
                        theorem NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} (hx : (mixedEmbedding K) โ†‘x โˆˆ integerSet K) :
                        โ†‘(preimageOfMemIntegerSet โŸจ(mixedEmbedding K) โ†‘x, hxโŸฉ) = x
                        source
                        theorem NumberField.mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integerSet {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} (hx : x โ‰  0) (hx' : x โˆˆ โ‡‘(mixedEmbedding K) '' Set.range โ‡‘(algebraMap (RingOfIntegers K) K)) :
                        โˆƒ (u : (RingOfIntegers K)หฃ), u โ€ข x โˆˆ integerSet K

                        If x : mixedSpace K is nonzero and the image of an algebraic integer, then there exists a unit such that u โ€ข x โˆˆ integerSet K.

                        source
                        theorem NumberField.mixedEmbedding.fundamentalCone.torsion_unitSMul_mem_integerSet {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} {ฮถ : (RingOfIntegers K)หฃ} (hฮถ : ฮถ โˆˆ Units.torsion K) (hx : x โˆˆ integerSet K) :
                        ฮถ โ€ข x โˆˆ integerSet K

                        The set integerSet K is stable under the action of the torsion.

                        source
                        instance NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul {K : Type u_1} [Field K] [NumberField K] :
                        SMul โ†ฅ(Units.torsion K) โ†‘(integerSet K)

                        The action of torsion K on integerSet K.

                        Equations
                          source
                          @[simp]
                          theorem NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe {K : Type u_1} [Field K] [NumberField K] (xโœ : โ†ฅ(Units.torsion K)) (xโœยน : โ†‘(integerSet K)) :
                          โ†‘(xโœ โ€ข xโœยน) = โ†‘xโœ โ€ข โ†‘xโœยน
                          source
                          instance NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet {K : Type u_1} [Field K] [NumberField K] :
                          MulAction โ†ฅ(Units.torsion K) โ†‘(integerSet K)
                          Equations
                            source
                            def NumberField.mixedEmbedding.fundamentalCone.intNorm {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                            โ„•

                            The mixedEmbedding.norm of a : integerSet K as a natural number, see also intNorm_coe.

                            Equations
                              Instances For
                                source
                                @[simp]
                                theorem NumberField.mixedEmbedding.fundamentalCone.intNorm_coe {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                โ†‘(intNorm a) = mixedEmbedding.norm โ†‘a
                                source
                                def NumberField.mixedEmbedding.fundamentalCone.quotIntNorm {K : Type u_1} [Field K] [NumberField K] :
                                Quotient (MulAction.orbitRel โ†ฅ(Units.torsion K) โ†‘(integerSet K)) โ†’ โ„•

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

                                Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                    quotIntNorm โŸฆaโŸง = intNorm a
                                    source
                                    def NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates (K : Type u_1) [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                    Associates โ†ฅ(nonZeroDivisors (RingOfIntegers K))

                                    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
                                        source
                                        @[simp]
                                        theorem NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_apply {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                        integerSetToAssociates K a = โŸฆpreimageOfMemIntegerSet aโŸง
                                        source
                                        theorem NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_surjective (K : Type u_1) [Field K] [NumberField K] :
                                        Function.Surjective (integerSetToAssociates K)
                                        source
                                        theorem NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff {K : Type u_1} [Field K] [NumberField K] (a b : โ†‘(integerSet K)) :
                                        integerSetToAssociates K a = integerSetToAssociates K b โ†” โˆƒ (ฮถ : โ†ฅ(Units.torsion K)), ฮถ โ€ข a = b
                                        source
                                        def NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates (K : Type u_1) [Field K] [NumberField K] :
                                        Quotient (MulAction.orbitRel โ†ฅ(Units.torsion K) โ†‘(integerSet K)) โ‰ƒ Associates โ†ฅ(nonZeroDivisors (RingOfIntegers K))

                                        The equivalence between integerSet K modulo torsion K and Associates (๐“ž K)โฐ.

                                        Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                            (integerSetQuotEquivAssociates K) โŸฆaโŸง = โŸฆpreimageOfMemIntegerSet aโŸง
                                            source
                                            theorem NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                            MulAction.stabilizer (โ†ฅ(Units.torsion K)) a = โŠฅ
                                            source
                                            def NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv (K : Type u_1) [Field K] [NumberField K] :
                                            โ†‘(integerSet K) โ‰ƒ { I : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K))) // Submodule.IsPrincipal โ†‘I } ร— โ†ฅ(Units.torsion K)

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

                                            Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst {K : Type u_1} [Field K] [NumberField K] (a : โ†‘(integerSet K)) :
                                                โ†‘โ†‘((integerSetEquiv K) a).1 = Ideal.span {โ†‘(preimageOfMemIntegerSet a)}
                                                source
                                                def NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm (K : Type u_1) [Field K] [NumberField K] (n : โ„•) :
                                                { a : โ†‘(integerSet K) // mixedEmbedding.norm โ†‘a = โ†‘n } โ‰ƒ { I : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K))) // Submodule.IsPrincipal โ†‘I โˆง Ideal.absNorm โ†‘I = n } ร— โ†ฅ(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
                                                  Instances For
                                                    source
                                                    @[simp]
                                                    theorem NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst {K : Type u_1} [Field K] [NumberField K] {n : โ„•} (a : { a : โ†‘(integerSet K) // mixedEmbedding.norm โ†‘a = โ†‘n }) :
                                                    โ†‘โ†‘((integerSetEquivNorm K n) a).1 = Ideal.span {โ†‘(preimageOfMemIntegerSet โ†‘a)}
                                                    source
                                                    theorem NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion (K : Type u_1) [Field K] [NumberField K] (n : โ„•) :
                                                    Nat.card โ†‘{I : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K))) | Submodule.IsPrincipal โ†‘I โˆง Ideal.absNorm โ†‘I = n} * Units.torsionOrder K = Nat.card โ†‘{a : โ†‘(integerSet K) | 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.

                                                    source
                                                    def NumberField.mixedEmbedding.fundamentalCone.idealSet (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) :
                                                    Set (mixedSpace K)

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

                                                    Equations
                                                      Instances For
                                                        source
                                                        theorem NumberField.mixedEmbedding.fundamentalCone.mem_idealSet {K : Type u_1} [Field K] [NumberField K] {x : mixedSpace K} {J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))} :
                                                        x โˆˆ idealSet K J โ†” x โˆˆ fundamentalCone K โˆง โˆƒ a โˆˆ โ†‘โ†‘J, (mixedEmbedding K) โ†‘a = x
                                                        source
                                                        def NumberField.mixedEmbedding.fundamentalCone.idealSetMap (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) :
                                                        โ†‘(idealSet K J) โ†’ โ†‘(integerSet K)

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

                                                        Equations
                                                          Instances For
                                                            source
                                                            @[simp]
                                                            theorem NumberField.mixedEmbedding.fundamentalCone.idealSetMap_apply (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : โ†‘(idealSet K J)) :
                                                            โ†‘(idealSetMap K J a) = โ†‘a
                                                            source
                                                            theorem NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : โ†‘(idealSet K J)) :
                                                            โ†‘(preimageOfMemIntegerSet (idealSetMap K J a)) โˆˆ โ†‘โ†‘J
                                                            source
                                                            def NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) :
                                                            โ†‘(idealSet K J) โ‰ƒ โ†‘{a : โ†‘(integerSet K) | โ†‘(preimageOfMemIntegerSet a) โˆˆ โ†‘โ†‘J}

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

                                                            Equations
                                                              Instances For
                                                                source
                                                                theorem NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply {K : Type u_1} [Field K] [NumberField K] {J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))} (a : โ†‘(idealSet K J)) :
                                                                โ†‘โ†‘((idealSetEquiv K J) a) = โ†‘a
                                                                source
                                                                theorem NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] {J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))} (a : { a : โ†‘(integerSet K) // โ†‘(preimageOfMemIntegerSet a) โˆˆ โ†‘โ†‘J }) :
                                                                โ†‘((idealSetEquiv K J).symm a) = โ†‘โ†‘a
                                                                source
                                                                theorem NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply {K : Type u_1} [Field K] [NumberField K] {J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))} (a : โ†‘(idealSet K J)) :
                                                                โ†‘(intNorm โ†‘((idealSetEquiv K J) a)) = mixedEmbedding.norm โ†‘a
                                                                source
                                                                def NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : โ„•) :
                                                                { a : โ†‘(idealSet K J) // mixedEmbedding.norm โ†‘a = โ†‘n } โ‰ƒ { I : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K))) // โ†‘J โˆฃ โ†‘I โˆง Submodule.IsPrincipal โ†‘I โˆง Ideal.absNorm โ†‘I = n } ร— โ†ฅ(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
                                                                  Instances For
                                                                    source
                                                                    theorem NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le (K : Type u_1) [Field K] [NumberField K] (J : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : โ„) :
                                                                    Nat.card { I : โ†ฅ(nonZeroDivisors (Ideal (RingOfIntegers K))) // โ†‘J โˆฃ โ†‘I โˆง Submodule.IsPrincipal โ†‘I โˆง โ†‘(Ideal.absNorm โ†‘I) โ‰ค s } * Units.torsionOrder K = Nat.card { a : โ†‘(idealSet K J) // 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.