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.regOfFamily: the regulator of a family of units of K.

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

• Number.Field.Units.regOfFamily_eq_det: For any infinite place w', the regulator of the family u is equal to the absolute value of the determinant of the matrix (mult w * log w (u i)))_i, w where w runs through the infinite places distinct from w'.

Tags

number field, units, regulator

def NumberField.Units.equivFinRank (K : Type u_1) [Field K] [NumberField K] : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ dirichletUnitTheorem.w₀ }

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

@[reducible, inline]

abbrev NumberField.Units.IsMaxRank {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) → (RingOfIntegers K)ˣ) : Prop

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

def NumberField.Units.basisOfIsMaxRank {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} (hu : IsMaxRank u) : Module.Basis (Fin (rank K)) ℝ (dirichletUnitTheorem.logSpace K)

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

theorem NumberField.Units.basisOfIsMaxRank_apply {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} (hu : IsMaxRank u) (i : Fin (rank K)) : (basisOfIsMaxRank hu) i = (logEmbedding K) (Additive.ofMul (u i))

theorem NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex {K : Type u_1} [Field K] [NumberField K] (s : Subgroup (RingOfIntegers K)ˣ) : s.FiniteIndex ↔ (s ⊔ torsion K).FiniteIndex

theorem NumberField.Units.isMaxRank_iff_closure_finiteIndex {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} : IsMaxRank u ↔ (Subgroup.closure (Set.range u)).FiniteIndex

A family of units is of maximal rank iff the index of the subgroup it generates has finite index.

def NumberField.Units.regOfFamily {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) → (RingOfIntegers K)ˣ) : ℝ

The regulator of a family of units of K.

theorem NumberField.Units.regOfFamily_eq_zero {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} (hu : ¬IsMaxRank u) : regOfFamily u = 0

theorem NumberField.Units.regOfFamily_of_isMaxRank {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} (hu : IsMaxRank u) : regOfFamily u = ZLattice.covolume (Submodule.span ℤ (Set.range ⇑(basisOfIsMaxRank hu))) MeasureTheory.volume

theorem NumberField.Units.regOfFamily_pos {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} (hu : IsMaxRank u) : 0 < regOfFamily u

theorem NumberField.Units.regOfFamily_ne_zero {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} (hu : IsMaxRank u) : regOfFamily u ≠ 0

theorem NumberField.Units.regOfFamily_ne_zero_iff {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) → (RingOfIntegers K)ˣ} : regOfFamily u ≠ 0 ↔ IsMaxRank u

theorem NumberField.Units.regOfFamily_eq_det' {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) → (RingOfIntegers K)ˣ) : regOfFamily u = |(Matrix.of fun (i : { w : InfinitePlace K // w ≠ dirichletUnitTheorem.w₀ }) => (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm 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.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.

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

The regulator of a number field K.

theorem NumberField.Units.isMaxRank_fundSystem (K : Type u_1) [Field K] [NumberField K] : IsMaxRank (fundSystem K)

theorem NumberField.Units.basisOfIsMaxRank_fundSystem (K : Type u_1) [Field K] [NumberField K] : basisOfIsMaxRank ⋯ = Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)

theorem NumberField.Units.regulator_eq_regOfFamily_fundSystem (K : Type u_1) [Field K] [NumberField K] : regulator K = regOfFamily (fundSystem K)

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

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

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

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.