A multilinear form on matrices is determined on the diagonal by the invertible matrices

Let Θ be a multilinear form in ι matrix arguments over a commutative semiring K. Its diagonal Y ↦ Θ (Y, …, Y) is a polynomial function of the entries of Y: expanding each argument in the matrix units Matrix.single i j 1 writes it as a sum, over the functions a : ι → m × n, of the constant Θ (fun i => single (a i).1 (a i).2 1) times the monomial ∏ᵢ Y (a i).1 (a i).2. The matrices need not be square. That is MultilinearMap.exists_mvPolynomial_eval_eq_apply_const below.

Over an infinite field the invertible square matrices are Zariski dense, so such a polynomial function vanishes everywhere as soon as it vanishes on GL m K (MvPolynomial.eq_of_eval_eq_on_gl). Hence a multilinear form whose diagonal kills every invertible matrix has zero diagonal: MultilinearMap.apply_const_eq_zero_of_eq_zero_on_gl.

This is the form in which density is used to pass from the invertible diagonal operators g^{⊗ι} on a tensor power to all of them; the argument is stated here on matrices, where the ambient polynomial ring MvPolynomial (m × m) K and the density statement live.

Main results

• MultilinearMap.exists_mvPolynomial_eval_eq_apply_const: the diagonal of a multilinear form on (possibly rectangular) matrices is the evaluation of a polynomial in the matrix entries.
• MultilinearMap.apply_const_eq_zero_of_eq_zero_on_gl: over an infinite field, a multilinear form on matrices whose diagonal vanishes on the invertible matrices has vanishing diagonal.

theorem MultilinearMap.exists_mvPolynomial_eval_eq_apply_const {ι : Type u} {m : Type v} {n : Type v'} {K : Type w} [Finite ι] [Finite m] [Finite n] [CommSemiring K] (Θ : MultilinearMap K (fun (x : ι) => Matrix m n K) K) : ∃ (P : MvPolynomial (m × n) K), ∀ (Y : Matrix m n K), (MvPolynomial.eval fun (p : m × n) => Y p.1 p.2) P = Θ fun (x : ι) => Y

The diagonal of a multilinear form on matrices is a polynomial in the matrix entries. Expanding each of the ι arguments in the matrix units, the value Θ (Y, …, Y) is a sum of constants times monomials ∏ᵢ Y (a i).1 (a i).2 indexed by the functions a : ι → m × n.

theorem MultilinearMap.apply_const_eq_zero_of_eq_zero_on_gl {ι : Type u} {m : Type v} {K : Type w} [Finite ι] [Fintype m] [DecidableEq m] [Field K] [Infinite K] (Θ : MultilinearMap K (fun (x : ι) => Matrix m m K) K) (h : ∀ (g : GL m K), (Θ fun (x : ι) => ↑g) = 0) (Y : Matrix m m K) : (Θ fun (x : ι) => Y) = 0

A multilinear form on matrices whose diagonal vanishes on the invertible matrices has vanishing diagonal. The diagonal is a polynomial function of the matrix entries (the square case of MultilinearMap.exists_mvPolynomial_eval_eq_apply_const), and over an infinite field the invertible matrices are Zariski dense.