Homotopy Type Theory polynomial ring > history (Rev #1)

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 $ind:T \to R[T]$ representing the indeterminants of the polynomial ring
a function $scal:R \to R[T]$ representing the scalars of the polynomial ring
a term $c:isCRing(R[T])$ representing that the polynomial ring is a commutative ring.
a term $h:isCRingHom(scal)$ representing that $scal:R \to R[T]$ is a commutative ring homomorphism?.

The elements of a polynomial ring are called polynomials.

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

\frac{\partial}{\partial(-)}: T \to (R[T] \to R[T])

such that there are dependent terms

t:T \vdash \lambda(t):\prod_{a:R} \prod_{b:R} \prod_{p:R[T]} \prod_{q:R[T]} \frac{\partial}{\partial t}(scal(a) \cdot p + scal(b) \cdot q) = scal(a) \cdot \frac{\partial}{\partial t}(p) + scal(b) \cdot \frac{\partial}{\partial t}(q)

t:T \vdash \pi(t): \prod_{p:R[T]} \prod_{q:R[T]} \frac{\partial}{\partial t}(p \cdot q) = p \cdot \frac{\partial}{\partial t}(q) + \frac{\partial}{\partial t}(p) \cdot q

t:T \vdash \iota(t): \frac{\partial}{\partial t}(ind(t)) = 1

s:T, t:T \vdash c(s, t): (s \neq t) \times \left(\frac{\partial}{\partial t}(ind(s)) = 0\right)

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

Homotopy Type Theory polynomial ring > history (Rev #1)

Definition

Properties

Partial derivative

See also