English
If A1 ≃ₐ[R] A1' and A2 ≃ₐ[R] A2', then the map between homomorphism spaces A1 →ₐ[R] A2 and A1' →ₐ[R] A2' is an equivalence given by pre/post composition with the given equivalences.
Русский
Если A1 ≃ₐ A1' и A2 ≃ₐ A2', то отображение между пространствами алгебраических гомоморфизмов является эквивалентностью, задаваемой композициями с данными эквивалентностями.
LaTeX
$$$\arrowCongr(e_1,e_2): (A_1 \toₐ[R] A_2) \simeq (A_1' \toₐ[R] A_2')$ with $f \mapsto e_2 \circ f \circ e_1^{-1}$$$
Lean4
/-- Algebra equivalences are transitive. -/
@[trans]
def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃ :=
{ e₁.toRingEquiv.trans e₂.toRingEquiv with
commutes' := fun r => show e₂.toFun (e₁.toFun _) = _ by rw [e₁.commutes', e₂.commutes'] }
