Homomorphisms of ℚ-algebras

def RingHom.toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : R →ₐ[ℚ] S

Reinterpret a RingHom as a ℚ-algebra homomorphism. This actually yields an equivalence, see RingHom.equivRatAlgHom.

Equations

• f.toRatAlgHom = { toRingHom := f, commutes' := ⋯ }

@[simp]

theorem RingHom.toRatAlgHom_toRingHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : ↑f.toRatAlgHom = f

@[simp]

theorem AlgHom.toRingHom_toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →ₐ[ℚ] S) : (↑f).toRatAlgHom = f

def RingHom.equivRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] : (R →+* S) ≃ (R →ₐ[ℚ] S)

The equivalence between RingHom and ℚ-algebra homomorphisms.

Equations

• RingHom.equivRatAlgHom = { toFun := RingHom.toRatAlgHom, invFun := AlgHom.toRingHom, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RingHom.equivRatAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : RingHom.equivRatAlgHom f = f.toRatAlgHom

@[simp]

theorem RingHom.equivRatAlgHom_symm_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (self : R →ₐ[ℚ] S) : RingHom.equivRatAlgHom.symm self = self.toRingHom