English
There is a canonical equivalence between ring homomorphisms R → S and ℚ-algebra homomorphisms R →ₐ[ℚ] S, given by f ↦ f.toRatAlgHom and its inverse by forgetting the ℚ-structure.
Русский
Существует каноническое эквивалентство между гомоморфизмами колец R → S и ℚ-алгебра-гомоморфизмами R →ₐ[ℚ] S, которое задаётся переходами f ↦ f.toRatAlgHom и обратным переходом.
LaTeX
$$$(R \\to+* S) \\simeq (R \\to_{\\mathbb{Q}} S)$$$
Lean4
/-- The equivalence between `RingHom` and `ℚ`-algebra homomorphisms. -/
@[simps]
def equivRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] : (R →+* S) ≃ (R →ₐ[ℚ] S)
where
toFun := RingHom.toRatAlgHom
invFun := AlgHom.toRingHom
left_inv f := RingHom.toRatAlgHom_toRingHom f
right_inv f := AlgHom.toRingHom_toRatAlgHom f
