Matrices of formal power series

Let A be a square matrix over a nontrivial ring R, indexed by a finite type ι, and let M = (1 + X²) I - X A in the ring of matrices of formal power series over R. This file proves that M has no right inverse whose entries are polynomials unless ι is empty (Matrix.isEmpty_of_one_add_X_sq_smul_sub_X_smul_mul_eq_one). Indeed the coefficient matrices of a right inverse N satisfy N_{n+2} = A N_{n+1} - N_n, so if they vanish from some degree on, then they vanish in every degree by descending induction, against N_0 = I.

Main results

• Matrix.isEmpty_of_one_add_X_sq_smul_sub_X_smul_mul_eq_one: no polynomial matrix is a right inverse of (1 + X²) I - X A over a nonempty index type.

References

• P. Etingof and C.-H. Eu, Koszulity and the Hilbert series of preprojective algebras, Math. Res. Lett. 14 (2007), Section 3, where (1 + X²) I - X A is the Hilbert-series denominator of a preprojective algebra.

theorem Matrix.isEmpty_of_one_add_X_sq_smul_sub_X_smul_mul_eq_one {R : Type u_1} {ι : Type u_2} [Ring R] [Nontrivial R] [Fintype ι] [DecidableEq ι] (A : Matrix ι ι R) {N : Matrix ι ι (PowerSeries R)} (hN : ((1 + PowerSeries.X ^ 2) • 1 - PowerSeries.X • A.map ⇑PowerSeries.C) * N = 1) {d : ℕ} (hd : ∀ (n : ℕ), d ≤ n → ∀ (i j : ι), (PowerSeries.coeff n) (N i j) = 0) : IsEmpty ι

No polynomial matrix is a right inverse of (1 + X²) I - X A over a nonempty index type. If ((1 + X²) I - X A) N = I for a matrix A over a nontrivial ring R, and the coefficients of every entry of N vanish from degree d on, then the index type is empty.