The height of a matrix #
The height of a matrix here is the sup-norm height of the tuple of its entries.
Row-space heights instead use the tuple of maximal minors and belong to Layer 3.
Bombieri–Vaaler's H(A) is the absolute Arakelov height of those minors, using Euclidean norms
at infinity. This file uses Matrix.mulHeight for the sup-norm entry height.
The content of the file is four bounds.
- The product bound
Matrix.mulHeight_mul_le, with the constantFintype.card n ^ totalWeight Kfor the inner index typen. It is the tuple sum bound of Layer 2.4 applied to the multiplication table of the entries ofAand ofB: an entry ofA * Bis a sum ofFintype.card nentries of that one table, and the Segre relation evaluates its height. - The Arakelov product bound
Matrix.arakelovMulHeight_mul_le, with constant exactly1. Cauchy–Schwarz entry by entry produces the Frobenius norm, which is submultiplicative; the cardinality of the inner index type is not paid at all. This is the matrix form ofNumberField.arakelovMulHeight_linearMap_apply_leand the reason Layer 0 carries two normalizations. - The determinant bound
Matrix.mulHeight₁_det_le. It cannot be stated withmulHeight Aon the right:A ↦ c • Afixes the projective height of the matrix and multiplies the determinant byc ^ n, whichMatrix.exists_not_mulHeight₁_det_lerecords. What is true uses the affine height of Layer 0.5, and the sharp form of it is columnwise, one affine column height per column, with the constant(Fintype.card n)! ^ totalWeight Kfrom the Leibniz expansion. - The action on tuples,
Matrix.mulHeight_mulVec_le, which is Mathlib'sHeight.mulHeight_linearMap_apply_leread through the definition, and its Arakelov companion.
The Leibniz expansion carries the signs of the permutations, so the tuple sum bound is used here
through Height.mulHeight_sum_sign_comp_le', a version whose summands may be multiplied by ±1.
That version is deduced from the unsigned one by doubling the alphabet with a Bool, whose two
letters 1 and -1 have height 1.
Main definitions #
Matrix.mulHeight AandMatrix.logHeight A: the height of the tuple of entries ofA.Matrix.mulHeightAff AandMatrix.logHeightAff A: its affine counterpart, the height of the tuple of entries with a coordinate1appended.Matrix.arakelovMulHeight AandMatrix.arakelovLogHeight A: the same in the Arakelov normalization, over a number field.
Main results #
Matrix.mulHeight_transpose,Matrix.mulHeight_submatrix_le,Matrix.mulHeight_submatrix_equivandMatrix.mulHeight_smul: invariance under transpose, under re-indexing of rows and columns — in particular under row and column permutations — and under scaling, and the submatrix bound.Matrix.mulHeight_mul_leandMatrix.logHeight_mul_le: the product bound.Matrix.arakelovMulHeight_mul_leandMatrix.arakelovLogHeight_mul_le: the product bound in the Arakelov normalization, with constant1.Matrix.mulHeight₁_det_leandMatrix.logHeight₁_det_le: the determinant against the affine heights of the columns, andMatrix.mulHeight₁_det_le_mulHeightAff_powagainst the affine height of the matrix.Matrix.exists_not_mulHeight₁_det_le: no constant bounds the height of a determinant by the projective height of the matrix.Height.mulHeight_sum_sign_comp_le': the signed tuple sum bound.
Implementation notes #
Matrix m n K is definitionally m → n → K, and Height.mulHeight takes a tuple, so
Matrix.mulHeight is the height of fun q : m × n ↦ A q.1 q.2. Every statement about
re-indexing is then a statement about Prod.map, and transpose is Equiv.prodComm.
The finiteness hypotheses are Finite wherever the height alone is involved and Fintype only
where a matrix product or a determinant is formed.
Height.mulHeight_sum_sign_comp_le' belongs next to the unsigned tuple sum bound of Layer 2.4;
it is here because the determinant is the only consumer so far.
References #
E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006),
2.9.8 (p. 75) for the entry-tuple height H(A), and Definition 2.8.1 with 2.8.2–2.8.3
(pp. 66–67) for the local Euclidean factors and absolute Arakelov normalization.
Definition 2.8.11 instead concerns the Grassmannian row-space height, treated separately in
ArithmeticHeights.RowSpace.
This is Layer 2.5 of the ArithmeticHeights roadmap.
The signed tuple sum bound. Height.mulHeight_sum_comp_le' with each summand allowed a
sign: if in each coordinate i at most n entries of one tuple w, each possibly negated, are
summed, the height of the tuple of sums is at most n ^ totalWeight K times mulHeight w.
Signs cost nothing, because v (-x) = v x at every absolute value. Formally this is the unsigned
bound for the doubled alphabet κ × Bool, whose height is mulHeight w by the Segre relation and
Height.mulHeight_boolSign. The Leibniz expansion of a determinant is the intended consumer.
The height of a matrix is the sup-norm height of the tuple of its entries,
corresponding to the entry-tuple construction in Bombieri–Gubler 2.9.8.
Bombieri–Vaaler's H(A) instead uses the absolute Arakelov height of the maximal minors.
Equations
- A.mulHeight = Height.mulHeight fun (q : m × n) => A q.1 q.2
Instances For
The logarithmic height of a matrix. As everywhere in this development, the logarithmic height is defined as the logarithm of the multiplicative one and never independently.
Instances For
The affine height of a matrix: the height of the tuple of its entries with a coordinate
1 appended, Height.mulHeightAff of the entries. Unlike Matrix.mulHeight it is not invariant
under scaling, which is exactly what a bound on the determinant needs.
Equations
- A.mulHeightAff = Height.mulHeightAff fun (q : m × n) => A q.1 q.2
Instances For
The logarithmic affine height of a matrix.
Equations
Instances For
The height of a matrix is invariant under transpose: transposing re-indexes the entries by
Equiv.prodComm.
Re-indexing rows and columns by equivalences leaves the height unchanged; taking
e and e' to be permutations, the height is invariant under row and column permutations.
The affine height of a column of A is at most the affine height of A: a column is a
sub-tuple of the entries, and the appended coordinate 1 is common to both.
The product bound. An entry of A * B is a sum of
Fintype.card n entries of the multiplication table of the entries of A and of B, so the
tuple sum bound of Layer 2.4 applies with #s = Fintype.card n, and the Segre relation evaluates
the height of that table as mulHeight A * mulHeight B.
n must be nonempty: for n empty A * B = 0 has the junk height 1 against a right-hand side
of 0. The constant is sharp, and its exponent totalWeight K is needed as soon as K has
degree > 1; both are the examples at the end of this file. In the Arakelov normalization the
constant disappears entirely, Matrix.arakelovMulHeight_mul_le.
The logarithmic form of Matrix.mulHeight_mul_le.
The action on tuples, Mathlib's Height.mulHeight_linearMap_apply_le read through the
definition of Matrix.mulHeight. Nothing is reproved here.
The logarithmic form of Matrix.mulHeight_mulVec_le.
The height of a determinant, from the Leibniz expansion. The determinant is a sum of
(Fintype.card n)! products, one entry from each column, so the signed tuple sum bound applies to
the multiplication table of the affine columns and the Segre relation of
Height.mulHeight_fun_prod_eq evaluates its height as the product of the affine column heights.
The right-hand side cannot be made scaling-invariant: see
Matrix.exists_not_mulHeight₁_det_le.
The logarithmic form of Matrix.mulHeight₁_det_le.
Matrix.mulHeight₁_det_le with the affine height of the whole matrix in place of the affine
heights of its columns. This is the form the roadmap states, except that the height on the right
is the affine one.
The logarithmic form of Matrix.mulHeight₁_det_le_mulHeightAff_pow.
The determinant is not bounded by the projective height of the matrix. For a 1 × 1
matrix the index type is a subsingleton, so mulHeight A = 1 whatever the entry is, while the
determinant is that entry. This is the same scaling obstruction as in Layer 2.4: A ↦ c • A
fixes mulHeight A and multiplies A.det by c ^ n. The affine height of
Matrix.mulHeight₁_det_le is what the statement needs.
Matrices in the Arakelov normalization #
At an infinite place the local factor of the Arakelov height is the Frobenius norm of the matrix,
and Cauchy–Schwarz entry by entry makes it submultiplicative; at a finite place the sup norm is
submultiplicative by the ultrametric inequality. So the constant
Fintype.card n ^ totalWeight K of Matrix.mulHeight_mul_le disappears.
The Arakelov height of a matrix: the Arakelov height of the tuple of its entries, so the Frobenius norm at each infinite place and the sup norm at each finite one.
Equations
- A.arakelovMulHeight = NumberField.arakelovMulHeight fun (q : m × n) => A q.1 q.2
Instances For
The logarithmic Arakelov height of a matrix.
Equations
Instances For
The Arakelov product bound, with constant 1. Against
Fintype.card n ^ totalWeight K for the sup-norm height of Matrix.mulHeight_mul_le, and with no
hypothesis on the index types at all — for n empty, A * B = 0 has the junk height 1, which
is at most the right-hand side. This is the matrix form of
NumberField.arakelovMulHeight_linearMap_apply_le.
The logarithmic form of Matrix.arakelovMulHeight_mul_le: in the Arakelov normalization a
matrix product costs nothing beyond the two heights.
The action on tuples in the Arakelov normalization, from
NumberField.arakelovMulHeight_linearMap_apply_le.
The logarithmic form of Matrix.arakelovMulHeight_mulVec_le.
Examples #
The tests that fix the constants of the product bound: that Fintype.card n ^ totalWeight K is
attained, that its exponent is needed as soon as K has degree > 1 — the rejection test the
roadmap states over ℚ(i), here for every number field at once — that [Nonempty n] cannot be
dropped, and that the Arakelov constant 1 is attained.