The absolute height of a tuple of algebraic numbers

Mathlib's Height.mulHeight is the height relative to the field it is computed over: over a number field K it is the [K : ℚ]-th power of the classical absolute height. This file defines the absolute height of a tuple of algebraic numbers,

absMulHeight x = mulHeight_F x ^ (1 / [F : ℚ]) with F = ℚ(x₀, x₁, …),

and proves that the field of definition does not matter: any number field containing the coordinates computes the same number. It is the tuple analogue of Mathlib's NumberField.absMulHeight₁, which handles a single element through ℚ⟮x⟯, and restricts to it.

Main definitions

• NumberField.absMulHeight x for x : ι → K over a field K of characteristic zero, and NumberField.absLogHeight x, its logarithm. A tuple with a coordinate that is not algebraic gets the junk value 1, as NumberField.absMulHeight₁ does.
• Projectivization.absMulHeight and Projectivization.absLogHeight: the descent to Projectivization K (ι → K) over a field all of whose elements are algebraic.

Main results

• NumberField.absMulHeight_eq: over a number field K, absMulHeight x is mulHeight x ^ (finrank ℚ K)⁻¹. With NumberField.mulHeight_pow_finrank of Layer 0.3 this is the classical statement that the absolute height does not depend on the field of definition.
• NumberField.absMulHeight_eq_of_mem: the same, computed in an intermediate field containing the coordinates rather than in K itself. This is the form the other results consume.
• NumberField.absMulHeight_comp: invariance under an embedding of fields of characteristic zero — the absolute height belongs to the algebraic numbers themselves, not to any field holding them. It is what lets a value computed over ℚ be read off in ℝ or ℂ.
• NumberField.absMulHeight_eq_absMulHeight₁: the absolute height of ![x, 1] is Mathlib's absolute height of x, so the tuple definition extends the one-variable one. With it, NumberField.absMulHeight₁_comp transports Mathlib's absMulHeight₁ along an embedding — an algebraic number and each of its conjugates have the same absolute height.
• NumberField.absMulHeight_smul_eq: scaling invariance, for an algebraic scalar.
• NumberField.absMulHeight_comp_le: reindexing does not raise the height, and NumberField.absMulHeight₁_le_absMulHeight, the bound on the coordinates of an affine chart that Northcott's theorem on projective space runs on.
• NumberField.absMulHeight_pow and NumberField.absMulHeight₁_pow: the height of a coordinatewise power, together with NumberField.absMulHeight₁_zero and NumberField.absMulHeight₁_one. Kronecker's theorem of Layer 1.4 runs on these.

Implementation notes

⚠ The algebraicity hypothesis on the scalar in absMulHeight_smul_eq is not decorative. For c transcendental and x a nonzero algebraic tuple, c • x has a transcendental coordinate, so its absolute height is the junk value 1 while that of x need not be; absMulHeight is then not constant on the line through x. This is refuted among the examples at the end of the file. The descent to Projectivization K (ι → K) is therefore stated over a field with [Algebra.IsAlgebraic ℚ K] — a number field, or AlgebraicClosure ℚ — and not over a general field of characteristic zero, even though absMulHeight itself is defined there.

Two facts about Height.mulHeight do the work. Passing from the field ℚ(x₀, x₁, …) generated by the coordinates to a larger number field is NumberField.mulHeight_pow_finrank of Layer 0.3, and the normalizing exponent is what cancels the degree it introduces. Passing between two isomorphic number fields is the degree-one case of the same theorem, recorded here as NumberField.mulHeight_comp_ringEquiv; it is what absMulHeight_comp needs, since an embedding carries ℚ(x₀, x₁, …) to the field generated by the image coordinates, not into a fixed field.

The index type carries Finite, as Height.mulHeight does, where the roadmap's pinned signature has Fintype; nothing here sums over ι.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §1.5. Their h(P) is Definition 1.5.4, the absolute logarithmic height; the independence of the field of definition is Lemma 1.5.2, the invariance under coordinate scaling that makes the height projective is Lemma 1.5.3, and the affine case — the height of (x₁, …, xₙ) read as the height of (1 : x₁ : ⋯ : xₙ) — is 1.5.6. NumberField.absMulHeight_comp generalizes their Proposition 1.5.17, which states the same invariance for an element of the absolute Galois group of ℚ.

This is Layer 0.4 of the ArithmeticHeights roadmap.

The definition

The absolute height is computed over IntermediateField.adjoin ℚ (Set.range x), the field the coordinates generate, and normalized by the inverse of its degree.

noncomputable def NumberField.absMulHeight {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : ℝ

The absolute multiplicative height of a tuple of algebraic numbers: the height relative to the field the coordinates generate, taken to the power 1 / [ℚ(x₀, x₁, …) : ℚ]. A tuple with a coordinate that is not algebraic gets the junk value 1.

This is the tuple analogue of Mathlib's NumberField.absMulHeight₁, which takes this route through ℚ⟮x⟯; absMulHeight_eq_absMulHeight₁ says the two agree where both apply.

Equations

• NumberField.absMulHeight x = if hx : ∀ (i : ι), IsIntegral ℚ (x i) then (Height.mulHeight fun (i : ι) => ⟨x i, ⋯⟩) ^ (↑(Module.finrank ℚ ↥(IntermediateField.adjoin ℚ (Set.range x))))⁻¹ else 1

noncomputable def NumberField.absLogHeight {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : ℝ

The absolute logarithmic height of a tuple of algebraic numbers.

Equations

• NumberField.absLogHeight x = Real.log (NumberField.absMulHeight x)

theorem NumberField.absLogHeight_eq_log_absMulHeight {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : absLogHeight x = Real.log (absMulHeight x)

theorem NumberField.absMulHeight_eq_one_of_not_isIntegral {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : ¬∀ (i : ι), IsIntegral ℚ (x i)) : absMulHeight x = 1

The junk value: a tuple with a coordinate that is not algebraic has absolute height 1.

theorem NumberField.absLogHeight_eq_zero_of_not_isIntegral {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : ¬∀ (i : ι), IsIntegral ℚ (x i)) : absLogHeight x = 0

Heights of isomorphic number fields

NumberField.mulHeight_pow_finrank at degree one: an isomorphism of number fields preserves the relative height. This is the second ingredient of absMulHeight_comp, where the two fields generated by a tuple and by its image are isomorphic but not equal.

theorem NumberField.mulHeight_comp_ringEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] {ι : Type u_3} [Finite ι] (e : K ≃+* L) (x : ι → K) : Height.mulHeight (⇑e ∘ x) = Height.mulHeight x

The relative height is invariant under an isomorphism of number fields, being the degree-one case of NumberField.mulHeight_pow_finrank.

The field of definition does not matter

The two statements of the layer. Both come from NumberField.mulHeight_pow_finrank: passing from ℚ(x₀, x₁, …) to a larger field raises the relative height to the degree of the step, which the normalizing exponent divides out again.

theorem NumberField.absMulHeight_eq_of_mem {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {E : IntermediateField ℚ K} [NumberField ↥E] {x : ι → K} (hx : ∀ (i : ι), x i ∈ E) : absMulHeight x = (Height.mulHeight fun (i : ι) => ⟨x i, ⋯⟩) ^ (↑(Module.finrank ℚ ↥E))⁻¹

The absolute height computed in a field of definition. Any number field between ℚ(x₀, x₁, …) and K gives the same value.

theorem NumberField.absMulHeight_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : absMulHeight x = Height.mulHeight x ^ (↑(Module.finrank ℚ K))⁻¹

The absolute height over a number field is the relative height normalized by the degree. With NumberField.mulHeight_pow_finrank, this says that the absolute height does not depend on the field the coordinates are read in.

theorem NumberField.absLogHeight_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (x : ι → K) : absLogHeight x = (↑(Module.finrank ℚ K))⁻¹ * Height.logHeight x

The logarithmic form: the absolute logarithmic height is the relative one divided by the degree.

Invariance under an embedding

The absolute height is attached to the algebraic numbers themselves: an embedding of fields of characteristic zero leaves it unchanged. This is what makes a value computed over ℚ readable inside ℝ or ℂ, where absMulHeight_eq does not apply because the ambient field is not a number field.

theorem NumberField.absMulHeight_comp {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [Field L] [CharZero L] {ι : Type u_3} [Finite ι] (f : K →ₐ[ℚ] L) (x : ι → K) : absMulHeight (⇑f ∘ x) = absMulHeight x

The absolute height is invariant under an embedding. The height of x is a property of the algebraic numbers x i, not of the field they are read in.

theorem NumberField.absLogHeight_comp {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [Field L] [CharZero L] {ι : Type u_3} [Finite ι] (f : K →ₐ[ℚ] L) (x : ι → K) : absLogHeight (⇑f ∘ x) = absLogHeight x

The logarithmic form of NumberField.absMulHeight_comp.

The absolute Arakelov height is invariant under an embedding

The Arakelov normalization has no absolute form of its own in this development — it is written arakelovMulHeight x ^ (finrank ℚ K : ℝ)⁻¹ wherever it is needed — so the statement is that that expression does not change along a homomorphism of number fields. It is NumberField.arakelovMulHeight_pow_finrank of Layer 0.3 read through the degree, and it is what lets a conjugate of a tuple be compared with the tuple itself.

theorem NumberField.arakelovMulHeight_rpow_comp {F : Type u_1} {L : Type u_2} [Field F] [NumberField F] [Field L] [NumberField L] {κ : Type u_3} [Fintype κ] (f : F →+* L) (x : κ → F) : arakelovMulHeight (⇑f ∘ x) ^ (↑(Module.finrank ℚ L))⁻¹ = arakelovMulHeight x ^ (↑(Module.finrank ℚ F))⁻¹

The absolute Arakelov height is invariant under an embedding of number fields. Every ring homomorphism between fields of characteristic zero is a ℚ-algebra map, so no compatibility hypothesis is needed; the degree of the extension it exhibits is exactly what the normalizing exponent divides out.

Basic API, the affine case, and scaling

theorem NumberField.one_le_absMulHeight {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : 1 ≤ absMulHeight x

theorem NumberField.absMulHeight_pos {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : 0 < absMulHeight x

theorem NumberField.absMulHeight_ne_zero {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : absMulHeight x ≠ 0

theorem NumberField.absLogHeight_nonneg {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) : 0 ≤ absLogHeight x

@[simp]

theorem NumberField.absMulHeight_eq_one_of_subsingleton {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] [Subsingleton ι] (x : ι → K) : absMulHeight x = 1

On a subsingleton index type every tuple has absolute height 1: the height is computed in the field the single coordinate generates, where Height.mulHeight_eq_one_of_subsingleton is the product formula.

@[simp]

theorem NumberField.absLogHeight_eq_zero_of_subsingleton {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] [Subsingleton ι] (x : ι → K) : absLogHeight x = 0

theorem NumberField.absMulHeight_comp_le {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {ι' : Type u_3} [Finite ι'] (f : ι → ι') {x : ι' → K} (hx : ∀ (i : ι'), IsIntegral ℚ (x i)) : absMulHeight (x ∘ f) ≤ absMulHeight x

The absolute height does not increase under reindexing. Dropping or repeating coordinates of an algebraic tuple cannot raise its height; this is Height.mulHeight_comp_le read in the field the coordinates generate.

⚠ The algebraicity hypothesis is not decorative. Without it the statement is false: if some coordinate of x is transcendental then absMulHeight x is the junk value 1, while x ∘ f may omit that coordinate and have a larger height.

theorem NumberField.absLogHeight_comp_le {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {ι' : Type u_3} [Finite ι'] (f : ι → ι') {x : ι' → K} (hx : ∀ (i : ι'), IsIntegral ℚ (x i)) : absLogHeight (x ∘ f) ≤ absLogHeight x

The logarithmic form of NumberField.absMulHeight_comp_le.

theorem NumberField.absMulHeight_comp_equiv {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {ι' : Type u_3} [Finite ι'] (e : ι ≃ ι') (x : ι' → K) : absMulHeight (x ∘ ⇑e) = absMulHeight x

The absolute height is invariant under re-indexing. Unlike NumberField.absMulHeight_comp_le, of which it is the two-sided form, this needs no algebraicity hypothesis: an equivalence permutes the transcendental coordinates rather than dropping them, so the two sides take the junk value together.

theorem NumberField.absLogHeight_comp_equiv {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {ι' : Type u_3} [Finite ι'] (e : ι ≃ ι') (x : ι' → K) : absLogHeight (x ∘ ⇑e) = absLogHeight x

The logarithmic form of NumberField.absMulHeight_comp_equiv.

theorem NumberField.absMulHeight_pow {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : ∀ (i : ι), IsIntegral ℚ (x i)) (n : ℕ) : absMulHeight (x ^ n) = absMulHeight x ^ n

The absolute height of a coordinatewise power. Raising every coordinate of an algebraic tuple to the n-th power raises the height to the n-th power. This is Height.mulHeight_pow read in the field the coordinates generate, which the power does not enlarge, so the normalizing exponent is the same on both sides.

theorem NumberField.absLogHeight_pow {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : ∀ (i : ι), IsIntegral ℚ (x i)) (n : ℕ) : absLogHeight (x ^ n) = ↑n * absLogHeight x

The logarithmic form of NumberField.absMulHeight_pow.

theorem NumberField.absMulHeight_eq_absMulHeight₁ {K : Type u_1} [Field K] [CharZero K] (x : K) : absMulHeight ![x, 1] = absMulHeight₁ x

The tuple definition extends Mathlib's one-variable one. Both sides take the junk value 1 when x is not algebraic.

theorem NumberField.absLogHeight_eq_absLogHeight₁ {K : Type u_1} [Field K] [CharZero K] (x : K) : absLogHeight ![x, 1] = absLogHeight₁ x

The logarithmic form of NumberField.absMulHeight_eq_absMulHeight₁.

theorem NumberField.one_le_absMulHeight₁ {K : Type u_1} [Field K] [CharZero K] (x : K) : 1 ≤ absMulHeight₁ x

Mathlib's absolute height of an element is at least 1, the junk value included.

theorem NumberField.absLogHeight₁_nonneg {K : Type u_1} [Field K] [CharZero K] (x : K) : 0 ≤ absLogHeight₁ x

The logarithmic form of NumberField.one_le_absMulHeight₁.

theorem NumberField.absMulHeight₁_pow {K : Type u_1} [Field K] [CharZero K] {x : K} (hx : IsIntegral ℚ x) (n : ℕ) : absMulHeight₁ (x ^ n) = absMulHeight₁ x ^ n

Mathlib's absolute height of a power: the one-variable form of NumberField.absMulHeight_pow. It is what makes the easy half of Kronecker's theorem immediate — a root of unity has a power of height 1, hence height 1.

theorem NumberField.absLogHeight₁_pow {K : Type u_1} [Field K] [CharZero K] {x : K} (hx : IsIntegral ℚ x) (n : ℕ) : absLogHeight₁ (x ^ n) = ↑n * absLogHeight₁ x

The logarithmic form of NumberField.absMulHeight₁_pow.

theorem NumberField.absMulHeight₁_zero {K : Type u_1} [Field K] [CharZero K] : absMulHeight₁ 0 = 1

Zero has absolute height 1, the value Mathlib's Height.mulHeight₁_zero gives for the relative height. Both this and NumberField.absMulHeight₁_one come from absMulHeight₁_pow: 0 and 1 are the idempotents of K, and a real number at least 1 that is its own square is 1.

theorem NumberField.absLogHeight₁_zero {K : Type u_1} [Field K] [CharZero K] : absLogHeight₁ 0 = 0

The logarithmic form of NumberField.absMulHeight₁_zero.

theorem NumberField.absMulHeight₁_one {K : Type u_1} [Field K] [CharZero K] : absMulHeight₁ 1 = 1

One has absolute height 1; see NumberField.absMulHeight₁_zero.

theorem NumberField.absLogHeight₁_one {K : Type u_1} [Field K] [CharZero K] : absLogHeight₁ 1 = 0

The logarithmic form of NumberField.absMulHeight₁_one.

theorem NumberField.absMulHeight₁_le_absMulHeight {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : ∀ (i : ι), IsIntegral ℚ (x i)) {j : ι} (hj : x j = 1) (i : ι) : absMulHeight₁ (x i) ≤ absMulHeight x

In an affine chart, every coordinate has absolute height at most that of the tuple. A tuple with a coordinate equal to 1 is the affine normalization of the projective point it represents, and this is the bound its coordinates then satisfy.

It is the absolute counterpart of Height.mulHeight₁_div_le_mulHeight, and the one arithmetic step in Northcott's theorem on projective space.

theorem NumberField.absLogHeight₁_le_absLogHeight {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : ∀ (i : ι), IsIntegral ℚ (x i)) {j : ι} (hj : x j = 1) (i : ι) : absLogHeight₁ (x i) ≤ absLogHeight x

The logarithmic form of NumberField.absMulHeight₁_le_absMulHeight.

theorem NumberField.absMulHeight₁_comp {K : Type u_1} [Field K] [CharZero K] {L : Type u_3} [Field L] [CharZero L] (f : K →ₐ[ℚ] L) (x : K) : absMulHeight₁ (f x) = absMulHeight₁ x

Mathlib's absolute height of an element is invariant under an embedding. This is the one-variable form of NumberField.absMulHeight_comp, obtained from it through absMulHeight_eq_absMulHeight₁; it is the statement that an algebraic number and each of its conjugates have the same absolute height.

theorem NumberField.absLogHeight₁_comp {K : Type u_1} [Field K] [CharZero K] {L : Type u_3} [Field L] [CharZero L] (f : K →ₐ[ℚ] L) (x : K) : absLogHeight₁ (f x) = absLogHeight₁ x

The logarithmic form of NumberField.absMulHeight₁_comp.

theorem NumberField.absMulHeight_smul_eq {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) {c : K} (hc : c ≠ 0) (hc' : IsAlgebraic ℚ c) : absMulHeight (c • x) = absMulHeight x

Scaling invariance, for an algebraic scalar. ⚠ The algebraicity hypothesis is not decorative: for c transcendental and x a nonzero algebraic tuple, c • x has a transcendental coordinate and absMulHeight (c • x) is the junk value 1. See the examples at the end of the file.

theorem NumberField.absLogHeight_smul_eq {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} [Finite ι] (x : ι → K) {c : K} (hc : c ≠ 0) (hc' : IsAlgebraic ℚ c) : absLogHeight (c • x) = absLogHeight x

The logarithmic form of NumberField.absMulHeight_smul_eq.

The descent to projective space

Scaling invariance makes the absolute height a well-defined function on Projectivization K (ι → K) — but only over a field all of whose elements are algebraic, since that is where NumberField.absMulHeight_smul_eq applies to every scalar.

noncomputable def Projectivization.absMulHeight {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : ℝ

The absolute multiplicative height of a point of projective space over a field of algebraic numbers.

Equations

• x.absMulHeight = Projectivization.lift (fun (r : { v : ι → K // v ≠ 0 }) => NumberField.absMulHeight ↑r) ⋯ x

noncomputable def Projectivization.absLogHeight {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : ℝ

The absolute logarithmic height of a point of projective space over a field of algebraic numbers.

Equations

• x.absLogHeight = Projectivization.lift (fun (r : { v : ι → K // v ≠ 0 }) => NumberField.absLogHeight ↑r) ⋯ x

theorem Projectivization.absMulHeight_mk {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : x ≠ 0) : (mk K x hx).absMulHeight = NumberField.absMulHeight x

theorem Projectivization.absLogHeight_mk {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : x ≠ 0) : (mk K x hx).absLogHeight = NumberField.absLogHeight x

theorem Projectivization.absLogHeight_eq_log_absMulHeight {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : x.absLogHeight = Real.log x.absMulHeight

theorem Projectivization.one_le_absMulHeight {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : 1 ≤ x.absMulHeight

theorem Projectivization.absMulHeight_pos {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : 0 < x.absMulHeight

theorem Projectivization.absMulHeight_ne_zero {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : x.absMulHeight ≠ 0

theorem Projectivization.absLogHeight_nonneg {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] (x : Projectivization K (ι → K)) : 0 ≤ x.absLogHeight

@[simp]

theorem Projectivization.absMulHeight_eq_one_of_subsingleton {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] [Subsingleton ι] (x : Projectivization K (ι → K)) : x.absMulHeight = 1

On a subsingleton index type every point of projective space has absolute height 1; the projective form of NumberField.absMulHeight_eq_one_of_subsingleton.

@[simp]

theorem Projectivization.absLogHeight_eq_zero_of_subsingleton {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] [Subsingleton ι] (x : Projectivization K (ι → K)) : x.absLogHeight = 0

theorem Projectivization.absMulHeight_eq {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_2} [Finite ι] [NumberField K] (x : Projectivization K (ι → K)) : x.absMulHeight = x.mulHeight ^ (↑(Module.finrank ℚ K))⁻¹

Over a number field the projective absolute height is the projective relative height normalized by the degree, as it is for tuples.

positivity extensions

The absolute heights are positive (multiplicative) resp. nonnegative (logarithmic), exactly as their relative counterparts in Mathlib.NumberTheory.Height.Basic.

def Mathlib.Meta.Positivity.evalAbsMulHeight : PositivityExt

Extension for the positivity tactic: NumberField.absMulHeight is always positive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalAbsLogHeight : PositivityExt

Extension for the positivity tactic: NumberField.absLogHeight is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalProjAbsMulHeight : PositivityExt

Extension for the positivity tactic: Projectivization.absMulHeight is always positive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalProjAbsLogHeight : PositivityExt

Extension for the positivity tactic: Projectivization.absLogHeight is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.

Worked examples

The layer's acceptance test is that one number has one absolute height, whichever field it is read in; the rejection test is that the scaling invariance really does need its algebraicity hypothesis.