comap_apply — Mathlib

English

Applying comap to the identity algebra hom yields the identity function on evaluations: comap id x = x.

Русский

Применение перехода по тождественному алгохомомоду даёт тождественную отображение: comap id x = x.

LaTeX

$$$\\operatorname{comap}(\\mathrm{AlgHom.id\\,R\\, (MvPolynomial\\, σ\\, R)})\\,x = x$$$

Lean4

@[simp]
theorem comap_apply (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (x : τ → R) (i : σ) :
    comap f x i = aeval x (f (X i)) :=
  rfl

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