The duality theorem for the height of a subspace #

A subspace and its annihilator have the same height. This is W. M. Schmidt's theorem: the Plücker coordinates of the annihilator are those of the subspace read at the complementary index, up to a sign at each index and one common nonzero factor, and every height in this development is insensitive to exactly that much — a signed reindexing and a scalar.

Main results #

Submodule.mulHeight_comap_piEquiv_dualAnnihilator, with its Arakelov and absolute companions Submodule.arakelovMulHeight_comap_piEquiv_dualAnnihilator and Submodule.absMulHeight_comap_piEquiv_dualAnnihilator and every logarithmic form: the duality theorem, the height of V against the height of its annihilator, transported back to ι → K along the standard basis.
Matrix.mulHeight_ker_mulVecLin and its five companions: the solution space of A x = 0 and the row space of A have the same height in each supported normalization. The Arakelov case corresponds to Bombieri–Gubler Corollary 2.8.12.
Submodule.exists_plucker_eq_plucker_compl: the coordinate statement behind both. A subspace and its annihilator have bases whose Plücker coordinates agree at complementary indices up to a sign and one common nonzero factor — Schmidt's involution τ.
Submodule.mem_comap_piEquiv_dualAnnihilator: the transported annihilator is the orthogonal complement for the standard bilinear form, and Submodule.eq_comap_piEquiv_dualAnnihilator_of_forall_dotProduct_eq_zero is that reading as a way into the theorems above. Submodule.comap_piEquiv_dualAnnihilator_eq_map is the same subspace in the other spelling, the map along the inverse identification.
Height.mulHeight_eq_of_forall_eq_or_eq_neg and its Arakelov and absolute companions: no height in this development sees a change of sign in a coordinate. These are statements about Mathlib's heights and belong upstream.

Implementation notes #

The annihilator lives in the dual space, so it is transported back to ι → K along Module.piEquiv ι K K, whose value at x is the functional v ↦ v ⬝ᵥ x; the transported annihilator is therefore the orthogonal complement of V for the standard bilinear form. Submodule.comap_piEquiv_dualAnnihilator_eq_map turns the comap used here into the map along the inverse equivalence, which is the other spelling in use.

⚠ The annihilator and not the orthogonal complement is what the proof must use, even though the two are identified here. Over a field that is not formally real the two summands V and V^⊥ can meet — over ℚ(i), the line spanned by (1, i) is its own orthogonal complement — so the matrix whose rows are a basis of V stacked on a basis of V^⊥ is singular, and every argument through its determinant fails. The proof below is stated for a complement W of V, which always exists, and reaches the annihilator through the dual basis.

The proof is elementary, and in particular uses neither a Laplace expansion along a block of rows nor Jacobi's identity for the complementary minors of an inverse, neither of which Mathlib has. Instead: let the rows of C be a basis of ι → K whose first block is a basis of V, and let the rows of D be the dual basis read back in ι → K, so that C * Dᵀ = 1. For a set s of k columns, multiply C by the matrix whose first k columns are the standard basis vectors at s and whose remaining columns are the second block of Dᵀ. The product is block triangular with the s-minor of the first block of C in one corner and an identity in the other, while the second factor, read through the enumeration of ι that lists s and then its complement, is block triangular with the complementary minor of the second block of D in one corner. Two applications of Matrix.det_fromBlocks_zero₁₂ and Matrix.det_fromBlocks_zero₂₁ give the identity, and the factor that appears is the determinant of C read through that enumeration, which depends on s only through a permutation sign (Matrix.det_permute').

References #

W. M. Schmidt, On heights of algebraic subspaces and diophantine approximations, Annals of Mathematics 85 (1967), §1, equations (2) and (4), where the involution on Grassmann coordinates that reverses the index order and attaches a sign is what makes the theorem hold in every normalization at once. E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Proposition 2.8.10 and Corollary 2.8.12 for the absolute Arakelov version. The same Plücker identity also gives the sup-norm counterparts here. The underlying linear algebra is Hindry–Silverman, Diophantine Geometry: An Introduction, Exercise A.1.11(c).

This is Layer 3.5 of the ArithmeticHeights roadmap.

The duality theorem for the height of a subspace #

Main results #

Implementation notes #

References #

Worked examples #