Documentation

TauCeti.NumberTheory.NumberField.SUnits.Regulator

The S-regulator #

Let S be a finite set of finite places of a number field K. A family ε : ι → S.unit K is a fundamental system of S-units if, together with the torsion, it generates the S-units and it has NumberField.Units.rank K + #S members. The imported lattice API identifies fundamental systems with the families whose S-logarithmic images form a ℤ-basis of the S-unit lattice TauCeti.NumberField.SUnit.unitLattice S.

The S-regulator is the covolume of the S-unit lattice. It is positive, and for any fundamental system ε and any infinite place w' it is the absolute value of the determinant of the square matrix of weighted logarithms of the ε i at the places of S and the infinite places other than w'. The choice of w' does not matter because the product formula makes the rows of the full matrix of weighted logarithms, over all places in S and at infinity, sum to zero. For S = ∅ the S-regulator is the regulator of K.

Main definitions and results #

References #

The definitions and the determinant formula are modelled on Mathlib's regulator of a number field, NumberField.Units.regulator and NumberField.Units.regulator_eq_det in Mathlib.NumberTheory.NumberField.Units.Regulator, by Xavier Roblot.

The S-regulator #

source
noncomputable def TauCeti.NumberField.SUnit.regulator {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
ℝ

The S-regulator is the covolume of the S-unit lattice.

Instances For
    source
    theorem TauCeti.NumberField.SUnit.regulator_def {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
    regulator S = ZLattice.covolume (unitLattice S) MeasureTheory.volume

    The defining covolume formula for the S-regulator.

    source
    theorem TauCeti.NumberField.SUnit.regulator_pos {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
    0 < regulator S

    The S-regulator is positive.

    source
    theorem TauCeti.NumberField.SUnit.regulator_ne_zero {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
    regulator S ≠ 0

    The S-regulator is nonzero.

    The determinant formula #

    source
    theorem TauCeti.NumberField.SUnit.regulator_eq_abs_det {K : Type u_1} [Field K] [NumberField K] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ε : ι → ↥((↑S).unit K)} (hε : Subgroup.closure (Set.range ε) ⊔ CommGroup.torsion ↥((↑S).unit K) = ⊤) (w' : NumberField.InfinitePlace K) (e : ι ≃ { w : NumberField.InfinitePlace K // w ≠ w' } ⊕ ↥S) :
    regulator S = |(Matrix.of fun (i k : ι) => Sum.elim (fun (w : { w : NumberField.InfinitePlace K // w ≠ w' }) => ↑(↑w).mult * Real.log (↑w ↑↑(ε i))) (fun (v : ↥S) => Real.log ((NumberField.FinitePlace.mk ↑v) ↑↑(ε i))) (e k)).det|

    The determinant formula for the S-regulator. For a family ε of S-units that, together with the torsion subgroup, generates the S-units, an infinite place w' and any identification e of ι with the places of S and the infinite places other than w', the S-regulator is the absolute value of the determinant of the matrix whose i-th row lists mult w * log (w (ε i)) at the infinite places w ≠ w' and log ‖ε i‖_v at the places v ∈ S, in the order given by e. The family ε is then a fundamental system, its cardinality being forced by e. This is the S-analogue of Mathlib's NumberField.Units.regulator_eq_det.

    source
    theorem TauCeti.NumberField.SUnit.regulator_empty {K : Type u_1} [Field K] [NumberField K] :
    regulator ∅ = NumberField.Units.regulator K

    The S-regulator of the empty set of places is the regulator of K.