First-order expansion of the determinant

TheoremThe determinant is affine along a rank-one direction#✓fully proved

Let \(K\) be a field, let \(B\) be a square matrix over \(K\) indexed by a finite type \(n\), and let \(u, v \in K^n\). Then for every \(t \in K\), \(\det(B + t\,uv^{\mathsf T}) = \det B + t\,(\det(B + uv^{\mathsf T}) - \det B)\).

public theorem det_add_smul_vecMulVec {n K : Type*} [Fintype n] [DecidableEq n] [Field K]
    (B : Matrix n n K) (u v : n → K) (t : K) :
    det (B + t • vecMulVec u v) =
      det B + t * (det (B + vecMulVec u v) - det B)

Used by 1

Used byRank-one coefficients make the mixed determinant polynomial affine

DefinitionFirst-order term of the determinant#✓fully proved

Let \(R\) be a commutative ring and let \(A\) and \(B\) be square matrices over \(R\) indexed by a finite type \(n\). The first-order term of the determinant of \(B\) in the direction \(A\) is \(L_B(A) = \sum_{i \in n} \det B^{(i)}\), where \(B^{(i)}\) is the matrix \(B\) with its \(i\)-th row replaced by the \(i\)-th row of \(A\).

It is the coefficient of \(X\) in the polynomial \(\det(B + XA)\).

public noncomputable def detLinear {n R : Type*}
    [Fintype n] [DecidableEq n] [CommRing R] (B A : Matrix n n R) : R :=
  ∑ i, det (updateRow B i (fun j ↦ A i j))

Used by 5

Used byMarcus--Spielman--Srivastava barrier bound · The mixed characteristic polynomial is affine in each matrix · The coefficient of \(X\) in \(\det(B + XA)\) · Additivity of the first-order term of the determinant · Homogeneity of the first-order term of the determinant

TheoremThe coefficient of \(X\) in \(\det(B + XA)\)#✓fully proved

Let \(R\) be a commutative ring and let \(A\) and \(B\) be square matrices over \(R\) indexed by a finite type \(n\). Regard \(B + XA\) as a matrix over the polynomial ring \(R[X]\). Then the coefficient of \(X\) in the polynomial \(\det(B + XA)\) equals the first-order term of the determinant \(L_B(A) = \sum_{i \in n} \det B^{(i)}\), where \(B^{(i)}\) is the matrix \(B\) with its \(i\)-th row replaced by the \(i\)-th row of \(A\).

public theorem coeff_one_det_add_X_smul {n R : Type*}
    [Fintype n] [DecidableEq n] [CommRing R] (B A : Matrix n n R) :
    (det (B.map Polynomial.C + (Polynomial.X : R[X]) • A.map Polynomial.C)).coeff 1 =
      detLinear B A

Uses 1 · Used by 2

Statement usesFirst-order term of the determinant

Used byMarcus--Spielman--Srivastava barrier bound · The mixed characteristic polynomial is affine in each matrix

TheoremAdditivity of the first-order term of the determinant#✓fully proved

Let \(R\) be a commutative ring and let \(A\), \(B\), \(C\) be square matrices over \(R\) indexed by a finite type \(n\). Write \(L_B(A) = \sum_{i \in n} \det B^{(i)}_A\), where \(B^{(i)}_A\) is the matrix \(B\) with its \(i\)-th row replaced by the \(i\)-th row of \(A\). Then \(L_B(A + C) = L_B(A) + L_B(C)\).

public theorem detLinear_add {n R : Type*} [Fintype n] [DecidableEq n] [CommRing R]
    (B A C : Matrix n n R) :
    detLinear B (A + C) = detLinear B A + detLinear B C

Uses 1 · Used by 1

Statement usesFirst-order term of the determinant

Used byThe mixed characteristic polynomial is affine in each matrix

TheoremHomogeneity of the first-order term of the determinant#✓fully proved

Let \(R\) be a commutative ring, let \(a \in R\), and let \(A\) and \(B\) be square matrices over \(R\) indexed by a finite type \(n\). Write \(L_B(A) = \sum_{i \in n} \det B^{(i)}_A\), where \(B^{(i)}_A\) is the matrix \(B\) with its \(i\)-th row replaced by the \(i\)-th row of \(A\). Then \(L_B(aA) = a \, L_B(A)\).

public theorem detLinear_smul {n R : Type*} [Fintype n] [DecidableEq n] [CommRing R]
    (B A : Matrix n n R) (a : R) :
    detLinear B (a • A) = a * detLinear B A

Uses 1 · Used by 1

Statement usesFirst-order term of the determinant

Used byThe mixed characteristic polynomial is affine in each matrix

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.