[[!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 $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 $$isConstant(a) \coloneqq \Vert fiber(s, a) \Vert$$ A term $a:R[T]$ is an __indeterminant__ if the [[fiber]] of $t$ at $a$ is inhabited $$isIndeterminant(a) \coloneqq \Vert fiber(t, a) \Vert$$ ## 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[T]} \prod_{b:R[T]} isConstant(a) \times isConstant(b) \times \prod_{p:R[T]} \prod_{q:R[T]} \frac{\partial}{\partial t}(a \cdot p + b \cdot q) = a \cdot \frac{\partial}{\partial t}(p) + 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): \prod_{u:R[T]} \isIndeterminant(u) \times (u = t) \times \left(\frac{\partial}{\partial t}(u) = 1\right)$$ $$t:T \vdash c(t): \prod_{u:R[T]} \isIndeterminant(u) \times (u \neq t) \times \left(\frac{\partial}{\partial t}(u) = 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]] category: not redirected to nlab yet