Let \((\alpha , +_\alpha , *_\alpha )\) and \((\beta , +_\beta , *_\beta )\) be rings. A ring homomorphism from \(\alpha \) to \(\beta \) is a map \(\mathit {1} : \alpha \to _{+*} \beta \) such that

1. \(\mathit {1}(x +_{\alpha } y) = \mathit {1}(x) +_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
2. \(\mathit {1}(x *_{\alpha } y) = \mathit {1}(x) *_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
3. \(\mathit {1}(1_{\alpha }) = 1_{\beta }\).

Fix the algebraic structures and the homomorphisms under consideration. An Isomorphism \(\phi :A\to B\) is an iso: a homomorphism admitting an inverse homomorphism \(\phi ^{-1}:B\to A\), so that \(\phi ^{-1}\circ \phi =\operatorname {id}_A\) and \(\phi \circ \phi ^{-1}=\operatorname {id}_B\). We write \(A\cong B\) when such an isomorphism exists. This is the invertible-morphism definition of [stacks2017stacks, Definition 4.2.4 and the following paragraph, Tag 0013].

An Endomorphism of \(A\) is a homomorphism \(\phi :A\to A\). The set of all such homomorphisms is denoted \(\operatorname {End}(A)\). Thus an individual endomorphism satisfies \(\phi \in \operatorname {End}(A)\).

An Automorphism of \(A\) is an endomorphism that is an isomorphism. The set of all automorphisms is denoted \(\operatorname {Aut}(A)\). These notations always refer to the chosen kind of homomorphism; for modules over \(R\), the notation \(\operatorname {End}_R(M)\) specifies \(R\)-linear maps.

Let \(R\) be a commutative ring with identity. An algebra \(A\) over \(R\) is an associative ring with identity, equipped with a ring homomorphism \(\mathit {1} : R \to _{+*} A\) and a scalar multiplication \(\bullet : R \to A \to A\), such that for every \(r \in R\) and \(x \in A\), \[ \mathit {1}(r) * x = x * \mathit {1}(r), \qquad r \bullet x = \mathit {1}(r) * x. \] The ring homomorphism preserves the identity; multiplication in \(A\) need not be commutative.

This is the central-map convention of [stacks2017stacks, Section 22.2, Tag 09JF]. It is equivalent to the module formulation in [jadczyk2019notes, Definition 1.6, p. 4]; see the comparison.

Following literatures, for \(r \in R\), usually we write \(\mathit {1}_A(r) : R \to _{+*} A\) as a product \(r \mathit {1}_A\) if not omitted, while they are written as a call to algebraMap _ _ r in \(\textsf {Mathlib}\), which is defined to be Algebra.toRingHom r.

For a commutative ring \(R\), the algebra structure is equivalently an \(R\)-module structure on an associative ring \(A\) with identity, with the same addition, such that \[ r \bullet (x * y) = (r \bullet x) * y = x * (r \bullet y) \qquad (r \in R,\ x,y \in A). \] This is the formulation of [jadczyk2019notes, Definition 1.6, p. 4]. Both formulations require associativity and an identity.

The corresponding Mathlib constructions are Algebra.toModule and Algebra.ofModule. Mathlib also permits semirings; under the ring hypotheses here, the two formulations describe the same structures.

What's simply called algebra is actually associative algebra with identity, a.k.a. associative unital algebra. See the red herring principle for more about such phenomenon for naming, particularly the example of (possibly) nonassociative algebra.

Let \(A\) and \(B\) be \(R\)-algebras. \(\mathit {1}_A\) and \(\mathit {1}_B\) are ring homomorphisms from \(R\) to \(A\) and \(B\), respectively. A algebra homomorphism from \(A\) to \(B\) is a map \(f : \alpha \to _{a} \beta \) such that

1. \(f\) is a ring homomorphism
2. \(f(\mathit {1}_{A}(r)) = \mathit {1}_{B}(r)\) for each \(r \in R\)

Let \(R\) be a non-commutative ring, \(r\) an arbitrary equivalence relation on \(R\). The ring quotient of \(R\) by \(r\) is the quotient of \(R\) by the strengthen equivalence relation of \(r\) such that for all \(a, b, c\) in \(R\):

1. \(a + c \sim b + c\) if \(a \sim b\)
2. \(a * c \sim b * c\) if \(a \sim b\)
3. \(a * b \sim a * c\) if \(b \sim c\)

As ideals haven't been formalized for the non-commutative case, \(\textsf {Mathlib}\) uses RingQuot in places where the quotient of non-commutative rings by ideal is needed. The universal properties of the quotient are proven, and should be used instead of the definition that is subject to change.

Let \(X\) be an arbitrary set. An free \(R\)-algebra on \(X\) (or "generated by \(X\)"), named \(A\), is the ring quotient of the following inductively constructed set \(A_{\mathtt {pre}}\)

1. for all \(x\) in \(X\), there exists a map \(X \to A_{\mathtt {pre}}\).
2. for all \(r\) in \(R\), there exists a map \(R \to A_{\mathtt {pre}}\).
3. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a + b\) is in \(A_{\mathtt {pre}}\).
4. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a * b\) is in \(A_{\mathtt {pre}}\).

1. there exists a ring homomorphism from \(R\) to \(A_{\mathtt {pre}}\), denoted \(R \to _{+*} A_{\mathtt {pre}}\).
2. \(A\) is a commutative group under \(+\).
3. \(A\) is a monoid under \(*\).
4. left and right distributivity under \(*\) over \(+\).
5. \(0 * a \sim a * 0 \sim 0\).
6. for all \(a, b, c\) in \(A\), if \(a \sim b\), we have
   1. \(a + c \sim b + c\)
   2. \(c + a \sim c + b\)
   3. \(a * c \sim b * c\)
   4. \(c * a \sim c * b\)
   (compatibility with the ring operations \(+\) and \(*\))

Similar to Remark 6, what we defined here is the free (associative, unital) \(R\)-algebra on \(X\), it can be denoted \(R\langle X \rangle \), expressing that it's freely generated by \(R\) and \(X\), where \(X\) is the set of generators.

Let \(R, S\) be rings, \(M\) an \(R\)-module, \(N\) an \(S\)-module. A linear map from \(M\) to \(N\) is a function \(f : M \to _{l} N\) over a ring homomorphism \(\sigma : R \to _{+*} S\), satisfying:

1. \(f(x + y) = f(x) + f(y)\) for all \(x, y \in M\).
2. \(f(r \bullet x) = \sigma (r) \bullet f(x)\) for all \(r \in R\), \(x \in M\).

Let \(R\) be a commutative ring and let \(M,M'\) be \(R\)-modules. The set of all \(R\)-linear maps \(M\to M'\) is denoted \[ \operatorname {Lin}_R(M,M')=\operatorname {Hom}_R(M,M'). \] Here linear map means that the scalar homomorphism is \(\sigma =\operatorname {id}_R\). For this notation and scalar convention, see [stacks2017stacks, Section 10.10, Tag 0581].

For \(M'=M\), write \[ \operatorname {Lin}_R(M)=\operatorname {End}_R(M). \] This is the set of linear endomorphisms of \(M\); its elements are the individual endomorphisms. When the coefficient ring is understood, we omit \(R\) and write \(\operatorname {Lin}(M,M')\) and \(\operatorname {Lin}(M)\).

Let \(A\) be a free \(R\)-algebra generated by module \(M\), let \(\iota : M \to A\) denote the map from \(M\) to \(A\). An tensor algebra over \(M\) (or "of \(M\)") \(T\) is the ring quotient of the free \(R\)-algebra generated by \(M\), by the equivalence relation satisfying:

1. for all \(a, b\) in \(M\), \(\iota (a + b) \sim \iota (a) + \iota (b)\).
2. for all \(r\) in \(R\), \(a\) in \(M\), \(\iota (r \bullet a) \sim r * \iota (a)\).

The definition above is equivalent to the following definition in literature (e.g. [jadczyk2019notes, 1.7]):

Let \(M\) be a module over \(R\). An algebra \(T\) is called a tensor algebra over \(M\) (or "of \(M\)") if it satisfies the following universal properties:

1. \(T\) is an algebra containing \(M\) as a submodule, and it is generated by \(M\),
2. Every linear mapping \(\lambda \) of \(M\) into an algebra \(A\) over \(R\), can be extended to
a homomorphism \(\theta \) of \(T\) into \(A\).