English
Let M be an m×m matrix over S and k ∈ m. For a ring hom f: S →+* Matrix(n,n,R), the determinants satisfy a multiplicative relation relating det((M.map f).comp) and det of auxiliary block matrices, incorporating powers of det(f(M_{k,k})).
Русский
Пусть M — матрица m×m над S и k ∈ {1,...,m}. При гомоморфизме f: S →+* Matrix(n,n,R) выполняется тождественная связь между детерминантами соответствующих блочно-образованных матриц и детерминантами вспомогательных блочных матриц, включая степени det(f(M_{k,k})).
LaTeX
$$$((M.map\\ f).\\text{comp} \\_ \\_ n n R).\\det \\cdot (f(M_{k k})).\\det^{(\\lvert F\\rvert - 1)} = (f(M_{k k})).\\det \\cdot \\bigl(((\\text{mulAuxMatBlock}).map\\ f).\\text{comp} \\_ \\_ n n R\\bigr).\\det$$$
Lean4
theorem comp_det_mul_pow :
((M.map f).comp m m n n R).det * (f (M k k)).det ^ (Fintype.card m - 1) =
(f (M k k)).det * (((mulAuxMatBlock).map f).comp _ _ n n R).det :=
by
trans (((M * auxMat M k).map f).comp m m n n R).det
· simp_rw [← f.mapMatrix_apply, ← compRingEquiv_apply, map_mul, det_mul, f.mapMatrix_apply, compRingEquiv_apply,
((auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop, comp_toSquareBlock (b := (· ≠ k)),
det_reindex_self, map_toSquareBlock, auxMat_toSquareBlock_eq, auxMat_toSquareBlock_ne, smul_one_eq_diagonal, ←
diagonal_one, diagonal_map (map_zero _), comp_diagonal, det_reindex_self]
simp
· simp_rw [((mul_auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop,
comp_toSquareBlock (b := (· = k)), det_reindex_self, map_toSquareBlock, mul_auxMat_toSquareBlock_eq,
smul_one_eq_diagonal, diagonal_map (map_zero _), comp_diagonal, det_reindex_self]
simp
