Diagonal entries of the resolvent

The diagonal entry ∑ₖ (Mᵏ)ᵢᵢ Xᵏ of the resolvent series of M is, by Cramer's rule, the ratio of the reversed characteristic polynomial of M with row and column i deleted to that of M: (∑ₖ (Mᵏ)ᵢᵢ Xᵏ) · charpolyRev M = charpolyRev (M∖i) in R⟦X⟧.

Main results

• Matrix.one_sub_X_smul_submatrix_ne: deleting row and column i commutes with 1 - X • M.
• Matrix.resolventSeries_diag_mul_det, Matrix.resolventSeries_diag_mul_coe_charpolyRev: the identity above, with det (1 - X • M) and with charpolyRev.
• Matrix.coe_charpolyRev_eq_det: the coercion of charpolyRev M to R⟦X⟧ is det (1 - X • M) computed in R⟦X⟧.

theorem Matrix.one_sub_X_smul_submatrix_ne {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (M : Matrix n n R) (i : n) : (1 - PowerSeries.X • M.map ⇑PowerSeries.C).submatrix Subtype.val Subtype.val = 1 - PowerSeries.X • (M.submatrix Subtype.val Subtype.val).map ⇑PowerSeries.C

Deleting row/column i of 1 - X·M gives 1 - X·(M∖i). The construction commutes with the principal {j ≠ i} submatrix (1, the X• scalar, and map C all restrict entrywise; 1 restricts to 1 because Subtype.val is injective).

theorem Matrix.resolventSeries_diag_mul_det {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (M : Matrix n n R) (i : n) : M.resolventSeries i i * (1 - PowerSeries.X • M.map ⇑PowerSeries.C).det = ((1 - PowerSeries.X • M.map ⇑PowerSeries.C).submatrix Subtype.val Subtype.val).det

Diagonal resolvent as a determinant ratio (cleared denominators), Lemma 3. For any matrix M over a commutative ring and index i, the generating function of the diagonal matrix powers times det(1 - X·M) equals the determinant of the i-deleted block:

(Σ_k (Mᵏ)_{ii} Xᵏ) · det(1 - X·M) = det((1 - X·M)∖i).

1 - X·M is invertible over R⟦X⟧ (det has constant term det 1 = 1, a unit — extracted from the Neumann identity (1-X·M)·resolventSeries = 1); Cramer turns the diagonal of its inverse into Ring.inverse(det)·adjugate, the determinant cancels the inverse, and adjugate B i i = det(B∖i) (adjugate_apply_self_eq_det_submatrix).

Bridge to charpolyRev

det(1 - X·M) over R⟦X⟧ is the image of the reversed characteristic polynomial charpolyRev M (a R[X] object) under the canonical coercion R[X] → R⟦X⟧. This connects the resolvent determinants above to the polynomial world where Godsil's matching/charpoly identities live.

theorem Matrix.coe_charpolyRev_eq_det {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (M : Matrix n n R) : ↑M.charpolyRev = (1 - PowerSeries.X • M.map ⇑PowerSeries.C).det

det(1 - X·M) over R⟦X⟧ is the coercion of charpolyRev M. The canonical ring homomorphism R[X] → R⟦X⟧ commutes with det (RingHom.map_det) and sends X ↦ X, C a ↦ C a (Polynomial.coe_X, Polynomial.coe_C), turning Mathlib's charpolyRev M = det(1 - X·M.map C) in R[X] into the same determinant in R⟦X⟧.

theorem Matrix.resolventSeries_diag_mul_coe_charpolyRev {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (M : Matrix n n R) (i : n) : M.resolventSeries i i * ↑M.charpolyRev = ↑(M.submatrix Subtype.val Subtype.val).charpolyRev

Diagonal resolvent as a charpolyRev ratio (cleared denominators), Lemma 3 + bridge. (Σ_k (Mᵏ)_{ii} Xᵏ) · ↑charpolyRev(M) = ↑charpolyRev(M∖i): combine resolventSeries_diag_mul_det with coe_charpolyRev_eq_det on both determinants (one_sub_X_smul_submatrix_ne identifies the deleted block as 1 - X·(M∖i)). The matching-polynomial form of Godsil's resolvent step.