Homotopy Type Theory
univariate rational expressions > history (Rev #2)
Definition
Given a field F F , 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 : F → F ( 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 : F → F ( 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 s s at a a is inhabited
isConstant ( a ) ≔ ‖ fiber ( s , a ) ‖ 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 x^{-1} and 0 0 does not exist by definition of a field. If a reciprocal of 0 0 did exist, then the type 0 = 1 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 ) 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 ( a ⋅ p + b ⋅ q ) = a ⋅ ∂ ∂ x ( p ) + b ⋅ ∂ ∂ t ( 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 ( p ⋅ q ) = p ⋅ ∂ ∂ x ( 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 R R 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 F F is an integral domain , there is a term
ζ : ∏ a : R isConstant ( a ) × ( ∂ ∂ x a = 0 ) \zeta: \prod_{a:R} isConstant(a) \times \left(\frac{\partial}{\partial x}a = 0\right)
and since F F is a field, there is a term
δ : ∏ p : F ( x ) ∏ q : F ( x ) ( q # 0 ) × ( ∂ ∂ x ( p q ) = ∂ ∂ x ( p ) ⋅ 1 q − ∂ ∂ x ( q ) ⋅ p q 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.