Theorems · Definition · commutative algebra

FreeCommRing

Type u → Type u

If α is a type, then FreeCommRing α is the free commutative ring generated by α. This is a commutative ring equipped with a function FreeCommRing.of : α → FreeCommRing α which has the following universal property: if R is any commutative ring, and f : α → R is any function, then this function is the composite of FreeCommRing.of and a unique ring homomorphism FreeCommRing.lift f : FreeCommRing α →+* R. A typical element of FreeCommRing α is a ℤ-linear combination of formal products of elements of α. For example if x and y are terms of type α then 3 * x * x * y - 2 * x * y + 1 is a "typical" element of FreeCommRing α. In particular if α is empty then FreeCommRing α is isomorphic to ℤ, and if α has one term t then FreeCommRing α is isomorphic to the polynomial ring ℤ[t]. One can think of FreeRing α as the free polynomial ring with coefficients in the integers and variables indexed by α.

Defined in

Mathlib.RingTheory.FreeCommRing

Cited by

43 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound