comap_id_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem comap_id_apply (x : σ → R) : comap (AlgHom.id R (MvPolynomial σ R)) x = x :=
  by
  funext i
  simp only [comap, AlgHom.id_apply, aeval_X]

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