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 ofK
.NumberField.Units.regulator
: the regulator of the number fieldK
.Number.Field.Units.regulator_eq_det
: For any infinite placew'
, the regulator is equal to the absolute value of the determinant of the matrix(mult w * log w (fundSystem K i)))_i, w
wherew
runs through the infinite places distinct fromw'
.
Tags #
number field, units, regulator
An equiv
between Fin (rank K)
, used to index the family of units, and {w // w ≠ w₀}
the index of the logSpace
.
Equations
Instances For
A family of units is of maximal rank if its image by logEmbedding
is linearly independent
over ℝ
.
Equations
- NumberField.Units.IsMaxRank u = LinearIndependent ℝ fun (i : Fin (NumberField.Units.rank K)) => (NumberField.Units.logEmbedding K) (Additive.ofMul (u i))
Instances For
The images by logEmbedding
of a family of units of maximal rank form a basis of logSpace K
.
Equations
Instances For
The regulator of a family of units of K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
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'
.
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
.
The regulator of a number field K
.
Equations
Instances For
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'
.
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
.