[[!redirects univariate polynomial]] ## Definition ## Given a [[commutative ring]] $R$, the __univariate polynomial ring__ $R[x]$ is the free [[commutative algebra (ring theory)|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 $$isConstant(a) \coloneqq \Vert fiber(s, a) \Vert$$ ## Properties ## ### Composition of univariate polynomials ### Since the function type $R[x] \to R[x]$ is a [[function algebra|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__ $$\frac{\partial}{\partial x}: R[x] \to R[x]$$ such that there are terms $$\lambda:\prod_{a:R[x]} \prod_{b:R[x]} isConstant(a) \times isConstant(b) \times \prod_{p:R[x]} \prod_{q:R[x]} \frac{\partial}{\partial x}(a \cdot p + b \cdot q) = a \cdot \frac{\partial}{\partial x}(p) + b \cdot \frac{\partial}{\partial t}(q)$$ $$\pi: \prod_{p:R[x]} \prod_{q:R[x]} \frac{\partial}{\partial x}(p \cdot q) = p \cdot \frac{\partial}{\partial x}(q) + \frac{\partial}{\partial x}(p) \cdot q$$ $$\iota: \frac{\partial}{\partial x}(x) = 1$$ Thus the univariate polynomial ring $R[x]$ is a [[differential algebra]]. Since $R$ is power-associative, there is a term $$\alpha: \prod_{n:\mathbb{Z}_+} isConstant(a) \times \left(\frac{\partial}{\partial x}p^{n+1} = j(n) \circ p^{n}\right)$$ 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 $$\zeta: \prod_{a:R} isConstant(a) \times \left(\frac{\partial}{\partial x}a = 0\right)$$ ### Antiderivatives ### Given a polynomial $p:R[x]$, we define the __type of antiderivatives__ of $p$ to be the [[fiber]] of the derivative at $p$: $$antiderivatives(p) \coloneqq fiber(\frac{\partial}{\partial x}, p)$$ ## See also ## * [[commutative ring]] * [[commutative algebra (ring theory)]] * [[polynomial ring]] * [[higher inductive type]] * [[differential algebra]] * [[rational root theorem]] category: not redirected to nlab yet