English
Let e: A1 ≃ₐ[R] A2. For y ∈ R and x ∈ A1, we have algebraMap_R,A2(y) = e(x) if and only if algebraMap_R,A1(y) = x. This characterizes how e intertwines the base algebra maps.
Русский
Пусть e: A1 ≃ₐ[R] A2. Для y∈R и x∈A1 верно, что algebraMap_R,A2(y) = e(x) тогда и только тогда, когда algebraMap_R,A1(y) = x. Описывает, как e сохраняет базовые отображения алгебры.
LaTeX
$$$ \\forall y\\in R, \\; \\forall x\\in A_1:\\ algebraMap R A_2\, y = e(x) \\iff algebraMap R A_1\, y = x.$$$
Lean4
@[simp]
theorem algebraMap_eq_apply (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} : algebraMap R A₂ y = e x ↔ algebraMap R A₁ y = x :=
⟨fun h => by simpa using e.symm.toAlgHom.algebraMap_eq_apply h, fun h => e.toAlgHom.algebraMap_eq_apply h⟩
