map_map — Mathlib

English

For ring hom f and g, map g (map f p) = map (g ∘ f) p; the functoriality of map.

Русский

Для гомоморфизмов f, g верно map g (map f p) = map (g ∘ f) p; отображение слева направо компонуется.

LaTeX

$$$$\operatorname{map} g\bigl(\operatorname{map} f\;p\bigr) = \operatorname{map} (g\circ f)\;p.$$$$

Lean4

theorem map_map [CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) : map g (map f p) = map (g.comp f) p :=
  (eval₂_comp_left (map g) (C.comp f) X p).trans <| by
    congr
    · ext1 a
      simp only [map_C, comp_apply, RingHom.coe_comp]
    · ext1 n
      simp only [map_X, comp_apply]

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