English
Let I be an ideal in a commutative ring R and M ∈ M_n(R) be an n×n matrix with every entry M_ij ∈ I. Then for every natural number k, the k-th coefficient of the characteristic polynomial of M lies in the (Fintype.card n − k)-th power of I, i.e. coeff_k(charpoly(M)) ∈ I^{|n| − k}. In particular, higher coefficients are controlled by the entries lying in I.
Русский
Пусть I — идеал в коммутативной кольце R, и M ∈ M_n(R) — матрица размерности n×n, все элементы которой принадлежат I. Тогда для любого натурального k коэффициент k-ого члена характеристического многочлена M лежит в I^{|n| − k}. То есть coeff_k(charpoly(M)) ∈ I^{card(n) − k}. В частности, старшие коэффициенты зависят от элементов, лежащих в I.
LaTeX
$$$\\Big(\\forall i,j,\\ M_{ij} \\in I\\Big) \\Rightarrow \\forall k \\in \\mathbb{N},\\ M.\\mathrm{charpoly}.\\mathrm{coeff}\\\\ k \\in I^{|n| - k}$$$
Lean4
theorem coeff_charpoly_mem_ideal_pow {I : Ideal R} (h : ∀ i j, M i j ∈ I) (k : ℕ) :
M.charpoly.coeff k ∈ I ^ (Fintype.card n - k) :=
by
delta charpoly
rw [Matrix.det_apply, finset_sum_coeff]
apply sum_mem
rintro c -
rw [coeff_smul, Submodule.smul_mem_iff']
have : ∑ x : n, 1 = Fintype.card n := by rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
rw [← this]
apply coeff_prod_mem_ideal_pow_tsub
rintro i - (_ | k)
· rw [tsub_zero, pow_one, charmatrix_apply, coeff_sub, ← smul_one_eq_diagonal, smul_apply, smul_eq_mul,
coeff_X_mul_zero, coeff_C_zero, zero_sub, neg_mem_iff]
exact h (c i) i
· rw [add_comm, tsub_self_add, pow_zero, Ideal.one_eq_top]
exact Submodule.mem_top
