The logarithmic embedding of the units

Let L be a number field. Mathlib's logarithmic embedding sends a unit x of 𝓞 L to the vector (mult w * log w(x))_w indexed by the infinite places w ≠ w₀ of L, for a distinguished infinite place w₀; its image is the unit lattice, a full ℤ-lattice in this space logSpace L. The omitted coordinate is recovered from the product formula: the full vector, indexed by all infinite places, has coordinate sum zero. So logSpace L is a coordinate chart on the sum-zero hyperplane of ℝ^{InfinitePlace L} (TauCeti.NumberField.Units.logSpaceExtend).

The relative logarithmic height of a unit is half the ℓ¹ norm of this full vector. Therefore it is the sum of the absolute values of the kept coordinates together with the absolute value of their sum, divided by two. This gives two-sided ℓ¹ comparisons, a sharp supremum-norm bound, and the corresponding absolute-height estimate. It also records exactly when the omitted coordinate contributes to the positive-part and absolute-value formulas.

An automorphism σ of L over a subfield K permutes the infinite places of L, and so acts on that hyperplane by permuting coordinates. Read in the chart this is a real representation TauCeti.NumberField.Units.logSpaceRep K L of Aut(L/K) on logSpace L. The logarithmic embedding is equivariant for the Galois action on the units (TauCeti.NumberField.Units.logEmbedding_smul), so the unit lattice is a Galois-stable lattice in this representation (TauCeti.NumberField.Units.unitLatticeSubrep). This is the form in which the unit group enters the computation of Herbrand quotients of units in class field theory.

Main definitions

• TauCeti.NumberField.Units.logSpaceExtend: the extension of a vector of logSpace L to the infinite place w₀ by minus the sum of its coordinates.
• TauCeti.NumberField.Units.logSpaceRep: the permutation representation of Aut(L/K) on logSpace L.
• TauCeti.NumberField.Units.unitLatticeSubrep: the unit lattice as an integral subrepresentation.

Main results

• TauCeti.NumberField.Units.logSpaceExtend_logSpaceRep: the extension intertwines logSpaceRep with the permutation of the infinite places.
• TauCeti.NumberField.Units.mem_unitLattice_iff: the unit lattice is the set of logarithmic embeddings of units.
• TauCeti.NumberField.Units.logEmbedding_smul: the logarithmic embedding is Aut(L/K)-equivariant.
• TauCeti.NumberField.Units.two_mul_logHeight₁_eq_sum_mult_mul_abs_log: twice the height of a unit is the sum of its weighted absolute logarithms over all infinite places.
• TauCeti.NumberField.Units.two_mul_logHeight₁_eq_sum_abs_logEmbedding: the exact relation between logarithmic height and the omitted-coordinate embedding.
• TauCeti.NumberField.Units.norm_logEmbedding_le_logHeight₁ and TauCeti.NumberField.Units.logHeight₁_le_rank_mul_norm_logEmbedding: the supremum-norm comparisons.
• TauCeti.NumberField.Units.sum_abs_logEmbedding_le_sum_mult_mul_abs_log: the ℓ¹ norm of the logarithmic embedding of a unit is at most the sum of its weighted absolute logarithms over all infinite places.

References

• J. S. Milne, Class Field Theory, Chapter VII, §3 (the Herbrand quotient of the unit group).
• Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, formula (12).

The sum-zero hyperplane

noncomputable def TauCeti.NumberField.Units.logSpaceExtend (L : Type u_1) [Field L] [NumberField L] : NumberField.Units.dirichletUnitTheorem.logSpace L →ₗ[ℝ] NumberField.InfinitePlace L → ℝ

The extension of a vector of logSpace L, indexed by the infinite places other than w₀, to all infinite places, with coordinate at w₀ minus the sum of the others. It identifies logSpace L with the vectors of ℝ^{InfinitePlace L} of coordinate sum zero (TauCeti.NumberField.Units.sum_logSpaceExtend, TauCeti.NumberField.Units.logSpaceExtend_eq_self).

@[simp]

theorem TauCeti.NumberField.Units.logSpaceExtend_apply_w₀ {L : Type u_1} [Field L] [NumberField L] (y : NumberField.Units.dirichletUnitTheorem.logSpace L) : (logSpaceExtend L) y NumberField.Units.dirichletUnitTheorem.w₀ = -∑ i : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, y i

@[simp]

theorem TauCeti.NumberField.Units.logSpaceExtend_apply_val {L : Type u_1} [Field L] [NumberField L] (y : NumberField.Units.dirichletUnitTheorem.logSpace L) (w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) : (logSpaceExtend L) y ↑w = y w

@[simp]

theorem TauCeti.NumberField.Units.sum_logSpaceExtend {L : Type u_1} [Field L] [NumberField L] (y : NumberField.Units.dirichletUnitTheorem.logSpace L) : ∑ w : NumberField.InfinitePlace L, (logSpaceExtend L) y w = 0

The coordinates of logSpaceExtend L y sum to zero.

theorem TauCeti.NumberField.Units.sum_logSpaceExtend_perm {L : Type u_1} [Field L] [NumberField L] (y : NumberField.Units.dirichletUnitTheorem.logSpace L) (e : Equiv.Perm (NumberField.InfinitePlace L)) : ∑ w : NumberField.InfinitePlace L, (logSpaceExtend L) y (e w) = 0

The coordinates of logSpaceExtend L y, permuted by any permutation of the infinite places, sum to zero.

theorem TauCeti.NumberField.Units.logSpaceExtend_eq_self {L : Type u_1} [Field L] [NumberField L] {f : NumberField.InfinitePlace L → ℝ} (hf : ∑ w : NumberField.InfinitePlace L, f w = 0) : ((logSpaceExtend L) fun (w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) => f ↑w) = f

A vector of coordinate sum zero is the extension of its coordinates away from w₀.

@[simp]

theorem TauCeti.NumberField.Units.logSpaceExtend_logEmbedding {L : Type u_1} [Field L] [NumberField L] (x : (NumberField.RingOfIntegers L)ˣ) : (logSpaceExtend L) ((NumberField.Units.logEmbedding L) (Additive.ofMul x)) = fun (w : NumberField.InfinitePlace L) => ↑w.mult * Real.log (w ((algebraMap (NumberField.RingOfIntegers L) L) ↑x))

The extension of the logarithmic embedding of a unit x is the full vector (mult w * log w(x))_w over all infinite places, by the product formula.

The unit lattice

theorem TauCeti.NumberField.Units.mem_unitLattice_iff {L : Type u_1} [Field L] [NumberField L] {y : NumberField.Units.dirichletUnitTheorem.logSpace L} : y ∈ NumberField.Units.unitLattice L ↔ ∃ (u : (NumberField.RingOfIntegers L)ˣ), (NumberField.Units.logEmbedding L) (Additive.ofMul u) = y

A vector lies in the unit lattice exactly when it is the logarithmic embedding of a unit.

@[simp]

theorem TauCeti.NumberField.Units.logEmbedding_mem_unitLattice {L : Type u_1} [Field L] [NumberField L] (x : Additive (NumberField.RingOfIntegers L)ˣ) : (NumberField.Units.logEmbedding L) x ∈ NumberField.Units.unitLattice L

The logarithmic embedding of a unit lies in the unit lattice.

The ℓ¹ norm

theorem TauCeti.NumberField.Units.sum_abs_logEmbedding_le_sum_mult_mul_abs_log {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : ∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |(NumberField.Units.logEmbedding L) (Additive.ofMul u) w| ≤ ∑ w : NumberField.InfinitePlace L, ↑w.mult * |Real.log (w ((algebraMap (NumberField.RingOfIntegers L) L) ↑u))|

The ℓ¹ norm of the logarithmic embedding of a unit, which omits the distinguished infinite place, is at most the sum of the weighted absolute logarithms over all infinite places.

Comparison with the logarithmic height

theorem TauCeti.NumberField.Units.two_mul_logHeight₁_eq_sum_mult_mul_abs_log {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : 2 * Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) = ∑ w : NumberField.InfinitePlace L, ↑w.mult * |Real.log (w ((algebraMap (NumberField.RingOfIntegers L) L) ↑u))|

Twice the relative logarithmic height of a unit is the sum over all infinite places of its weighted absolute logarithms: the finite places contribute nothing.

theorem TauCeti.NumberField.Units.two_mul_logHeight₁_eq_sum_abs_logEmbedding {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : 2 * Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) = ∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |(NumberField.Units.logEmbedding L) (Additive.ofMul u) w| + |∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, (NumberField.Units.logEmbedding L) (Additive.ofMul u) w|

Twice the relative logarithmic height of a unit is the ℓ¹ norm of its logarithmic embedding, together with the absolute value of the omitted coordinate.

theorem TauCeti.NumberField.Units.sum_abs_logEmbedding_le_two_mul_logHeight₁ {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : ∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |(NumberField.Units.logEmbedding L) (Additive.ofMul u) w| ≤ 2 * Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u)

The ℓ¹ norm of the logarithmic embedding of a unit is at most twice its relative logarithmic height.

theorem TauCeti.NumberField.Units.logHeight₁_le_sum_abs_logEmbedding {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) ≤ ∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |(NumberField.Units.logEmbedding L) (Additive.ofMul u) w|

The relative logarithmic height of a unit is at most the ℓ¹ norm of its logarithmic embedding.

theorem TauCeti.NumberField.Units.norm_logEmbedding_le_logHeight₁ {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : ‖(NumberField.Units.logEmbedding L) (Additive.ofMul u)‖ ≤ Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u)

The supremum norm of the logarithmic embedding of a unit is at most its relative logarithmic height. This improves by a factor of two on the bound obtained from its ℓ¹ norm.

theorem TauCeti.NumberField.Units.logHeight₁_le_rank_mul_norm_logEmbedding {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) ≤ ↑(NumberField.Units.rank L) * ‖(NumberField.Units.logEmbedding L) (Additive.ofMul u)‖

The relative logarithmic height of a unit is bounded by the unit rank times the supremum norm of its logarithmic embedding.

theorem TauCeti.NumberField.Units.absLogHeight₁_le_sum_abs_logEmbedding_div_finrank {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) ≤ (∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |(NumberField.Units.logEmbedding L) (Additive.ofMul u) w|) / ↑(Module.finrank ℚ L)

The absolute logarithmic height of a unit is at most the ℓ¹ norm of its logarithmic embedding divided by the degree of the number field.

theorem TauCeti.NumberField.Units.logHeight₁_eq_sum_posPart_logEmbedding_iff {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) = ∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, ((NumberField.Units.logEmbedding L) (Additive.ofMul u) w)⁺ ↔ NumberField.Units.dirichletUnitTheorem.w₀ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) ≤ 1

The relative logarithmic height of a unit equals the sum of the positive parts of the kept logarithmic coordinates exactly when its absolute value at the omitted place is at most one.

theorem TauCeti.NumberField.Units.two_mul_logHeight₁_eq_sum_abs_logEmbedding_iff {L : Type u_1} [Field L] [NumberField L] (u : (NumberField.RingOfIntegers L)ˣ) : 2 * Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) = ∑ w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, |(NumberField.Units.logEmbedding L) (Additive.ofMul u) w| ↔ NumberField.Units.dirichletUnitTheorem.w₀ ((algebraMap (NumberField.RingOfIntegers L) L) ↑u) = 1

Twice the relative logarithmic height of a unit equals the ℓ¹ norm of the kept logarithmic coordinates exactly when its absolute value at the omitted place is one.

The Galois representation

noncomputable def TauCeti.NumberField.Units.logSpaceRep (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] : Representation ℝ Gal(L/K) (NumberField.Units.dirichletUnitTheorem.logSpace L)

The real representation of Aut(L/K) on logSpace L: an automorphism σ permutes the coordinates of the sum-zero hyperplane of ℝ^{InfinitePlace L} by w ↦ σ • w, read in the chart logSpaceExtend L (TauCeti.NumberField.Units.logSpaceExtend_logSpaceRep).

@[simp]

theorem TauCeti.NumberField.Units.logSpaceRep_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (y : NumberField.Units.dirichletUnitTheorem.logSpace L) (w : { w : NumberField.InfinitePlace L // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) : ((logSpaceRep K L) σ) y w = (logSpaceExtend L) y (σ⁻¹ • ↑w)

@[simp]

theorem TauCeti.NumberField.Units.logSpaceExtend_logSpaceRep {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (y : NumberField.Units.dirichletUnitTheorem.logSpace L) : (logSpaceExtend L) (((logSpaceRep K L) σ) y) = fun (w : NumberField.InfinitePlace L) => (logSpaceExtend L) y (σ⁻¹ • w)

logSpaceRep is the permutation of the infinite places, read through the identification logSpaceExtend L of logSpace L with the sum-zero hyperplane.

@[simp]

theorem TauCeti.NumberField.Units.logEmbedding_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (x : Additive (NumberField.RingOfIntegers L)ˣ) : (NumberField.Units.logEmbedding L) (σ • x) = ((logSpaceRep K L) σ) ((NumberField.Units.logEmbedding L) x)

The logarithmic embedding is Galois-equivariant: the logarithmic embedding of σ • x is logSpaceRep K L σ applied to that of x.

noncomputable def TauCeti.NumberField.Units.unitLatticeSubrep (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] : Subrepresentation (Representation.restrictScalars ℤ (logSpaceRep K L))

The unit lattice logEmbedding L ((𝓞 L)ˣ) as an integral subrepresentation of logSpaceRep: it is stable under Aut(L/K) by TauCeti.NumberField.Units.logEmbedding_smul.

@[simp]

theorem TauCeti.NumberField.Units.toSubmodule_unitLatticeSubrep {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] : (unitLatticeSubrep K L).toSubmodule = NumberField.Units.unitLattice L