toAlgHom_comp_apply — Mathlib

English

The toAlgHom of a composed generator equals the algebraMap incarnation of the renamed sum; i.e., (Q.toComp P).toAlgHom = rename Sum.inr.

Русский

toAlgHom композиции генераторов совпадает с переименованием по Sum.inr.

LaTeX

$$$ (Q.toComp P).toAlgHom = \\mathrm{rename}\\,\\mathrm{Sum.inr}$$$

Lean4

@[simp]
theorem toAlgHom_comp_apply [Algebra R R''] [IsScalarTower R R' R''] [IsScalarTower R' R'' S'']
    [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : Hom P P') (g : Hom P' P'') (x) :
    (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x) := by
  induction x using MvPolynomial.induction_on with
  | C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
  | add x y hx hy => simp only [map_add, hx, hy]
  | mul_X p i hp => simp only [map_mul, hp, toAlgHom_X, comp_val]; rfl

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