comap_eq_id_of_eq_id — Mathlib

English

If an algebra homomorphism f acts as the identity on all polynomials, then comap f x equals x for all x.

Русский

Если алгебраический гомоморфизм f действует как тождественный на всех полиномах, тогда comap f x = x для всех x.

LaTeX

$$$\\forall x, \\operatorname{comap}(f)\\, x = x$ при hf, где hf(φ) = φ$$

Lean4

theorem comap_eq_id_of_eq_id (f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (hf : ∀ φ, f φ = φ) (x : σ → R) :
    comap f x = x := by
  convert comap_id_apply x
  ext1 φ
  simp [hf, AlgHom.id_apply]

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