Documentation

Mathlib.NumberTheory.NumberField.Units.Regulator

Regulator of a number field #

We define and prove basic results about the regulator of a number field K.

Main definitions and results #

Tags #

number field, units, regulator

An equiv between Fin (rank K), used to index the family of units, and {w // w ≠ w₀} the index of the logSpace.

Equations
Instances For
    @[reducible, inline]
    abbrev NumberField.Units.IsMaxRank {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K)(RingOfIntegers K)ˣ) :

    A family of units is of maximal rank if its image by logEmbedding is linearly independent over .

    Equations
    Instances For

      The images by logEmbedding of a family of units of maximal rank form a basis of logSpace K.

      Equations
      Instances For

        The regulator of a family of units of K.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem NumberField.Units.abs_det_eq_abs_det {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K)(RingOfIntegers K)ˣ) {w₁ w₂ : InfinitePlace K} (e₁ : { w : InfinitePlace K // w w₁ } Fin (rank K)) (e₂ : { w : InfinitePlace K // w w₂ } Fin (rank K)) :
          |(Matrix.of fun (i w : { w : InfinitePlace K // w w₁ }) => (↑w).mult * Real.log (w ((algebraMap (RingOfIntegers K) K) (u (e₁ i))))).det| = |(Matrix.of fun (i w : { w : InfinitePlace K // w w₂ }) => (↑w).mult * Real.log (w ((algebraMap (RingOfIntegers K) K) (u (e₂ i))))).det|

          Let u : Fin (rank K) → (𝓞 K)ˣ be a family of units and let w₁ and w₂ be two infinite places. Then, the two square matrices with entries (mult w * log w (u i))_i where w ≠ w_j for j = 1, 2 have the same determinant in absolute value.

          theorem NumberField.Units.regOfFamily_eq_det {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K)(RingOfIntegers K)ˣ) (w' : InfinitePlace K) (e : { w : InfinitePlace K // w w' } Fin (rank K)) :
          regOfFamily u = |(Matrix.of fun (i w : { w : InfinitePlace K // w w' }) => (↑w).mult * Real.log (w ((algebraMap (RingOfIntegers K) K) (u (e i))))).det|

          For any infinite place w', the regulator of the family u is equal to the absolute value of the determinant of the matrix with entries (mult w * log w (u i))_i for w ≠ w'.

          theorem NumberField.Units.finrank_mul_regOfFamily_eq_det {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K)(RingOfIntegers K)ˣ) (w' : InfinitePlace K) (e : { w : InfinitePlace K // w w' } Fin (rank K)) :
          (Module.finrank K) * regOfFamily u = |(Matrix.of fun (i w : InfinitePlace K) => if h : i = w' then w.mult else w.mult * Real.log (w ((algebraMap (RingOfIntegers K) K) (u (e i, h))))).det|

          The degree of K times the regulator of the family u is equal to the absolute value of the determinant of the matrix whose columns are (mult w * log w (fundSystem K i))_i, w and the column (mult w)_w.

          theorem NumberField.Units.regulator_eq_det (K : Type u_1) [Field K] [NumberField K] (w' : InfinitePlace K) (e : { w : InfinitePlace K // w w' } Fin (rank K)) :
          regulator K = |(Matrix.of fun (i w : { w : InfinitePlace K // w w' }) => (↑w).mult * Real.log (w ((algebraMap (RingOfIntegers K) K) (fundSystem K (e i))))).det|

          For any infinite place w', the regulator is equal to the absolute value of the determinant of the matrix with entries (mult w * log w (fundSystem K i))_i for w ≠ w'.

          theorem NumberField.Units.finrank_mul_regulator_eq_det (K : Type u_1) [Field K] [NumberField K] (w' : InfinitePlace K) (e : { w : InfinitePlace K // w w' } Fin (rank K)) :
          (Module.finrank K) * regulator K = |(Matrix.of fun (i w : InfinitePlace K) => if h : i = w' then w.mult else w.mult * Real.log (w ((algebraMap (RingOfIntegers K) K) (fundSystem K (e i, h))))).det|

          The degree of K times the regulator of K is equal to the absolute value of the determinant of the matrix whose columns are (mult w * log w (fundSystem K i))_i, w and the column (mult w)_w.