Documentation

LeanPool.CCDN.ArithmeticHeights.Extension

Heights under a finite extension of number fields #

Mathlib's Height.mulHeight is the height relative to the field it is computed over. This file proves how it changes when that field grows: for a finite extension L / K of number fields and a tuple x over K,

mulHeight x ^ [L : K] = mulHeight (algebraMap K L ∘ x).

Equivalently, mulHeight x ^ (finrank ℚ K)⁻¹ does not depend on the field the coordinates are read in — the statement that the absolute height is well defined, recorded here for a single element as NumberField.absMulHeight₁_eq.

Main results #

Implementation notes #

The two factors of the height are handled by different mechanisms, and neither is the places-above-places bookkeeping one might expect.

The archimedean factor is first turned into a product over the complex embeddings — this is what InfinitePlace.card_filter_mk_eq does, the exponent mult v being the number of embeddings inducing v. The statement then becomes the count #{φ : L →+* ℂ | φ.comp (algebraMap K L) = ψ} = [L : K], which is AlgHom.card once ℂ carries the K-algebra structure of ψ. The roadmap asks for InfinitePlace.liesOver_iff_comap_eq as the first step of this layer; it is not needed on this route, and Mathlib meanwhile carries that theory itself, in Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean.

The nonarchimedean factor of the height of an integral tuple is the inverse of the absolute norm of the ideal its coordinates generate, by NumberField.absNorm_mul_finprod_finitePlace_eq_one. So that half reduces to Ideal.absNorm (I.map (algebraMap (𝓞 K) (𝓞 L))) = Ideal.absNorm I ^ [L : K], which is Ideal.relNorm_algebraMap followed by Ideal.absNorm_relNorm — no ramification or inertia appears, since those are already inside Mathlib's relative ideal norm.

⚠ The nonarchimedean factor alone is not invariant under scaling: ∏ᶠ v, ⨆ i, v (c * x i) picks up the finite part of the product formula for c. The reduction from an arbitrary tuple to an integral one is therefore performed on the whole height, where Height.mulHeight_smul_eq_mulHeight applies to both sides at once, and not factor by factor.

References #

These are the statements of mathlib4#41606 and carry its names, so that adopting Mathlib's version is a deletion plus an import.

This is Layer 0.3 of the ArithmeticHeights roadmap.

The archimedean factor #

A product over the infinite places, weighted by mult, is a product over the complex embeddings; in that form the extension statement is the count of extensions of an embedding.

source
theorem NumberField.prod_embeddings_eq {K : Type u_1} [Field K] [NumberField K] {M : Type u_4} [CommMonoid M] (f : InfinitePlace K → M) :
∏ φ : K →+* ℂ, f (InfinitePlace.mk φ) = ∏ w : InfinitePlace K, f w ^ w.mult

A mult-weighted product over the infinite places is the product over the complex embeddings, each place counted once per embedding inducing it.

source
theorem NumberField.prod_comp_eq_prod_pow {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (F : (K →+* ℂ) → ℝ) :
∏ φ : L →+* ℂ, F (φ.comp (algebraMap K L)) = (∏ ψ : K →+* ℂ, F ψ) ^ Module.finrank K L

A product over the complex embeddings of L of a factor that reads an embedding only through its restriction to K is the [L : K]-th power of the product over the embeddings of K.

source
theorem NumberField.prod_infinitePlace_pow_mult_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (f : InfinitePlace K → ℝ) (g : InfinitePlace L → ℝ) (h : ∀ (φ : L →+* ℂ), g (InfinitePlace.mk φ) = f (InfinitePlace.mk (φ.comp (algebraMap K L)))) :
∏ w : InfinitePlace L, g w ^ w.mult = (∏ v : InfinitePlace K, f v ^ v.mult) ^ Module.finrank K L

The archimedean half of every extension formula for a height. A mult-weighted product over the infinite places of L of a local factor g that reads a place only through its restriction to K is the [L : K]-th power of the corresponding product over K. The two normalizations of Layer 0 differ in g and in nothing else, so both take this lemma as it stands.

The nonarchimedean factor #

For an integral tuple this factor is the inverse of the absolute norm of the ideal the coordinates generate, so the extension statement is one about ideal norms.

The extension formula #

source
theorem NumberField.mulHeight_pow_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] {ι : Type u_3} [Finite ι] (x : ι → K) :
Height.mulHeight x ^ Module.finrank K L = Height.mulHeight (⇑(algebraMap K L) ∘ x)

The height over L is the [L : K]-th power of the height over K. The relative height grows with the field the tuple is read in, by exactly the degree.

source
theorem NumberField.mulHeight₁_pow_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (x : K) :
Height.mulHeight₁ x ^ Module.finrank K L = Height.mulHeight₁ ((algebraMap K L) x)

The one-variable form of NumberField.mulHeight_pow_finrank.

source
theorem NumberField.finrank_nsmul_logHeight {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] {ι : Type u_3} [Finite ι] (x : ι → K) :
Module.finrank K L • Height.logHeight x = Height.logHeight (⇑(algebraMap K L) ∘ x)

The logarithmic form of NumberField.mulHeight_pow_finrank.

source
theorem NumberField.finrank_nsmul_logHeight₁ {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (x : K) :
Module.finrank K L • Height.logHeight₁ x = Height.logHeight₁ ((algebraMap K L) x)

The logarithmic form of NumberField.mulHeight₁_pow_finrank.

source
theorem NumberField.absMulHeight₁_eq {K : Type u_1} [Field K] [NumberField K] (x : K) :
absMulHeight₁ x = Height.mulHeight₁ x ^ (↑(Module.finrank ℚ K))⁻¹

The absolute height does not depend on the field of definition. Mathlib defines absMulHeight₁ x through ℚ⟮x⟯; this computes it in any number field containing x.

source
theorem NumberField.absMulHeight₁_pow_finrank {K : Type u_1} [Field K] [NumberField K] (x : K) :
absMulHeight₁ x ^ Module.finrank ℚ K = Height.mulHeight₁ x

The relative height is the [K : ℚ]-th power of the absolute one: absMulHeight₁_eq read backwards, in the form that carries a natural-number exponent rather than a real one.

source
theorem NumberField.absLogHeight₁_eq {K : Type u_1} [Field K] [NumberField K] (x : K) :
absLogHeight₁ x = Height.logHeight₁ x / ↑(Module.finrank ℚ K)

The logarithmic form of NumberField.absMulHeight₁_eq: the absolute logarithmic height is the relative one divided by the degree.

The Arakelov normalization #

NumberField.arakelovMulHeight differs from Height.mulHeight only in the archimedean local factor, and that factor reads a place in exactly the same way, so the two counts above prove the extension formula for it too. The nonarchimedean factor is literally the same expression, and the reduction to an integral tuple is the same reduction.

source
theorem NumberField.arakelovMulHeight_pow_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] {κ : Type u_4} [Fintype κ] (x : κ → K) :
arakelovMulHeight x ^ Module.finrank K L = arakelovMulHeight (⇑(algebraMap K L) ∘ x)

The Arakelov height over L is the [L : K]-th power of the Arakelov height over K, the companion of NumberField.mulHeight_pow_finrank in the normalization of Layer 0.1. Only the archimedean factor has to be redone, and only through the local factor it reads off a place.

source
theorem NumberField.finrank_nsmul_arakelovLogHeight {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] {κ : Type u_4} [Fintype κ] (x : κ → K) :
Module.finrank K L • arakelovLogHeight x = arakelovLogHeight (⇑(algebraMap K L) ∘ x)

The logarithmic form of NumberField.arakelovMulHeight_pow_finrank.

Worked examples #

The special case K = ℚ is the acceptance test the roadmap names for the general statement: it needs no places above places, and it is literally an instance.