Transcendence theory in Lean 4

8 Roy’s lemma

Roy’s lemma on linear spaces of singular matrices. It is the step by which the Structural Rank Conjecture implies the Matrix Coefficient Conjecture of Dasgupta and Kakde [ DK24 ] .

Lemma 8.1 Roy’s lemma
✓

Let \(F\) be an infinite field and \(E\) a linear subspace of the \(n\times n\) matrices over \(F\), all of whose elements are singular. Then there are non-zero \(v,w\in F^{n}\) with

\[ w^{\mathsf T}Av=0\qquad \text{for every }A\in E. \]

Source: [ DK24 , Theorem 2.2 ] , with a proof communicated by D. Roy; a stronger form is [ Wal00 , Proposition 12.5 ] , credited there to Roy (1990).

Proof ▶

Take \(A_0\in E\) of maximal rank \(r\lt n\). For every \(B\in E\), \(B(\ker A_0)\subseteq \operatorname {Im}A_0\): otherwise \(A_0+aB\in E\) would have rank \(r+1\) for all but finitely many \(a\in F\). Take non-zero \(v\in \ker A_0\) and non-zero \(w\) orthogonal to \(\operatorname {Im}A_0\).