feat(linear_algebra/matrix/charpoly): Coefficients of the characteris…

…tic polynomial falls in the ideal power. (#15459)




Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/algebra/order/sub.lean

@@ -238,6 +238,15 @@ by { rw [add_comm], apply tsub_add_eq_tsub_tsub }
 lemma tsub_right_comm : a - b - c = a - c - b :=
 by simp_rw [← tsub_add_eq_tsub_tsub, add_comm]
 
+lemma add_tsub_add_le_tsub_add_tsub :
+  (a + b) - (c + d) ≤ (a - c) + (b - d) :=
+begin
+  rw [add_comm c, ← tsub_tsub],
+  refine (tsub_le_tsub_right add_tsub_le_assoc c).trans _,
+  rw [add_comm a, add_comm (a - c)],
+  exact add_tsub_le_assoc
+end
+
 end cov
 
 /-! ### Lemmas that assume that an element is `add_le_cancellable`. -/

src/linear_algebra/matrix/charpoly/basic.lean

@@ -46,6 +46,9 @@ The determinant of this matrix is the characteristic polynomial.
 def charmatrix (M : matrix n n R) : matrix n n R[X] :=
 matrix.scalar n (X : R[X]) - (C : R →+* R[X]).map_matrix M
 
+lemma charmatrix_apply (M : matrix n n R) (i j : n) :
+  charmatrix M i j = X * (1 : matrix n n R[X]) i j - C (M i j) := rfl
+
 @[simp] lemma charmatrix_apply_eq (M : matrix n n R) (i : n) :
   charmatrix M i i = (X : R[X]) - C (M i i) :=
 by simp only [charmatrix, sub_left_inj, pi.sub_apply, scalar_apply_eq,

src/linear_algebra/matrix/charpoly/coeff.lean

@@ -190,3 +190,26 @@ lemma pow_eq_aeval_mod_charpoly (M : matrix n n R) (k : ℕ) : M^k = aeval M (X^
 by rw [←aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
 
 end matrix
+
+section ideal
+
+lemma 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) :=
+begin
+  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, coeff_X_mul_zero, coeff_C_zero, zero_sub,
+      neg_mem_iff],
+    exact h (c i) i },
+  { rw [nat.succ_eq_one_add, tsub_self_add, pow_zero, ideal.one_eq_top],
+    exact submodule.mem_top }
+end
+
+end ideal

src/ring_theory/polynomial/basic.lean

@@ -519,6 +519,28 @@ begin
     I.leading_coeff_nth_mono (nat.le_add_left _ _)⟩
 end
 
+/--
+If `I` is an ideal, and `pᵢ` is a finite family of polynomials each satisfying
+`∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ` for some `nᵢ`, then `p = ∏ pᵢ` also satisfies `∀ k, pₖ ∈ Iⁿ⁻ᵏ` with `n = ∑ nᵢ`.
+-/
+lemma _root_.polynomial.coeff_prod_mem_ideal_pow_tsub {ι : Type*} (s : finset ι) (f : ι → R[X])
+  (I : ideal R) (n : ι → ℕ) (h : ∀ (i ∈ s) k, (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ) :
+  (s.prod f).coeff k ∈ I ^ (s.sum n - k) :=
+begin
+  classical,
+  induction s using finset.induction with a s ha hs generalizing k,
+  { rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, ideal.one_eq_top],
+    exact submodule.mem_top },
+  { rw [sum_insert ha, prod_insert ha, coeff_mul],
+    apply sum_mem,
+    rintro ⟨i, j⟩ e,
+    obtain rfl : i + j = k := nat.mem_antidiagonal.mp e,
+    apply ideal.pow_le_pow add_tsub_add_le_tsub_add_tsub,
+    rw pow_add,
+    exact ideal.mul_mem_mul (h _ (finset.mem_insert.mpr $ or.inl rfl) _)
+      (hs (λ i hi k, h _ (finset.mem_insert.mpr $ or.inr hi) _) j) }
+end
+
 end comm_semiring
 
 section ring