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
  • One or more equations did not get rendered due to their size.
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) :
{ w : InfinitePlace K // w โ‰  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
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      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
        @[deprecated NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet (since := "2024-12-17")]
        theorem NumberField.mixedEmbedding.fundamentalCone.exists_unique_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

        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.

        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
          • One or more equations did not get rendered due to their size.
          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
            • One or more equations did not get rendered due to their size.
            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
                  • One or more equations did not get rendered due to their size.
                  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
                    • One or more equations did not get rendered due to their size.
                    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
                          • One or more equations did not get rendered due to their size.
                          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
                            • One or more equations did not get rendered due to their size.
                            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.