Rational algebras from ring homomorphisms

The image of a ring homomorphism ℚ →+* B is central, because every rational number is a quotient of integers and integer casts commute with everything. Hence such a homomorphism makes B a ℚ-algebra, even when B is not commutative. This is used, for instance, to view the target of a ring homomorphism out of a ℚ-algebra as a ℚ-algebra.

Main declarations

• RingHom.commute_apply_rat: the image of a rational number commutes with every element.
• RingHom.toRatAlgebra: the ℚ-algebra structure induced by a ring homomorphism ℚ →+* B.
• RingHom.algebraMap_toRatAlgebra: its algebra map is the given homomorphism.

theorem RingHom.commute_apply_rat {B : Type u_1} [Ring B] (g : ℚ →+* B) (q : ℚ) (y : B) : Commute (g q) y

The image of a rational number under a ring homomorphism is central.

@[reducible, inline]

abbrev RingHom.toRatAlgebra {B : Type u_1} [Ring B] (g : ℚ →+* B) : Algebra ℚ B

A ring homomorphism ℚ →+* B makes B a ℚ-algebra, since its image is central. See note [reducible non-instances].

theorem RingHom.algebraMap_toRatAlgebra {B : Type u_1} [Ring B] (g : ℚ →+* B) : algebraMap ℚ B = g

The algebra map of RingHom.toRatAlgebra g is g.