Homotopy Type Theory polynomial ring > history (Rev #4, changes)

Definition

Given a commutative ring $R$ and a type $T$, the polynomial ring $R[T]$ is the free commutative algebra generated by $T$, or equivalently, it is a higher inductive type $R[T]$ inductively generated by

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

The terma of a polynomial ring are called polynomials.

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

A term $a:R[T]$ is an indeterminant if the fiber of $t$ at $a$ is inhabited

Properties

Partial derivative

Suppose $T$ has decidable equality? and $R$ is an integral domain. For every polynomial ring $R[T]$, one could define a function called a partial derivative

such that there are dependent terms

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

See also

• commutative ring
• commutative algebra (ring theory)
• higher inductive type
• differential algebra?
• univariate polynomial ring