[[!redirects polynomial]] < [[nlab:polynomial ring]] ## 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$$ ## See also ## * [[commutative ring]] * [[commutative algebra (ring theory)]] * [[higher inductive type]] * [[differential algebra]] * [[univariate polynomial ring]] category: not redirected to nlab yet