The relative height of a subspace

Let K be a field with admissible absolute values (Height.AdmissibleAbsValues K), for instance a number field, and let ι be a finite linearly ordered type. The relative height of a subspace U of K^ι is the multiplicative height of its Plücker point, that is, the projective height Height.mulHeight of the Plücker coordinates of any basis of U. Its logarithm is the relative logarithmic height. Neither needs a number field or characteristic zero.

The zero subspace and the whole space have height 1, and a line has the height of any nonzero vector spanning it. The height of a subspace does not depend on the spanning vectors: over ℚ the line spanned by (2, 2) has height 1, so no primitive spanning vector is needed.

A subspace and its orthogonal complement for the dot product, Submodule.euclideanDual, have the same height: up to a common nonzero factor and signs, the Plücker coordinates of the complement are the complementary Plücker coordinates of the subspace. Over ℚ, the line spanned by (1, 2) and the line spanned by (-2, 1), its orthogonal complement in ℚ², both have height 2.

If the field has finitely many elements of bounded height, for instance a number field, then K^ι has finitely many subspaces of bounded height, of all dimensions together. A subspace is determined by its dimension and its Plücker point, and the projective space of each dimension has finitely many points of bounded height.

Main definitions

• Submodule.relativeSubspaceHeight U: the multiplicative height of the Plücker point of U.
• Submodule.relativeSubspaceLogHeight U: its logarithm.

Main results

• Submodule.relativeSubspaceHeight_eq_mulHeight_plucker: the height of U is the height of the Plücker coordinates of any basis of U.
• Submodule.relativeSubspaceHeight_span_range: the height of the span of a linearly independent family is the height of its Plücker coordinates.
• Submodule.relativeSubspaceHeight_bot, Submodule.relativeSubspaceHeight_top: the zero subspace and the whole space have height 1.
• Submodule.relativeSubspaceHeight_span_singleton: the line spanned by a nonzero vector has the height of that vector.
• Submodule.relativeSubspaceHeight_euclideanDual: the orthogonal complement of U for the dot product has the height of U.
• Submodule.instNorthcottRelativeSubspaceHeight and Submodule.instNorthcottRelativeSubspaceLogHeight: the Northcott property for the relative height and the relative logarithmic height.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §2.8.
• J.-H. Evertse and R. G. Ferretti, A further improvement of the quantitative Subspace Theorem, Ann. of Math. 177 (2013), §6.1, (6.13).
• W. M. Schmidt, On heights of algebraic subspaces and diophantine approximations, Ann. of Math. 85 (1967), 430–472.

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

The relative multiplicative height of a subspace U of ι → K: the multiplicative height Height.mulHeight of the Plücker coordinates of any basis of U (relativeSubspaceHeight_eq_mulHeight_plucker).

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

The relative logarithmic height of a subspace U of ι → K: the logarithmic height Height.logHeight of the Plücker coordinates of any basis of U.

theorem Submodule.relativeSubspaceLogHeight_eq_log_relativeSubspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] (U : Submodule K (ι → K)) : U.relativeSubspaceLogHeight = Real.log U.relativeSubspaceHeight

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

theorem Submodule.relativeSubspaceHeight_eq_mulHeight_plucker {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] {U : Submodule K (ι → K)} {p : ℕ} (b : Module.Basis (Fin p) K ↥U) : U.relativeSubspaceHeight = Height.mulHeight (TauCeti.plucker fun (i : Fin p) => ↑(b i))

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

theorem Submodule.relativeSubspaceLogHeight_eq_logHeight_plucker {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] {U : Submodule K (ι → K)} {p : ℕ} (b : Module.Basis (Fin p) K ↥U) : U.relativeSubspaceLogHeight = Height.logHeight (TauCeti.plucker fun (i : Fin p) => ↑(b i))

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

theorem Submodule.relativeSubspaceHeight_span_range {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] {p : ℕ} {x : Fin p → ι → K} (hx : LinearIndependent K x) : (span K (Set.range x)).relativeSubspaceHeight = Height.mulHeight (TauCeti.plucker x)

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

theorem Submodule.relativeSubspaceLogHeight_span_range {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] {p : ℕ} {x : Fin p → ι → K} (hx : LinearIndependent K x) : (span K (Set.range x)).relativeSubspaceLogHeight = Height.logHeight (TauCeti.plucker x)

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

theorem Submodule.one_le_relativeSubspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] (U : Submodule K (ι → K)) : 1 ≤ U.relativeSubspaceHeight

The relative height of a subspace is at least 1.

theorem Submodule.relativeSubspaceHeight_pos {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] (U : Submodule K (ι → K)) : 0 < U.relativeSubspaceHeight

The relative height of a subspace is positive.

theorem Submodule.relativeSubspaceLogHeight_nonneg {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] (U : Submodule K (ι → K)) : 0 ≤ U.relativeSubspaceLogHeight

The relative logarithmic height of a subspace is nonnegative.

@[simp]

theorem Submodule.relativeSubspaceHeight_bot {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] : ⊥.relativeSubspaceHeight = 1

The zero subspace has relative height 1.

@[simp]

theorem Submodule.relativeSubspaceHeight_top {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] : ⊤.relativeSubspaceHeight = 1

The whole space has relative height 1.

@[simp]

theorem Submodule.relativeSubspaceLogHeight_bot {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] : ⊥.relativeSubspaceLogHeight = 0

The zero subspace has relative logarithmic height 0.

@[simp]

theorem Submodule.relativeSubspaceLogHeight_top {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] : ⊤.relativeSubspaceLogHeight = 0

The whole space has relative logarithmic height 0.

@[simp]

theorem Submodule.relativeSubspaceHeight_span_singleton {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] {x : ι → K} (hx : x ≠ 0) : (K ∙ x).relativeSubspaceHeight = Height.mulHeight x

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

@[simp]

theorem Submodule.relativeSubspaceLogHeight_span_singleton {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] {x : ι → K} (hx : x ≠ 0) : (K ∙ x).relativeSubspaceLogHeight = Height.logHeight x

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

instance Submodule.instNorthcottRelativeSubspaceHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] [Northcott Height.mulHeight₁] : Northcott relativeSubspaceHeight

The relative height of subspaces has the Northcott property whenever the scalar height does, for instance over a number field: for every B there are finitely many subspaces of ι → K of relative height at most B, of all dimensions together.

instance Submodule.instNorthcottRelativeSubspaceLogHeight {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] [Height.AdmissibleAbsValues K] [Northcott relativeSubspaceHeight] : Northcott relativeSubspaceLogHeight

The relative logarithmic height of subspaces has the Northcott property whenever the relative height does.

@[simp]

theorem Submodule.relativeSubspaceHeight_euclideanDual {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Fintype ι] [Field K] [Height.AdmissibleAbsValues K] (U : Submodule K (ι → K)) : U.euclideanDual.relativeSubspaceHeight = U.relativeSubspaceHeight

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

@[simp]

theorem Submodule.relativeSubspaceLogHeight_euclideanDual {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Fintype ι] [Field K] [Height.AdmissibleAbsValues K] (U : Submodule K (ι → K)) : U.euclideanDual.relativeSubspaceLogHeight = U.relativeSubspaceLogHeight

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

The line spanned by (2, 2) has height 1: no primitive spanning vector is needed. The line spanned by (1, 2) has height 2.

In ℚ² the orthogonal complement of the line spanned by (1, 2) is the line spanned by (-2, 1), so the two lines have the same height.

Over ℚ the Northcott instance applies through Mathlib's number-field instance for the scalar height.