The row space of a matrix and the height of its maximal minors #
The dictionary between a matrix of full row rank and the subspace it spans: the Plücker
coordinates of the row space are the maximal minors, so the height of the row space is the height
of the tuple of minors, and left multiplication by an invertible matrix — a row operation — leaves
it unchanged. That invariance is what distinguishes the height of the row space from
Matrix.mulHeight, the height of the entries of Layer 2.5, and it is the reason Bombieri–Vaaler
can improve on the naïve Siegel bound.
Main definitions #
None, deliberately. The row space of A is Submodule.span R (Set.range A.row), which is
Mathlib's LinearMap.range A.vecMulLinear by range_vecMulLinear, and the tuple of maximal minors
is exteriorPower.plucker m A.row of Layer 3.1. A third name for either would force every later
statement to choose between three spellings of one object.
Main results #
Matrix.plucker_row_eq_det_submatrix: the Plücker coordinate ofAat a setsof columns is the determinant of the submatrix on those columns, taken in increasing order. This is the index identification, andMatrix.plucker_row_eq_det_submatrix_orderIsorestates it withFinset.orderIsoOfFinin place ofFinset.orderEmbOfFin.Matrix.plucker_row_mul:plucker m (U * A).row = U.det • plucker m A.row, for every squareUand over any commutative ring — the determinant identity underlying the height invariance in Bombieri–Vaaler (2.5).Matrix.span_range_row_mul: forUof unit determinant the row space itself is unchanged, whenceMatrix.mulHeight_span_range_row_muland its Arakelov and absolute companions.Matrix.mulHeight_span_range_rowandMatrix.arakelovMulHeight_span_range_row: the height of the row space is the height of the tuple of maximal minors in each chosen normalization. The relative Arakelov version corresponds to Bombieri–Vaaler's absoluteH(A)after raising to the number-field degree. These row-space heights differ fromMatrix.mulHeight A.Matrix.linearIndependent_row_iff_rank_eqandMatrix.linearIndependent_row_iff_plucker_row_ne_zero: full row rank, in the two forms that the statements above take as a hypothesis.
Implementation notes #
The invariance under row operations is not a theorem about heights. Matrix.span_range_row_mul is
an equality of submodules, and every height statement below is one congrArg away from it,
because Layer 3.2 defines the height of a subspace as a function of the subspace alone. The
mathematical content sits in that span equality and, quantitatively, in Matrix.plucker_row_mul.
Matrix.plucker_row_mul needs no hypothesis on U, no field, and no expansion of an alternating
map along a matrix — which is fortunate, since Mathlib has no such expansion. The proof is Layer
3.1 used twice: exteriorPower.plucker_fin_eq_det says that the single Plücker coordinate of a
square family is its determinant, so the wedge of the rows of U is U.det times the wedge of the
standard basis; and exteriorPower.plucker_eq_smul_iff transports a proportionality of coordinate
tuples to one of wedges. exteriorPower.map then pushes the relation along A.vecMulLinear,
whose composition with the rows of U is the rows of U * A — by rfl.
References #
E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006),
Remark 2.8.7 for the dictionary, Definition 2.8.11 for the Arakelov normalization of the row-space
height, and 2.9.8 for the height of the entries, which is a different number and is Layer 2.5 here.
The book's h_Ar is absolute logarithmic; the relative multiplicative Arakelov height here is
exp([K : ℚ] · h_Ar(A)) in that convention.
E. Bombieri and J. Vaaler, "On Siegel's lemma", Inventiones Mathematicae 73 (1983), 11–32,
equation (2.5), where the invariance is the statement that the height is intrinsic on the
Grassmannian. W. M. Schmidt, "On heights of algebraic subspaces and diophantine approximations",
Annals of Mathematics 85 (1967), 430–472, §1.
This is Layer 3.3 of the ArithmeticHeights roadmap.
The Plücker coordinates of a matrix are its maximal minors #
The Plücker coordinates of a matrix are its maximal minors. The coordinate at a set s of
m columns is the determinant of the submatrix on those columns, enumerated in increasing order.
The enumeration is Mathlib's Finset.orderEmbOfFin, the one Set.powersetCard.ofFinEmbEquiv
already fixes, so no later statement has to choose it again.
Matrix.plucker_row_eq_det_submatrix with Finset.orderIsoOfFin in place of
Finset.orderEmbOfFin; the two enumerations agree by Finset.coe_orderIsoOfFin_apply.
Row operations multiply the Plücker coordinates by a determinant #
The rows of the identity matrix are the standard basis.
The wedge of the rows of a square matrix is its determinant times the wedge of the standard
basis. This is exteriorPower.plucker_fin_eq_det read through the injectivity of the coordinate
map on the top exterior power, which is a line.
A row operation multiplies the tuple of maximal minors by the determinant. This identity
underlies the height invariance in Bombieri–Vaaler (2.5). No hypothesis on U is needed:
for U singular both sides vanish.
The row space #
A row operation does not change the row space. Everything below about the height of a row
space is this equality followed by a congrArg, the height of Layer 3.2 being a function of the
subspace alone. The row index is an arbitrary finite type: Layer 5.6 multiplies by a
block-diagonal matrix whose rows are indexed by a product.
Full row rank #
Full row rank, in the form Mathlib's Matrix.rank takes.
A matrix has a maximal independent family of rows, of size its rank, spanning the same row
space: f picks out R = rank A of the rows, the submatrix on them has independent rows, and its
row space is that of A. This is what lets a bound in terms of the rows be paid rank A times
rather than once per row.
Full row rank, in minors: a matrix has independent rows exactly when some maximal minor is
nonzero. This is exteriorPower.plucker_eq_zero_iff of Layer 3.1, and it is what makes the height
of the row space a statement about a nonzero tuple.
The height of the row space #
The height of the row space is the height of the tuple of maximal minors (Bombieri–Gubler,
Remark 2.8.7). This uses sup norms, while Bombieri–Vaaler's H(A) uses the absolute Arakelov
height of the minors. Matrix.mulHeight A instead measures the entries.
The logarithmic form of Matrix.mulHeight_span_range_row.
The sup-norm height of the row space is invariant under row operations. This is the sup-norm counterpart of the Arakelov height invariance in Bombieri–Vaaler (2.5).
The logarithmic form of Matrix.mulHeight_span_range_row_mul.
The same invariance read on the tuple of minors rather than on the subspace: a row operation
scales it by U.det, and the projective height does not see a scalar.
The logarithmic form of Matrix.mulHeight_plucker_row_mul.
The relative Arakelov height of the row space is that of its tuple of maximal minors.
This is exp([K : ℚ] · h_Ar(A)) for the absolute logarithmic matrix height of
Bombieri–Gubler Definition 2.8.11. The Siegel-lemma constants of Layer 5 use the relative
multiplicative normalization here.
The logarithmic form of Matrix.arakelovMulHeight_span_range_row.
The absolute sup-norm height of the row space is that of its tuple of maximal minors.
Bombieri–Vaaler's H(A) uses the Arakelov normalization instead.
The logarithmic form of Matrix.absMulHeight_span_range_row.