Free commutative rings #
The theory of the free commutative ring generated by a type
It is isomorphic to the polynomial ring over ℤ with variables
Main definitions #
FreeCommRing α: the free commutative ring on a type α
lift (f : α → R): the ring hom
FreeCommRing α →+* Rinduced by functoriality from
map (f : α → β): the ring hom
FreeCommRing α →*+ FreeCommRing βinduced by functoriality from f.
Main results #
FreeCommRing has functorial properties (it is an adjoint to the forgetful functor).
In this file we have:
Implementation notes #
free commutative ring, free ring