The Arakelov height of a subspace

Let K be a number field and ι a finite linearly ordered type. The relative Arakelov height of a subspace U of K^ι is the relative Euclidean projective height TauCeti.arakelovMulHeight of its Plücker point, that is, of the Plücker coordinates of any basis of U. It differs from the relative sup height Submodule.relativeSubspaceHeight only at the infinite places, where it uses the Euclidean norm of the Plücker vector instead of its maximum norm. The zero subspace and the whole space have height 1, and a line has the height of any nonzero vector spanning it.

Comparing the two norms at the infinite places, for U of dimension k and n = #ι, relativeSubspaceHeight U ≤ relativeSubspaceArakelovHeight U and relativeSubspaceArakelovHeight U ≤ √(n.choose k) ^ [K : ℚ] · relativeSubspaceHeight U, since the Plücker vector has n.choose k coordinates. The first bound transfers the Northcott property of the sup height: K^ι has finitely many subspaces of bounded Arakelov height, of all dimensions together.

The absolute height Submodule.subspaceHeight U is the [K : ℚ]-th root of the relative Arakelov height, equivalently the absolute Euclidean height TauCeti.height2 of the Plücker coordinates of any basis of U. This is the height of a subspace in Evertse–Ferretti's quantitative Subspace Theorem. It inherits the Northcott property.

The orthogonal complement of U for the dot product, Submodule.euclideanDual, has the same relative Arakelov height and the same absolute height as U, since its Plücker coordinates are the complementary Plücker coordinates of U up to a common nonzero factor and signs. Over ℚ, the plane in ℚ³ orthogonal to (1, 2, 2) has absolute height 3, the Euclidean norm of (1, 2, 2).

Main definitions

• Submodule.relativeSubspaceArakelovHeight U: the relative Arakelov height of U.
• Submodule.relativeSubspaceArakelovLogHeight U: its logarithm.
• Submodule.subspaceHeight U: the absolute Euclidean height of U.
• Submodule.subspaceLogHeight U: its logarithm.

Main results

• Submodule.relativeSubspaceArakelovHeight_eq_arakelovMulHeight_plucker: the height of U is the Arakelov height of the Plücker coordinates of any basis of U.
• Submodule.relativeSubspaceHeight_le_relativeSubspaceArakelovHeight and Submodule.relativeSubspaceArakelovHeight_le_sqrt_choose_pow_mul_relativeSubspaceHeight: the comparison with the relative sup height.
• Submodule.instNorthcottRelativeSubspaceArakelovHeight and Submodule.instNorthcottRelativeSubspaceArakelovLogHeight: the Northcott property.
• Submodule.subspaceHeight_eq_height2_plucker: the absolute height of U is the absolute Euclidean height of the Plücker coordinates of any basis of U.
• Submodule.relativeSubspaceHeight_rpow_le_subspaceHeight and Submodule.subspaceHeight_le_sqrt_choose_mul_relativeSubspaceHeight_rpow: the comparison with the absolute sup height, with their logarithmic forms.
• Submodule.relativeSubspaceArakelovHeight_euclideanDual and Submodule.subspaceHeight_euclideanDual: the orthogonal complement of U for the dot product has the height of U, with their logarithmic forms.
• Submodule.finite_subspaceHeight_le, Submodule.instNorthcottSubspaceHeight and Submodule.instNorthcottSubspaceLogHeight: Northcott's theorem for the absolute height.

References

• J.-H. Evertse and R. G. Ferretti, A further improvement of the quantitative Subspace Theorem, Ann. of Math. 177 (2013), §6.1 and §6.3.
• W. M. Schmidt, On heights of algebraic subspaces and diophantine approximations, Ann. of Math. 85 (1967), 430–472.

noncomputable def Submodule.relativeSubspaceArakelovHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : ℝ

The relative Arakelov height of a subspace U of ι → K: the relative Euclidean projective height TauCeti.arakelovMulHeight of the Plücker coordinates of any basis of U (relativeSubspaceArakelovHeight_eq_arakelovMulHeight_plucker).

noncomputable def Submodule.relativeSubspaceArakelovLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : ℝ

The relative logarithmic Arakelov height of a subspace U of ι → K: the logarithm of relativeSubspaceArakelovHeight U.

theorem Submodule.relativeSubspaceArakelovLogHeight_eq_log_relativeSubspaceArakelovHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceArakelovLogHeight = Real.log U.relativeSubspaceArakelovHeight

The relative logarithmic Arakelov height is the logarithm of the relative Arakelov height.

theorem Submodule.relativeSubspaceArakelovHeight_eq_arakelovMulHeight_plucker {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {U : Submodule K (ι → K)} {p : ℕ} (b : Module.Basis (Fin p) K ↥U) : U.relativeSubspaceArakelovHeight = TauCeti.arakelovMulHeight (TauCeti.plucker fun (i : Fin p) => ↑(b i))

The relative Arakelov height of U is the Arakelov height of the Plücker coordinates of any basis of U.

theorem Submodule.relativeSubspaceArakelovLogHeight_eq_arakelovLogHeight_plucker {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {U : Submodule K (ι → K)} {p : ℕ} (b : Module.Basis (Fin p) K ↥U) : U.relativeSubspaceArakelovLogHeight = TauCeti.arakelovLogHeight (TauCeti.plucker fun (i : Fin p) => ↑(b i))

The relative logarithmic Arakelov height of U is the logarithmic Arakelov height of the Plücker coordinates of any basis of U.

theorem Submodule.relativeSubspaceArakelovHeight_span_range {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {p : ℕ} {x : Fin p → ι → K} (hx : LinearIndependent K x) : (span K (Set.range x)).relativeSubspaceArakelovHeight = TauCeti.arakelovMulHeight (TauCeti.plucker x)

The relative Arakelov height of the span of a linearly independent family is the Arakelov height of its Plücker coordinates.

theorem Submodule.relativeSubspaceArakelovLogHeight_span_range {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {p : ℕ} {x : Fin p → ι → K} (hx : LinearIndependent K x) : (span K (Set.range x)).relativeSubspaceArakelovLogHeight = TauCeti.arakelovLogHeight (TauCeti.plucker x)

The relative logarithmic Arakelov height of the span of a linearly independent family is the logarithmic Arakelov height of its Plücker coordinates.

theorem Submodule.one_le_relativeSubspaceArakelovHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : 1 ≤ U.relativeSubspaceArakelovHeight

The relative Arakelov height of a subspace is at least 1.

theorem Submodule.relativeSubspaceArakelovHeight_pos {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : 0 < U.relativeSubspaceArakelovHeight

The relative Arakelov height of a subspace is positive.

theorem Submodule.relativeSubspaceArakelovLogHeight_nonneg {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : 0 ≤ U.relativeSubspaceArakelovLogHeight

The relative logarithmic Arakelov height of a subspace is nonnegative.

theorem Submodule.relativeSubspaceHeight_le_relativeSubspaceArakelovHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceHeight ≤ U.relativeSubspaceArakelovHeight

The relative sup height of a subspace is at most its relative Arakelov height.

theorem Submodule.relativeSubspaceArakelovHeight_le_sqrt_choose_pow_mul_relativeSubspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceArakelovHeight ≤ √↑((Nat.card ι).choose (Module.finrank K ↥U)) ^ Module.finrank ℚ K * U.relativeSubspaceHeight

The relative Arakelov height of a subspace U of dimension k is at most √(#ι.choose k) ^ [K : ℚ] times its relative sup height: its Plücker vector has #ι.choose k coordinates.

theorem Submodule.relativeSubspaceLogHeight_le_relativeSubspaceArakelovLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceLogHeight ≤ U.relativeSubspaceArakelovLogHeight

The relative logarithmic sup height of a subspace is at most its relative logarithmic Arakelov height.

theorem Submodule.relativeSubspaceArakelovLogHeight_le_mul_log_choose_add_relativeSubspaceLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceArakelovLogHeight ≤ ↑(Module.finrank ℚ K) / 2 * Real.log ↑((Nat.card ι).choose (Module.finrank K ↥U)) + U.relativeSubspaceLogHeight

The relative logarithmic Arakelov height of a subspace U of dimension k exceeds its relative logarithmic sup height by at most [K : ℚ] / 2 · log (#ι.choose k).

@[simp]

theorem Submodule.relativeSubspaceArakelovHeight_bot {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊥.relativeSubspaceArakelovHeight = 1

The zero subspace has relative Arakelov height 1.

@[simp]

theorem Submodule.relativeSubspaceArakelovHeight_top {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊤.relativeSubspaceArakelovHeight = 1

The whole space has relative Arakelov height 1.

@[simp]

theorem Submodule.relativeSubspaceArakelovLogHeight_bot {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊥.relativeSubspaceArakelovLogHeight = 0

The zero subspace has relative logarithmic Arakelov height 0.

@[simp]

theorem Submodule.relativeSubspaceArakelovLogHeight_top {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊤.relativeSubspaceArakelovLogHeight = 0

The whole space has relative logarithmic Arakelov height 0.

@[simp]

theorem Submodule.relativeSubspaceArakelovHeight_span_singleton {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (x : ι → K) : (K ∙ x).relativeSubspaceArakelovHeight = TauCeti.arakelovMulHeight x

The relative Arakelov height of the line spanned by a vector is the Arakelov height of the vector.

@[simp]

theorem Submodule.relativeSubspaceArakelovLogHeight_span_singleton {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (x : ι → K) : (K ∙ x).relativeSubspaceArakelovLogHeight = TauCeti.arakelovLogHeight x

The relative logarithmic Arakelov height of the line spanned by a vector is the logarithmic Arakelov height of the vector.

@[simp]

theorem Submodule.relativeSubspaceArakelovHeight_euclideanDual {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) [Fintype ι] : U.euclideanDual.relativeSubspaceArakelovHeight = U.relativeSubspaceArakelovHeight

Duality of heights. The orthogonal complement of a subspace U of ι → K for the dot product has the relative Arakelov height of U.

@[simp]

theorem Submodule.relativeSubspaceArakelovLogHeight_euclideanDual {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) [Fintype ι] : U.euclideanDual.relativeSubspaceArakelovLogHeight = U.relativeSubspaceArakelovLogHeight

The orthogonal complement of a subspace U of ι → K for the dot product has the relative logarithmic Arakelov height of U.

instance Submodule.instNorthcottRelativeSubspaceArakelovHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : Northcott relativeSubspaceArakelovHeight

The relative Arakelov height of subspaces has the Northcott property: for every B there are finitely many subspaces of ι → K of relative Arakelov height at most B, of all dimensions together.

instance Submodule.instNorthcottRelativeSubspaceArakelovLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : Northcott relativeSubspaceArakelovLogHeight

The relative logarithmic Arakelov height of subspaces has the Northcott property.

The absolute Euclidean height of a subspace

noncomputable def Submodule.subspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : ℝ

The absolute Euclidean height of a subspace U of ι → K: the [K : ℚ]-th root of its relative Arakelov height. It is the absolute Euclidean height TauCeti.height2 of the Plücker coordinates of any basis of U (subspaceHeight_eq_height2_plucker).

noncomputable def Submodule.subspaceLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : ℝ

The absolute logarithmic Euclidean height of a subspace U of ι → K: the logarithm of subspaceHeight U.

theorem Submodule.subspaceLogHeight_eq_log_subspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.subspaceLogHeight = Real.log U.subspaceHeight

The absolute logarithmic height of a subspace is the logarithm of its absolute height.

theorem Submodule.subspaceHeight_pow_finrank {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.subspaceHeight ^ Module.finrank ℚ K = U.relativeSubspaceArakelovHeight

The relative Arakelov height of a subspace is the [K : ℚ]-th power of its absolute height.

theorem Submodule.subspaceLogHeight_eq_relativeSubspaceArakelovLogHeight_div {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.subspaceLogHeight = U.relativeSubspaceArakelovLogHeight / ↑(Module.finrank ℚ K)

The absolute logarithmic height of a subspace is its relative logarithmic Arakelov height divided by [K : ℚ].

theorem Submodule.subspaceHeight_eq_height2_plucker {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {U : Submodule K (ι → K)} {p : ℕ} (b : Module.Basis (Fin p) K ↥U) : U.subspaceHeight = TauCeti.height2 (TauCeti.plucker fun (i : Fin p) => ↑(b i))

The absolute height of U is the absolute Euclidean height of the Plücker coordinates of any basis of U.

theorem Submodule.subspaceHeight_span_range {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {p : ℕ} {x : Fin p → ι → K} (hx : LinearIndependent K x) : (span K (Set.range x)).subspaceHeight = TauCeti.height2 (TauCeti.plucker x)

The absolute height of the span of a linearly independent family is the absolute Euclidean height of its Plücker coordinates.

theorem Submodule.one_le_subspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : 1 ≤ U.subspaceHeight

The absolute height of a subspace is at least 1.

theorem Submodule.subspaceHeight_pos {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : 0 < U.subspaceHeight

The absolute height of a subspace is positive.

theorem Submodule.subspaceLogHeight_nonneg {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : 0 ≤ U.subspaceLogHeight

The absolute logarithmic height of a subspace is nonnegative.

@[simp]

theorem Submodule.subspaceHeight_bot {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊥.subspaceHeight = 1

The zero subspace has absolute height 1.

@[simp]

theorem Submodule.subspaceHeight_top {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊤.subspaceHeight = 1

The whole space has absolute height 1.

@[simp]

theorem Submodule.subspaceLogHeight_bot {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊥.subspaceLogHeight = 0

The zero subspace has absolute logarithmic height 0.

@[simp]

theorem Submodule.subspaceLogHeight_top {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : ⊤.subspaceLogHeight = 0

The whole space has absolute logarithmic height 0.

@[simp]

theorem Submodule.subspaceHeight_span_singleton {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] {x : ι → K} (hx : x ≠ 0) : (K ∙ x).subspaceHeight = TauCeti.height2 x

The absolute height of the line spanned by a nonzero vector is the absolute Euclidean height of the vector.

@[simp]

theorem Submodule.subspaceLogHeight_span_singleton {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (x : ι → K) : (K ∙ x).subspaceLogHeight = Real.log (TauCeti.height2 x)

The absolute logarithmic height of the line spanned by a vector is the logarithm of the absolute Euclidean height of the vector.

@[simp]

theorem Submodule.subspaceHeight_euclideanDual {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) [Fintype ι] : U.euclideanDual.subspaceHeight = U.subspaceHeight

Duality of heights, Evertse–Ferretti (6.13). The orthogonal complement of a subspace U of ι → K for the dot product has the absolute height of U.

@[simp]

theorem Submodule.subspaceLogHeight_euclideanDual {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) [Fintype ι] : U.euclideanDual.subspaceLogHeight = U.subspaceLogHeight

The orthogonal complement of a subspace U of ι → K for the dot product has the absolute logarithmic height of U.

theorem Submodule.relativeSubspaceHeight_rpow_le_subspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceHeight ^ (↑(Module.finrank ℚ K))⁻¹ ≤ U.subspaceHeight

The absolute sup height of a subspace, the [K : ℚ]-th root of its relative sup height, is at most its absolute Euclidean height.

theorem Submodule.subspaceHeight_le_sqrt_choose_mul_relativeSubspaceHeight_rpow {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.subspaceHeight ≤ √↑((Nat.card ι).choose (Module.finrank K ↥U)) * U.relativeSubspaceHeight ^ (↑(Module.finrank ℚ K))⁻¹

The absolute Euclidean height of a subspace U of dimension k is at most √(#ι.choose k) times its absolute sup height, the [K : ℚ]-th root of its relative sup height.

theorem Submodule.relativeSubspaceLogHeight_div_le_subspaceLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.relativeSubspaceLogHeight / ↑(Module.finrank ℚ K) ≤ U.subspaceLogHeight

The absolute logarithmic sup height of a subspace, its relative logarithmic sup height divided by [K : ℚ], is at most its absolute logarithmic Euclidean height.

theorem Submodule.subspaceLogHeight_le_log_choose_div_two_add_relativeSubspaceLogHeight_div {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (U : Submodule K (ι → K)) : U.subspaceLogHeight ≤ Real.log ↑((Nat.card ι).choose (Module.finrank K ↥U)) / 2 + U.relativeSubspaceLogHeight / ↑(Module.finrank ℚ K)

The absolute logarithmic Euclidean height of a subspace U of dimension k exceeds its absolute logarithmic sup height by at most log (#ι.choose k) / 2.

theorem Submodule.finite_subspaceHeight_le {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] (B : ℝ) : {U : Submodule K (ι → K) | U.subspaceHeight ≤ B}.Finite

Northcott's theorem for subspaces (Schmidt): for every B there are finitely many subspaces of ι → K of absolute height at most B, of all dimensions together.

instance Submodule.instNorthcottSubspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : Northcott subspaceHeight

The absolute height of subspaces has the Northcott property.

instance Submodule.instNorthcottSubspaceLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [NumberField K] : Northcott subspaceLogHeight

The absolute logarithmic height of subspaces has the Northcott property.

Over ℚ there are finitely many subspaces of bounded relative logarithmic Arakelov height.

Over ℚ, the line spanned by (2, 2) has absolute height √2: no primitive spanning vector is needed.

Over ℚ, the plane in ℚ³ orthogonal to (1, 2, 2) has absolute height 3, the Euclidean norm of (1, 2, 2).

Over ℚ there are finitely many subspaces of bounded absolute logarithmic height.