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

source
def NumberField.Units.regulator (K : Type u_1) [Field K] [NumberField K] :
ℝ

The regulator of a number field K.

Equations
Instances For
    source
    theorem NumberField.Units.regulator_ne_zero (K : Type u_1) [Field K] [NumberField K] :
    regulator K ≠ 0
    source
    theorem NumberField.Units.regulator_pos (K : Type u_1) [Field K] [NumberField K] :
    0 < regulator K
    source
    theorem NumberField.Units.regulator_eq_det' (K : Type u_1) [Field K] [NumberField K] (e : { w : InfinitePlace K // w ≠ dirichletUnitTheorem.w₀ } ≃ Fin (rank K)) :
    regulator K = |(Matrix.of fun (i : { w : InfinitePlace K // w ≠ dirichletUnitTheorem.w₀ }) => (logEmbedding K) (Additive.ofMul (fundSystem K (e i)))).det|
    source
    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, {w ≠ w_i}, i = 1,2, have the same determinant in absolute value.

    source
    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 (mult w * log w (fundSystem K i)))_i, {w ≠ w'}.