comap_comp — Mathlib

English

For algebra homomorphisms f,g, comap (g ∘ f) equals comap f composed with comap g.

Русский

Для алгебраических отображений f,g: comap (g ∘ f) = comap f ∘ comap g.

LaTeX

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

Lean4

theorem comap_comp (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R) :
    comap (g.comp f) = comap f ∘ comap g := by
  funext x
  exact comap_comp_apply _ _ _

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