evalRingHom_mapMatrix_comp_compRingEquiv

English

A compatibility identity: composing evalRingHom 0 with compRingEquiv gives the same as composing the corresponding ring homs with mapMatrix.mapMatrix.

Русский

Совместимость: композиция evalRingHom 0 с compRingEquiv равна композиции соответствующих гомоморфизмов с mapMatrix.mapMatrix.

LaTeX

$$$(\\mathrm{evalRingHom}\\;0).\\mathrm{mapMatrix} \\circ \\mathrm{compRingEquiv}_{m\\;n\\;R[X]} = (\\mathrm{compRingEquiv}_{m\\;n\\;R})^\\mathrm{toRingHom} \\circ (\\mathrm{evalRingHom}\\;0).\\mathrm{mapMatrix}.mapMatrix$$$

Lean4

theorem evalRingHom_mapMatrix_comp_compRingEquiv {m} [Fintype m] [DecidableEq m] :
    (evalRingHom 0).mapMatrix.comp (compRingEquiv m n R[X]) =
      (compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix :=
  by ext; simp

Похожие утверждения