English
If A1 ≃ₐ[R] A1′ and A2 ≃ₐ[R] A2′ are algebra isomorphisms, then there is a natural equivalence between the algebra homomorphism spaces: (A1 →ₐ[R] A2) ≃ (A1′ →ₐ[R] A2′).
Русский
Если A1 ≃ₐ[R] A1′ и A2 ≃ₐ[R] A2′ — это алгебраические эквивалентности, существует естественное эквивалентное соответствие между множествами гомоморфизмов алгебр: (A1 →ₐ[R] A2) ≃ (A1′ →ₐ[R] A2′).
LaTeX
$$$ (A_1 \\to_{R} A_2) \\simeq (A_1' \\to_{R} A_2') $$$
Lean4
/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'`, then the type of maps
`A₁ →ₐ[R] A₂` is equivalent to the type of maps `A₁' →ₐ[R] A₂'`. -/
@[simps apply]
def arrowCongr (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂')
where
toFun f := (e₂.toAlgHom.comp f).comp e₁.symm.toAlgHom
invFun f := (e₂.symm.toAlgHom.comp f).comp e₁.toAlgHom
left_inv
f := by
simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, symm_comp]
simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]
right_inv
f := by
simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, comp_symm]
simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]
