map_algebraMap — Mathlib

English

For a S-algebra homomorphism f: A →ₐ[S] B, it respects the base R-algebra structure: f(algebraMap_R_A(r)) = algebraMap_R_B(r) for all r ∈ R.

Русский

Для алгомоморфизма f: A →ₐ[S] B он сохраняет базовую структуру R: f(algebraMap_R_A(r)) = algebraMap_R_B(r) для всех r ∈ R.

LaTeX

$$$ f\bigl( algebraMap_R A\ r\bigr) = algebraMap_R B\ r$$

Lean4

@[simp]
theorem _root_.AlgHom.map_algebraMap (f : A →ₐ[S] B) (r : R) : f (algebraMap R A r) = algebraMap R B r := by
  rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]

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