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

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

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

Properties

Composition

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.

Derivative

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: +isConstant(x(x n+1)=j(n+1)x n)(a)×(xp n+1=j(n)p n) \alpha: \prod_{n:\mathbb{Z}_+} isConstant(a) \times \left(\frac{\partial}{\partial x}p^{n+1} x}(x^{n+1}) = j(n) j(n \circ + p^{n}\right) 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.