[[!redirects polynomial]] ## Definition ## Given a [[commutative ring]] $R$ and a type $T$, the __polynomial ring__ $R[T]$ is the free [[commutative algebra (ring theory)|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]]. ## See also ## * [[commutative ring]] * [[commutative algebra (ring theory)]] * [[higher inductive type]] * [[differential algebra]] * [[univariate polynomial ring]]