Theorems · Definition · ring theory

FreeAlgebra

(R : Type u_1) → Type u_2 → [CommSemiring R] → Type (max u_1 u_2)

If α is a type, and R is a commutative semiring, then FreeAlgebra R α is the free (unital, associative) R-algebra generated by α. This is an R-algebra equipped with a function FreeAlgebra.ι R : α → FreeAlgebra R α which has the following universal property: if A is any R-algebra, and f : α → A is any function, then this function is the composite of FreeAlgebra.ι R and a unique R-algebra homomorphism FreeAlgebra.lift R f : FreeAlgebra R α →ₐ[R] A. A typical element of FreeAlgebra R α is an R-linear combination of formal products of elements of α. For example if x and y are terms of type α and a, b are terms of type R then (3 * a * a) • (x * y * x) + (2 * b + 1) • (y * x) + (a * b * b + 3) is a "typical" element of FreeAlgebra R α. In particular if α is empty then FreeAlgebra R α is isomorphic to R, and if α has one term t then FreeAlgebra R α is isomorphic to the polynomial ring R[t]. If α has two or more terms then FreeAlgebra R α is not commutative. One can think of FreeAlgebra R α as the free non-commutative polynomial ring with coefficients in R and variables indexed by α.

Defined in

Mathlib.Algebra.FreeAlgebra

Cited by

48 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiring