English
Let M be an m×m matrix over a commutative ring S, and k an index in m. Let f be a ring homomorphism from S to the m×m matrix ring over a commutative ring R, and consider corner augmentation cornerAddX(M,k). Then the determinant of the polynomial-matrix obtained by mapping cornerAddX(M,k) via f.polyToMatrix, evaluated at X = 0, equals the determinant of M after applying f.
Русский
Пусть M — матрица размера m×m над когерентной кольцом S, а k — индекс в {1,...,m}. Пусть f — кольцевой однородный гомоморфизм S →+* Mat_n(R). Тогда детерминантно-многочленный матричный объект, полученный из cornerAddX(M,k) через отображение f.polyToMatrix и затем взятие det, при подстановке X = 0 совпадает с det(M.map f).
LaTeX
$$$\\operatorname{ev}_0\\Bigl(\\det\\bigl(\\bigl(\\text{cornerAddX } M\\, k\\bigr) .map f.{\\text{polyToMatrix}}\\bigr)\\Bigr) = \\det\\bigl( M.map f \\bigr).$$$
Lean4
theorem eval_zero_comp_det :
eval 0 (comp m m n n R[X] <| (cornerAddX M k).map f.polyToMatrix).det = (comp m m n n R <| M.map f).det :=
by
simp_rw [← coe_evalRingHom, RingHom.map_det, ← compRingEquiv_apply, ← RingEquiv.coe_toRingHom, ←
RingHom.mapMatrix_apply, ← RingHom.comp_apply, ← RingHom.comp_assoc, evalRingHom_mapMatrix_comp_compRingEquiv,
RingHom.comp_assoc, RingHom.mapMatrix_comp, evalRingHom_mapMatrix_comp_polyToMatrix, ← RingHom.mapMatrix_comp,
RingHom.comp_apply]
congr with i j
simp [cornerAddX, diagonal, apply_ite]
