Regulator of a number field

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

Main definitions and results

• NumberField.Units.regulator: the regulator of the number field K.

• Number.Field.Units.regulator_eq_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 where w runs through the infinite places distinct from w'.

Tags

number field, units, regulator

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

The regulator of a number field K.

Equations

• NumberField.Units.regulator K = ZLattice.covolume (NumberField.Units.unitLattice K) MeasureTheory.volume

theorem NumberField.Units.regulator_ne_zero (K : Type u_1) [Field K] [NumberField K] : regulator K ≠ 0

theorem NumberField.Units.regulator_pos (K : Type u_1) [Field K] [NumberField K] : 0 < regulator K

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|

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.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.