Homotopy Type Theory univariate rational expressions > history (Rev #2)


Given a field FF, the type of univariate rational expression F(x)F(x) is the field inductively generated by

  • a term x:F(x)x:F(x) representing the indeterminant
  • a function s:FF(x)s:F \to F(x) representing the function of scalars to constant rational expressions
  • a term c:isField(F(x))c:isField(F(x)) representing that F(x)F(x) is a field.
  • a term h:isFieldHom(s)h:isFieldHom(s) representing that s:FF(x)s:F \to F(x) is a field homomorphism?.

A term a:F(x)a:F(x) is a constant univariate rational expression if the fiber of ss at aa is inhabited

isConstant(a)fiber(s,a)isConstant(a) \coloneqq \Vert fiber(s, a) \Vert



Unlike for univariate polynomials, composition is not well defined for univariate rational expressions because the composite of x 1x^{-1} and 00 does not exist by definition of a field. If a reciprocal of 00 did exist, then the type 0=10 = 1 has a term and the commutative reciprocal ring is trivial and thus by definition no longer a field.


For every type F(x)F(x), one could define a function called a derivative

x:F(x)F(x)\frac{\partial}{\partial x}: F(x) \to F(x)

such that there are terms

λ: a:F(x) b:F(x)isConstant(a)×isConstant(b)× p:F(x) q:F(x)x(ap+bq)=ax(p)+bt(q)\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)
π: p:F(x) q:F(x)x(pq)=px(q)+x(p)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
ι:x(x)=1\iota: \frac{\partial}{\partial x}(x) = 1

Thus F(x)F(x) is a differential algebra?.

Since RR is power-associative, there is a term

α: n: +(x(x n+1)=j(n+1)x n)\alpha: \prod_{n:\mathbb{Z}_+} \left(\frac{\partial}{\partial x}(x^{n+1}) = j(n + 1) \cdot x^{n} \right)

for monic function j: +R[x]j:\mathbb{Z}_+ \to R[x] from the positive integers to R[x]R[x].

Since FF is an integral domain, there is a term

ζ: a:RisConstant(a)×(xa=0)\zeta: \prod_{a:R} isConstant(a) \times \left(\frac{\partial}{\partial x}a = 0\right)

and since FF is a field, there is a term

δ: p:F(x) q:F(x)(q#0)×(x(pq)=x(p)1qx(q)pq 2)\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

Revision on March 16, 2022 at 02:44:07 by Anonymous?. See the history of this page for a list of all contributions to it.