mapAlgHom_comp — Mathlib

English

Let C be a Type with a semiring structure and an R-algebra structure. For f: B →ₐ[R] C and g: A →ₐ[R] B, the polynomial map composed via f and g equals the polynomial map of the composition: (mapAlgHom f) ∘ (mapAlgHom g) = mapAlgHom (f ∘ g).

Русский

Пусть C — полугруппа полиномов над R; для гомоморфизмов f: B →ₐ[R] C и g: A →ₐ[R] B выполняется: (mapAlgHom f) ∘ (mapAlgHom g) = mapAlgHom (f ∘ g).

LaTeX

$$$(\\operatorname{mapAlgHom} f) \\circ (\\operatorname{mapAlgHom} g) = \\operatorname{mapAlgHom}(f \\circ g)$$$

Lean4

@[simp]
theorem mapAlgHom_comp (C : Type*) [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) :
    (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g) := by ext <;> simp

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