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 }\).

Isomorphism \(A \cong B\) is a bijective homomorphism \(\phi : A \to B\) (it follows that \(\phi ^{-1} : B \to A\) is also a homomorphism).

Endomorphism is a homomorphism from an object to itself, denoted \(\operatorname {End}(A)\).

Automorphism is an endomorphism which is also an isomorphism, denoted \(\operatorname {Aut}(A)\).

Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((A, \bullet )\), satisfying:

1. \(A\) is a ring under \(*\).
2. there exists a ring homomorphism from \(R\) to \(A\), denoted \(\mathit {1} : R \to _{+*} A\).
3. \(\bullet : R \to M \to M\) is a scalar multiplication
4. for every \(r \in R\), \(x \in A\), we have
   1. \(r * x = x * r\) (commutativity between \(R\) and \(A\))
   2. \(r \bullet x = r * x\) (definition of scalar multiplication)
   where we omitted that the ring homomorphism \(\mathit {1}\) is applied to \(r\) before each multiplication.

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.

The definition above (adopted in \(\textsf {Mathlib}\)) is more general than the definition in literature (e.g. [jadczyk2019notes, 1.6]):

Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((M, *)\), satisfying:

1. \(A\) is a module \(M\) over \(R\) under \(+\) and \(\bullet \).
2. \(A\) is a ring under \(*\).
3. For \(x, y \in A, a \in R\), we have
\[ a \bullet (x * y) = (a \bullet x) * y = x * (a \bullet y) \]

See Implementation notes in Algebra for details.

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\).

The set of all linear maps from \(M\) to \(M'\) is denoted \(\operatorname {Lin}(M, M')\), and \(\operatorname {Lin}(M)\) for mapping from \(M\) to itself. \(\operatorname {Lin}(M)\) is an endomorphism.

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\).