Free rings #
The theory of the free ring over a type.
Main definitions #
FreeRing α
: the free (not commutative in general) ring over a type.lift (f : α → R)
: the ring homFreeRing α →+* R
induced byf
.map (f : α → β)
: the ring homFreeRing α →+* FreeRing β
induced byf
.
Implementation details #
FreeRing α
is implemented as the free abelian group over the free monoid on α
.
Tags #
free ring
If α
is a type, then FreeRing α
is the free ring generated by α
.
This is a ring equipped with a function FreeRing.of : α → FreeRing α
which has
the following universal property: if R
is any ring, and f : α → R
is any function,
then this function is the composite of FreeRing.of
and a unique ring homomorphism
FreeRing.lift f : FreeRing α →+* R
.
A typical element of FreeRing α
is a ℤ
-linear combination of
formal products of elements of α
.
For example if x
and y
are terms of type α
then 3 * x * y * x - 2 * y * x + 1
is a
"typical" element of FreeRing α
. In particular if α
is empty
then FreeRing α
is isomorphic to ℤ
, and if α
has one term t
then FreeRing α
is isomorphic to the polynomial ring ℤ[t]
.
If α
has two or more terms then FreeRing α
is not commutative.
One can think of FreeRing α
as the free non-commutative polynomial ring
with coefficients in the integers and variables indexed by α
.
Equations
- FreeRing α = FreeAbelianGroup (FreeMonoid α)
Instances For
Equations
Equations
The ring homomorphism FreeRing α →+* R
induced from a map α → R
.
Instances For
The canonical ring homomorphism FreeRing α →+* FreeRing β
generated by a map α → β
.
Equations
- FreeRing.map f = FreeRing.lift (FreeRing.of ∘ f)