English
For finite indices m,n and a ring hom f: S →+* Matrix(n,n,R), the determinant of the scalar det(M) mapped via f equals the determinant of the block-composed matrix (M.map f).
Русский
Пусть M — матрица над S, размер m×m, и f: S →+* Matrix(n,n,R). Детерминант скалярного det(M), отображенный через f, равен детерминанту блочно-сконструированной матрицы (M.map f).
LaTeX
$$$\\det\\bigl( f(\\det M) \\bigr) = \\det\\bigl((M.map f).\\text{comp} \\; m\\; m\\; n\\; n\\; R\\bigr).$$$
Lean4
/-- The main result in Silvester's paper *Determinants of Block Matrices*: the determinant of
a block matrix with commuting, equal-sized, square blocks can be computed by taking determinants
twice in a row: first take the determinant over the commutative ring generated by the
blocks (`S` here), then take the determinant over the base ring. -/
theorem det_det [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : (f M.det).det = ((M.map f).comp m m n n R).det := by
induction l : Fintype.card m generalizing R S m with
| zero =>
rw [Fintype.card_eq_zero_iff] at l
simp_rw [Matrix.det_isEmpty, map_one, det_one]
| succ l ih =>
have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)
let f' := f.polyToMatrix
let M' := cornerAddX M k
have : (f' M'.det).det = ((M'.map f').comp m m n n R[X]).det :=
by
refine
sub_eq_zero.mp <|
mem_nonZeroDivisors_iff_right.mp (pow_mem ?_ _) _
(det_det_aux k fun M ↦ ih _ _ <| by grind [Fintype.card_subtype_compl, Fintype.card_unique])
rw [polyToMatrix_cornerAddX, ← charpoly]
exact (Matrix.charpoly_monic _).mem_nonZeroDivisors
rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]
