[[!redirects univariate rational expression]] ## Definition ## Given a [[field (ring theory)|field]] $F$, the type of __univariate rational expression__ $F(x)$ is the field inductively generated by * a term $x:F(x)$ representing the __indeterminant__ * a function $s:F \to F(x)$ representing the function of __scalars__ to __constant rational expressions__ * a term $c:isField(F(x))$ representing that $F(x)$ is a [[field (ring theory)|field]]. * a term $h:isFieldHom(s)$ representing that $s:F \to F(x)$ is a [[field homomorphism]]. A term $a:F(x)$ is a __constant univariate rational expression__ if the [[fiber]] of $s$ at $a$ is inhabited $$isConstant(a) \coloneqq \Vert fiber(s, a) \Vert$$ ## Properties ## ### Composition ### Unlike for [[univariate polynomial]]s, composition is not well defined for univariate rational expressions because the composite of $x^{-1}$ and $0$ does not exist by definition of a field. If a reciprocal of $0$ did exist, then the type $0 = 1$ has a term and the [[commutative reciprocal ring]] is trivial and thus by definition no longer a field. ### Derivative ### For every type $F(x)$, one could define a function called a __derivative__ $$\frac{\partial}{\partial x}: F(x) \to F(x)$$ such that there are terms $$\lambda:\prod_{a:F(x)} \prod_{b:F(x)} isConstant(a) \times isConstant(b) \times \prod_{p:F(x)} \prod_{q:F(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:F(x)} \prod_{q:F(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 $F(x)$ is a [[differential algebra]]. Since $R$ is power-associative, there is a term $$\alpha: \prod_{n:\mathbb{Z}_+} \left(\frac{\partial}{\partial x}(x^{n+1}) = j(n + 1) \cdot x^{n} \right)$$ for [[monic function]] $j:\mathbb{Z}_+ \to R[x]$ from the positive [[integers]] to $R[x]$. Since $F$ is an [[integral domain]], there is a term $$\zeta: \prod_{a:R} isConstant(a) \times \left(\frac{\partial}{\partial x}a = 0\right)$$ and since $F$ is a field, there is a term $$\delta: \prod_{p:F(x)} \prod_{q:F(x)} (q # 0) \times \left(\frac{\partial}{\partial x}\left(\frac{p}{q}\right) = \frac{\partial}{\partial x}(p) \cdot \frac{1}{q} - \frac{\partial}{\partial x}(q) \cdot \frac{p}{q^2} \right)$$ ## See also ## * [[field (ring theory)]] * [[univariate polynomial ring]] * [[higher inductive type]] * [[differential algebra]]