toExtensionHom_toAlgHom_apply — Mathlib

English

Evaluating the extension-hom-applied map on an element x agrees with first applying the original map and then embedding into the extension.

Русский

Проведение элемента x через расширение-гомоморфизма даёт то же самое, что если сначала применить исходное отображение, а затем вложить в расширение.

LaTeX

$$$(f^{\\mathrm{ext}})^{\\!} (x) = f(x)$$$

Lean4

theorem toExtensionHom_toAlgHom_apply [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') (x) :
    f.toExtensionHom.toAlgHom x = f.toAlgHom x :=
  rfl

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