English
If e: A1 ≃ₐ[R] A2 and e': A1' ≃ₐ[R] A2' are algebra isomorphisms, then there is an equivalence between the space of maps A1 ≃ₐ[R] A1' and the space A2 ≃ₐ[R] A2' given by ψ ↦ e.symm.trans (ψ.trans e'), with inverse ψ' ↦ e.trans (ψ'.trans e'.symm).
Русский
Если e: A1 ≃ₐ[R] A2 и e': A1' ≃ₐ[R] A2' тождественные изоморфизмы, то существует эквивалентность между пространствами отображений A1 ≃ₐ[R] A1' и A2 ≃ₐ[R] A2', задаваемая ψ ↦ e.symm.trans (ψ.trans e'), и обратная ей.
LaTeX
$$$\\text{equivCongr}: (A_1 \\simeq_{R}^{\\mathrm{alg}} A_1') \\;\\Rightarrow\\; (A_2 \\simeq_{R}^{\\mathrm{alg}} A_2') \\,:\\\\\langle\\;\\text{toFun }\\psi = e^{-1} \\circ (\\psi \\circ e'),\\;\\; \\text{invFun }\\psi = e \\circ (\\psi \\circ e'^{-1}) \\rangle$$$
Lean4
@[simp]
theorem arrowCongr_symm (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
(arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm :=
rfl
