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] : NumberField.Units.regulator K ≠ 0

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

theorem NumberField.Units.regulator_eq_det' (K : Type u_1) [Field K] [NumberField K] (e : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } ≃ Fin (NumberField.Units.rank K)) : NumberField.Units.regulator K = |(Matrix.of fun (i : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) => (NumberField.Units.logEmbedding K) (Additive.ofMul (NumberField.Units.fundSystem K (e i)))).det|

theorem NumberField.Units.abs_det_eq_abs_det (K : Type u_1) [Field K] [NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) {w₁ : NumberField.InfinitePlace K} {w₂ : NumberField.InfinitePlace K} (e₁ : { w : NumberField.InfinitePlace K // w ≠ w₁ } ≃ Fin (NumberField.Units.rank K)) (e₂ : { w : NumberField.InfinitePlace K // w ≠ w₂ } ≃ Fin (NumberField.Units.rank K)) : |(Matrix.of fun (i w : { w : NumberField.InfinitePlace K // w ≠ w₁ }) => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e₁ i))))).det| = |(Matrix.of fun (i w : { w : NumberField.InfinitePlace K // w ≠ w₂ }) => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.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.

theorem NumberField.Units.regulator_eq_det (K : Type u_1) [Field K] [NumberField K] (w' : NumberField.InfinitePlace K) (e : { w : NumberField.InfinitePlace K // w ≠ w' } ≃ Fin (NumberField.Units.rank K)) : NumberField.Units.regulator K = |(Matrix.of fun (i w : { w : NumberField.InfinitePlace K // w ≠ w' }) => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.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'}.