English
If Fintype.card n ≤ Fintype.card m, then (A B).charpoly = X^{m-n}*(B A).charpoly up to isomorphism of HMul.
Русский
Если card(n) ≤ card(m), то χ_{A B} = X^{m-n} χ_{BA} (с точной неопределённостью по HMul).
LaTeX
$$$(A B).charpoly = X^{(Fintype.card m - Fintype.card n)} \cdot (B A).charpoly$$$
Lean4
/-- A version of `Matrix.charpoly_mul_comm` for rectangular matrices.
See also `Matrix.charpoly_mul_comm_of_le` which has just `(A * B).charpoly` as the LHS.
-/
theorem charpoly_mul_comm' (A : Matrix m n R) (B : Matrix n m R) :
X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly := by
-- This proof follows https://math.stackexchange.com/a/311362/315369
let M := fromBlocks (scalar m X) (A.map C) (B.map C) (1 : Matrix n n R[X])
let N := fromBlocks (-1 : Matrix m m R[X]) 0 (B.map C) (-scalar n X)
have hMN : M * N = fromBlocks (-scalar m X + (A * B).map C) (-(X : R[X]) • A.map C) 0 (-scalar n X) := by
simp [M, N, fromBlocks_multiply, smul_eq_mul_diagonal, -diagonal_neg]
have hNM : N * M = fromBlocks (-scalar m X) (-A.map C) 0 ((B * A).map C - scalar n X) := by
simp [M, N, fromBlocks_multiply, sub_eq_add_neg, -scalar_apply, scalar_comm, Commute.all]
have hdet_MN :
(M * N).det =
(-1 : R[X]) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * (scalar m X - (A * B).map C).det) :=
by
rw [hMN, det_fromBlocks_zero₂₁, neg_add_eq_sub, ← neg_sub, det_neg]
simp
ring
have hdet_NM :
(N * M).det =
(-1 : R[X]) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * (scalar n X - (B * A).map C).det) :=
by
rw [hNM, det_fromBlocks_zero₂₁, ← neg_sub, det_neg (_ - _)]
simp
ring
dsimp only [charpoly, charmatrix, RingHom.mapMatrix_apply]
rw [← (isUnit_neg_one.pow _).isRegular.left.eq_iff, ← hdet_NM, ← hdet_MN, det_mul_comm]
