English
An algebra equivalence e: A1 ≃ₐ[R] A2 can be viewed as an R-algebra homomorphism A1 → A2, and this is symmetric with the other projections to homs.
Русский
Эквивалентность A1 ≃ₐ[R] A2 может рассматриваться как гомоморфизм R-алгебр A1 → A2; это соответствует симметрии с другими проекциям на гомоморфизмы.
LaTeX
$$$ e : A_1 \simeq_{R} A_2 \quad\Rightarrow\quad e \mapsto e \,\text{as} \,-\! A_1 \to A_2 \text{ is a hom.}$$$
Lean4
/-- Interpret an algebra equivalence as an algebra homomorphism.
This definition is included for symmetry with the other `to*Hom` projections.
The `simp` normal form is to use the coercion of the `AlgHomClass.coeTC` instance. -/
@[coe]
def toAlgHom : A₁ →ₐ[R] A₂ :=
{ e with
map_one' := map_one e
map_zero' := map_zero e }
