Homotopy Type Theory univariate polynomial ring > history (changes)

Definition

Given a commutative ring $R$, the univariate polynomial ring $R[x]$ is the free commutative algebra generated by the unit type?, or equivalently, it is a higher inductive type $R[x]$ inductively generated by

• a term $x:R[x]$ representing the indeterminant of the univariate polynomial ring
• a function $s:R \to R[x]$ representing the function of scalars to constant univariate polynomials of the univariant polynomial ring
• a term $c:isCRing(R[x])$ representing that the univariate polynomial ring is a commutative ring.
• a term $h:isCRingHom(s)$ representing that $s:R \to R[x]$ is a commutative ring homomorphism?.

The elements of a univariate polynomial ring are called univariate polynomials.

A term $a:R[T]$ is a constant univariate polynomial if the fiber of $s$ at $a$ is inhabited

Properties

Composition of univariate polynomials

Since the function type $R[x] \to R[x]$ is a function $R$-algebra with the commutative $R$-algebra homomorphism to constant functions $C:R \to (R[x] \to R[x])$, there exists a commutative $R[x]$-algebra homomorphism $i:R[x] \to (R[x] \to R[x])$ inductively defined by $i(s(r)) \coloneqq C(r)$ for $r:R$ and $i(x) \coloneqq id_{R[x]}$. The composition of univariate polynomials $(-) \circ (-):R[x] \times R[x] \to R[x]$ is the uncurrying of $i$, $p \circ q \coloneqq i(p)(q)$ for $p:R[x]$ and $q:R[x]$.

Derivative

For every univariate polynomial ring $R[x]$, one could define a function called a derivative

such that there are terms

Thus the univariate polynomial ring $R[x]$ is a differential algebra?.

Since $R$ is power-associative, there is a term

for monic function $j:\mathbb{Z}_+ \to R[x]$ from the positive integers to $R[x]$.

If $R$ is an integral domain, then there is a term

Antiderivatives

Given a polynomial $p:R[x]$, we define the type of antiderivatives of $p$ to be the fiber of the derivative at $p$:

See also

• commutative ring
• commutative algebra (ring theory)
• polynomial ring
• higher inductive type
• differential algebra?
• rational root theorem