The bialternant Jacobi–Trudi identity

The matrix of variable powers x_j^{v i + (k−1−i)} factors as the column-reversed Jacobi–Trudi matrix of complete homogeneous polynomials times the signed elementary matrix in the complementary variables — entrywise this is the resolvent. Taking determinants and anchoring at v = 0 gives the bialternant form:

`det (powMat v) = det (jtMat v) * det (powMat 0)`,

the polynomial Jacobi–Trudi identity a_{v+δ} = s_v · a_δ.

noncomputable def RS.powMat {k : ℕ} (v : Fin k → ℕ) : Matrix (Fin k) (Fin k) (MvPolynomial (Fin k) ℂ)

The alternant matrix of variable powers.

Equations

• RS.powMat v = Matrix.of fun (i j : Fin k) => MvPolynomial.X j ^ (v i + (k - 1 - ↑i))

noncomputable def RS.hMat {k : ℕ} (v : Fin k → ℕ) : Matrix (Fin k) (Fin k) (MvPolynomial (Fin k) ℂ)

The column-reversed complete homogeneous matrix.

Equations

• RS.hMat v = Matrix.of fun (i r : Fin k) => RS.hSubZ Finset.univ (↑(v i) + (↑k - 1 - ↑↑r) - ↑↑i)

noncomputable def RS.jtMat {k : ℕ} (v : Fin k → ℕ) : Matrix (Fin k) (Fin k) (MvPolynomial (Fin k) ℂ)

The Jacobi–Trudi matrix of complete homogeneous polynomials.

Equations

• RS.jtMat v = Matrix.of fun (i j : Fin k) => RS.hSubZ Finset.univ (↑(v i) + ↑↑j - ↑↑i)

noncomputable def RS.eMat (k : ℕ) : Matrix (Fin k) (Fin k) (MvPolynomial (Fin k) ℂ)

The signed elementary matrix in complementary variables.

Equations

• RS.eMat k = Matrix.of fun (r j : Fin k) => (-1) ^ ↑r * RS.eSub (Finset.univ.erase j) ↑r

theorem RS.powMat_eq_mul {k : ℕ} (v : Fin k → ℕ) : powMat v = hMat v * eMat k

The entrywise factorization via the resolvent.

theorem RS.hMat_eq_submatrix {k : ℕ} (v : Fin k → ℕ) : hMat v = (jtMat v).submatrix id ⇑Fin.revPerm

The reversed columns of hMat give the Jacobi–Trudi matrix.

theorem RS.det_hMat {k : ℕ} (v : Fin k → ℕ) : (hMat v).det = ↑↑(Equiv.Perm.sign Fin.revPerm) * (jtMat v).det

The power matrix's determinant is the Jacobi–Trudi matrix's, up to the column-reversal sign.

theorem RS.det_jtMat_zero {k : ℕ} : (jtMat fun (x : Fin k) => 0).det = 1

The zero-shape Jacobi–Trudi matrix is upper triangular with unit diagonal.

theorem RS.bialternant {k : ℕ} (v : Fin k → ℕ) : (powMat v).det = (jtMat v).det * (powMat fun (x : Fin k) => 0).det

The bialternant Jacobi–Trudi identity: a_{v+δ} = s_v · a_δ over the polynomial ring.