17.1. Algebras🔗

Mathlib represents inclusions of rings uniformly using the class Algebra. Specifically, [Algebra R S] supplies a canonical homomorphism from R to S: algebraMap R S. The idea then is that we set up the instances so that an extension of rings S / R becomes represented by the inclusion map algebraMap R S. Mathlib provides many of these inclusion maps already

Algebra instances in Mathlib include:

algebraMap ℕ R : ℕ →+* R#check algebraMap ℕ R -- n ↦ 1 + ... + 1, `n` times
algebraMap ℤ R : ℤ →+* R#check algebraMap ℤ R -- ± n ↦ ± (1 + ... + 1), `n` times
variable [CharZero K] in
algebraMap ℚ K : ℚ →+* K#check algebraMap ℚ K -- ± n ↦ ± (1 + ... + 1), `n` times

algebraMap R R : R →+* R#check algebraMap R R -- x ↦ x

algebraMap R (Polynomial R) : R →+* Polynomial R#check algebraMap R (Polynomial R) -- x ↦ C x

variable (s : Subring R) in
algebraMap (↥s) R : ↥s →+* R#check algebraMap s R -- ⟨x, hx⟩ ↦ x

variable (s : Submonoid R) in
algebraMap R (Localization s) : R →+* Localization s#check algebraMap R (Localization s) -- x ↦ x/1

17.1.1. Injectivity🔗

An algebraMap is not necessarily injective: it can be any ring homomorphism in principle. For ring extensions, you might need to add an extra hypothesis saying Function.Injective (algebraMap R S). Many of the theorems on ring extensions do not need these hypotheses, however, and in many other cases algebraMap R S is already true: for example when R is a division ring (see RingHom.injective) or R is the natural numbers or the integers and S has characteristic 0.