algHom_eval₂_algebraMap — Mathlib

English

For any α, membership in the range of algebraMap corresponds to existential equality via some witness.

Русский

Для любого элемента принадлежность диапазону algebraMap эквивалентна существованию свидетеля, подводящему равенство.

LaTeX

$$$x \in \mathrm{Range}(\mathrm{algebraMap}\; R\; A)$ эквивалентно $\exists y, \mathrm{algebraMap}\; R\; A\; y = x$$$

Lean4

@[simp]
theorem algHom_eval₂_algebraMap {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    (p : R[X]) (f : A →ₐ[R] B) (a : A) : f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p :=
  by
  simp only [eval₂_eq_sum, sum_def]
  simp only [map_sum, map_mul, map_pow, AlgHom.commutes]

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