The height of a linear subspace #
Schmidt's height of a subspace V : Submodule K (ι → K): the height of its Plücker point
Submodule.pluckerPoint, a point of Projectivization K (Set.powersetCard ι k → K), in each of
the three normalizations the roadmap carries — Mathlib's sup-norm height, the Arakelov height of
Layer 0.1, and the absolute height of Layer 0.4 — with the logarithmic form of each alongside.
The definition is Bombieri–Gubler 2.8.4 and Schmidt 1967, §1. What makes it the right definition
is Submodule.mulHeight_span_singleton: the height of a line is the projective height of the
point that spans it.
Main definitions #
Submodule.mulHeight,Submodule.logHeight: the height of a subspace ofι → K, over any field withHeight.AdmissibleAbsValues.Submodule.arakelovMulHeight,Submodule.arakelovLogHeight: the ℓ²-at-infinity variant, over a number field.Submodule.absMulHeight,Submodule.absLogHeight: the absolute variant, over a field of algebraic numbers.
Main results #
Submodule.mulHeight_span_singleton:Submodule.mulHeight (span K {x}) = Height.mulHeight xforx ≠ 0, and the same for the other three heights. This is the compatibility that fixes the definition; it isexteriorPower.plucker_one_compof Layer 3.1 read throughHeight.mulHeight_comp_equiv.Submodule.mulHeight_span_range: the height of the span of a linearly independent family is the height of its tuple of Plücker coordinates, which byexteriorPower.plucker_applyis its tuple of maximal minors. This is the form the matrix dictionary of 3.3 consumes.Submodule.mulHeight_botandSubmodule.mulHeight_top: the two degenerate ranks, where the exterior power is a line, have height1.Submodule.one_le_mulHeight, and positivity and nonnegativity beside it.Submodule.mulHeight_eq_mulHeight_pluckerPoint: the definition, re-typed along any proof that the rank ofVisk. Every proof enters through this rather than through the definition.Submodule.absMulHeight_eq: over a number field the absolute height of a subspace is the relative one normalized by the degree, as it is for tuples and for projective points.Submodule.mulHeight_le_arakelovMulHeight: the height of a subspace is at most its Arakelov height, the comparison of Layer 0.2 read at the Plücker point.
Set.powersetCard.subsingleton_iff and Projectivization.mulHeight_eq_one_of_subsingleton are
stated here because Mathlib has neither, although both are about Mathlib's own objects — the first
sits beside Set.powersetCard.nontrivial_iff, the second beside
Projectivization.mulHeight. They belong upstream rather than in this library.
Implementation notes #
The rank is not a parameter of the definition. Submodule.mulHeight V is
Projectivization.mulHeight (V.pluckerPoint rfl), taking k := Module.finrank K V, so it is a
total function of V alone: Submodule.mulHeight (V ⊓ W) is well formed without producing a rank
for V ⊓ W first, which is what the submodularity of 3.6 needs.
Submodule.mulHeight_eq_mulHeight_pluckerPoint re-types it along an arbitrary
hV : Module.finrank K V = k — by subst, since k is a variable — and that lemma, not the
definition, is what every proof below uses.
Both degenerate cases are one argument, and neither is a computation of Plücker coordinates: for
Module.finrank K V = 0 and for Module.finrank K V = Fintype.card ι the index type
Set.powersetCard ι (Module.finrank K V) is a subsingleton — only ∅, only Finset.univ — so
every tuple over it has height 1 by the product formula. In particular mulHeight ⊤ = 1 does
not go through exteriorPower.plucker_fin_eq_det, which is stated for ι = Fin n.
The four height families are separate sections rather than one definition parametrized by a
height, because their hypotheses differ: Height.AdmissibleAbsValues K for the first,
NumberField K for the Arakelov height, and CharZero K with Algebra.IsAlgebraic ℚ K for the
absolute one. As the roadmap's convention records, the duplication is in the statements only.
References #
E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006),
2.8.4 for the Plücker construction, Definition 1.5.4 for the absolute sup-norm height, and
Definition 2.8.5 (p. 67) for the absolute Arakelov height of a subspace.
The relative variants here use unnormalized place-weighted products. absMulHeight and
absLogHeight give the absolute sup-norm variants; the Arakelov variants here remain relative.
W. M. Schmidt, "On heights of algebraic subspaces and diophantine approximations", Annals of
Mathematics 85 (1967), 430–472, §1, where the height of a subspace is defined through its
Grassmann coordinates.
This is Layer 3.2 of the ArithmeticHeights roadmap.
Two lemmas that belong upstream #
Set.powersetCard.nontrivial_iff is in Mathlib; its negation is not, and it is what makes the two
degenerate ranks of a subspace height degenerate. Mathlib's Projectivization.mulHeight has no
subsingleton lemma either, although the tuple-level Height.mulHeight_eq_one_of_subsingleton is
there.
A type of n-element subsets is a subsingleton exactly when there is at most one such subset:
n = 0, when only ∅ qualifies, or n at least the cardinality, when only Finset.univ does.
This is the negation of Set.powersetCard.nontrivial_iff.
On a subsingleton index type every point of projective space has height 1; the projective
form of Height.mulHeight_eq_one_of_subsingleton.
The height of a subspace #
The multiplicative height of a linear subspace of ι → K: the projective height of its
Plücker point, following Schmidt. The rank is read off V rather than supplied, so this is a
total function of V.
Equations
- V.mulHeight = (V.pluckerPoint ⋯).mulHeight
Instances For
The logarithmic height of a linear subspace of ι → K.
Equations
- V.logHeight = (V.pluckerPoint ⋯).logHeight
Instances For
The definition, re-typed along an arbitrary proof that V has rank k. Every proof enters
through this.
The logarithmic form of Submodule.mulHeight_eq_mulHeight_pluckerPoint.
The height of a subspace is at least 1.
The zero subspace has height 1: its exterior power is the line spanned by the empty wedge,
whose single coordinate is indexed by ∅.
The whole space has height 1: its exterior power is the line spanned by the wedge of the
standard basis, whose single coordinate is indexed by Finset.univ.
The height of a line is the projective height of a point spanning it. This is the
compatibility that makes the Plücker point the right carrier of the definition: in rank one the
coordinates are the coordinates of the vector itself, re-indexed along
Set.powersetCard.ofSingleton.
The logarithmic form of Submodule.mulHeight_span_singleton.
The height of the span of a linearly independent family is the height of its tuple of
Plücker coordinates — by exteriorPower.plucker_apply, of its tuple of maximal minors. This is
the form the matrix dictionary of 3.3 consumes.
The logarithmic form of Submodule.mulHeight_span_range.
The Arakelov height of a subspace #
The same definition with the ℓ² norm at the archimedean places, which is the normalization the Siegel-lemma literature states its constants in.
The relative multiplicative Arakelov height of a linear subspace of ι → K,
exp([K : ℚ] · h_Ar(V)) in the absolute logarithmic convention of
Bombieri–Gubler Definition 2.8.5.
Equations
Instances For
The relative logarithmic Arakelov height of a linear subspace of ι → K,
[K : ℚ] · h_Ar(V) in the absolute convention of Bombieri–Gubler Definition 2.8.5.
Equations
Instances For
The Arakelov height of a line is the projective Arakelov height of a point spanning it.
The logarithmic form of Submodule.arakelovMulHeight_span_singleton.
The Arakelov height of the span of a linearly independent family is the Arakelov height of its tuple of maximal minors.
The logarithmic form of Submodule.arakelovMulHeight_span_range.
The height of a subspace is at most its Arakelov height, with no constant: the two
normalizations differ only at the archimedean places, where ‖·‖_∞ ≤ ‖·‖_2. This is
Projectivization.mulHeight_le_arakelovMulHeight at the Plücker point, and it is what carries
Northcott for subspaces (3.7) from one normalization to the other.
The reverse bound is not stated: it carries the constant
(Fintype.card ι).choose (finrank K V) ^ (Height.totalWeight K / 2), the number of Plücker
coordinates rather than the dimension of the ambient space, and nothing below needs it.
The logarithmic form of Submodule.mulHeight_le_arakelovMulHeight.
The absolute height of a subspace #
The sup-norm variant that does not depend on the field the subspace is written over.
absLogHeight is the literature's h(V), and absMulHeight is its exponential.
This is one of the six Northcott statements of 3.7.
The absolute multiplicative height of a linear subspace of ι → K,
exp(h(V)) via Bombieri–Gubler 2.8.4 and Definition 1.5.4.
Equations
- V.absMulHeight = (V.pluckerPoint ⋯).absMulHeight
Instances For
The absolute logarithmic height of a linear subspace of ι → K,
h(V) via Bombieri–Gubler 2.8.4 and Definition 1.5.4.
Equations
- V.absLogHeight = (V.pluckerPoint ⋯).absLogHeight
Instances For
The absolute height of a line is the absolute height of a point spanning it.
The logarithmic form of Submodule.absMulHeight_span_singleton.
The absolute height of the span of a linearly independent family is the absolute height of its tuple of maximal minors.
The logarithmic form of Submodule.absMulHeight_span_range.
Over a number field the absolute height of a subspace is the relative one normalized by the degree, exactly as for tuples and for projective points.
The logarithmic form of Submodule.absMulHeight_eq.