Documentation

FLT3.Mathlib.NumberTheory.NumberField.Units

Units of a number field #

We prove results about the group (π“ž K)Λ£ of units of the ring of integers π“ž K of a number field K.

Main definitions #

Main results #

Tags #

number field, units

theorem NumberField.Units.coe_injective (K : Type u_1) [Field K] :
Function.Injective fun (x : (β†₯(NumberField.ringOfIntegers K))Λ£) => ↑↑x
theorem NumberField.Units.coe_mul {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (y : (β†₯(NumberField.ringOfIntegers K))Λ£) :
↑↑(x * y) = ↑↑x * ↑↑y
theorem NumberField.Units.coe_pow {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (n : β„•) :
↑↑(x ^ n) = ↑↑x ^ n
theorem NumberField.Units.coe_zpow {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (n : β„€) :
↑↑(x ^ n) = ↑↑x ^ n
theorem NumberField.Units.coe_one {K : Type u_1} [Field K] :
↑↑1 = 1
theorem NumberField.Units.coe_neg_one {K : Type u_1} [Field K] :
↑↑(-1) = -1
theorem NumberField.Units.coe_ne_zero {K : Type u_1} [Field K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) :
↑↑x β‰  0

The torsion subgroup of the group of units.

Equations
Instances For

    The order of the torsion subgroup as a positive integer.

    Equations
    Instances For

      If k does not divide torsionOrder then there are no nontrivial roots of unity of order dividing k.

      The group of roots of unity of order dividing torsionOrder is equal to the torsion group.

      Dirichlet Unit Theorem #

      This section is devoted to the proof of Dirichlet's unit theorem.

      We define a group morphism from (π“ž K)Λ£ to {w : InfinitePlace K // w β‰  wβ‚€} β†’ ℝ where wβ‚€ is a distinguished (arbitrary) infinite place, prove that its kernel is the torsion subgroup (see logEmbedding_eq_zero_iff) and that its image, called unitLattice, is a full β„€-lattice. It follows that unitLattice is a free β„€-module (see instModuleFree_unitLattice) of rank card (InfinitePlaces K) - 1 (see unitLattice_rank). To prove that the unitLattice is a full β„€-lattice, we need to prove that it is discrete (see unitLattice_inter_ball_finite) and that it spans the full space over ℝ (see unitLattice_span_eq_top); this is the main part of the proof, see the section span_top below for more details.

      The distinguished infinite place.

      Equations
      • NumberField.Units.dirichletUnitTheorem.wβ‚€ = Nonempty.some β‹―
      Instances For
        def NumberField.Units.dirichletUnitTheorem.logEmbedding (K : Type u_1) [Field K] [NumberField K] :
        Additive (β†₯(NumberField.ringOfIntegers K))Λ£ β†’+ { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ

        The logarithmic embedding of the units (seen as an Additive group).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component {K : Type u_1} [Field K] [NumberField K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) :
          theorem NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component {K : Type u_1} [Field K] [NumberField K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) :
          (Finset.sum Finset.univ fun (w : { w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ }) => (NumberField.Units.dirichletUnitTheorem.logEmbedding K) x w) = -↑(NumberField.InfinitePlace.mult NumberField.Units.dirichletUnitTheorem.wβ‚€) * Real.log (NumberField.Units.dirichletUnitTheorem.wβ‚€ ↑↑x)
          noncomputable def NumberField.Units.unitLattice (K : Type u_1) [Field K] [NumberField K] :
          AddSubgroup ({ w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ)

          The lattice formed by the image of the logarithmic embedding.

          Equations
          Instances For

            Section span_top #

            In this section, we prove that the span over ℝ of the unitLattice is equal to the full space. For this, we construct for each infinite place w₁ β‰  wβ‚€ a unit u_w₁ of K such that, for all infinite places w such that w β‰  w₁, we have Real.log w (u_w₁) < 0 (and thus Real.log w₁ (u_w₁) > 0). It follows then from a determinant computation (using Matrix.det_ne_zero_of_sum_col_lt_diag) that the image by logEmbedding of these units is a ℝ-linearly independent family. The unit u_w₁ is obtained by constructing a sequence seq n of nonzero algebraic integers that is strictly decreasing at infinite places distinct from w₁ and of norm ≀ B. Since there are finitely many ideals of norm ≀ B, there exists two term in the sequence defining the same ideal and their quotient is the desired unit u_w₁ (see exists_unit).

            theorem NumberField.Units.dirichletUnitTheorem.seq_next (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : β„•} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) {x : β†₯(NumberField.ringOfIntegers K)} (hx : x β‰  0) :
            βˆƒ (y : β†₯(NumberField.ringOfIntegers K)), y β‰  0 ∧ (βˆ€ (w : NumberField.InfinitePlace K), w β‰  w₁ β†’ w ↑y < w ↑x) ∧ |(Algebra.norm β„š) ↑y| ≀ ↑B

            This result shows that there always exists a next term in the sequence.

            An infinite sequence of nonzero algebraic integers of K satisfying the following properties: β€’ seq n is nonzero; β€’ for w : InfinitePlace K, w β‰  w₁ β†’ w (seq n+1) < w (seq n); β€’ ∣norm (seq n)∣ ≀ B.

            Equations
            Instances For

              The sequence is strictly decreasing at infinite places distinct from w₁.

              theorem NumberField.Units.dirichletUnitTheorem.exists_unit (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) :
              βˆƒ (u : (β†₯(NumberField.ringOfIntegers K))Λ£), βˆ€ (w : NumberField.InfinitePlace K), w β‰  w₁ β†’ Real.log (w ↑↑u) < 0

              Construct a unit associated to the place w₁. The family, for w₁ β‰  wβ‚€, formed by the image by the logEmbedding of these units is ℝ-linearly independent, see unitLattice_span_eq_top.

              The unit rank of the number field K, it is equal to card (InfinitePlace K) - 1.

              Equations
              Instances For
                theorem NumberField.Units.finrank_eq_rank (K : Type u_1) [Field K] [NumberField K] :
                FiniteDimensional.finrank ℝ ({ w : NumberField.InfinitePlace K // w β‰  NumberField.Units.dirichletUnitTheorem.wβ‚€ } β†’ ℝ) = NumberField.Units.rank K

                The linear equivalence between unitLattice and (π“ž K)Λ£ β§Έ (torsion K) as an additive β„€-module.

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

                  A fundamental system of units of K. The units of fundSystem are arbitrary lifts of the units in basisModTorsion.

                  Equations
                  Instances For
                    theorem NumberField.Units.fun_eq_repr (K : Type u_1) [Field K] [NumberField K] {x : (β†₯(NumberField.ringOfIntegers K))Λ£} {ΞΆ : (β†₯(NumberField.ringOfIntegers K))Λ£} {f : Fin (NumberField.Units.rank K) β†’ β„€} (hΞΆ : ΞΆ ∈ NumberField.Units.torsion K) (h : x = ΞΆ * Finset.prod Finset.univ fun (i : Fin (NumberField.Units.rank K)) => NumberField.Units.fundSystem K i ^ f i) :
                    f = ⇑((NumberField.Units.basisModTorsion K).repr (Additive.ofMul ↑x))

                    The exponents that appear in the unique decomposition of a unit as the product of a root of unity and powers of the units of the fundamental system fundSystem (see exist_unique_eq_mul_prod) are given by the representation of the unit on basisModTorsion.

                    theorem NumberField.Units.exist_unique_eq_mul_prod (K : Type u_1) [Field K] [NumberField K] (x : (β†₯(NumberField.ringOfIntegers K))Λ£) :
                    βˆƒ! (ΞΆ : β†₯(NumberField.Units.torsion K)), βˆƒ! (e : Fin (NumberField.Units.rank K) β†’ β„€), x = ↑΢ * Finset.prod Finset.univ fun (i : Fin (NumberField.Units.rank K)) => NumberField.Units.fundSystem K i ^ e i

                    Dirichlet Unit Theorem. Any unit x of π“ž K can be written uniquely as the product of a root of unity and powers of the units of the fundamental system fundSystem.