Homotopy Type Theory polynomial ring > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definition

Given a commutative ring $R$ and a type $T$ , the polynomial ring $R[T]$ is the free commutative algebra generated by $T$ , or equivalently, it is a higher inductive type $R[T]$ inductively generated by

a function $ind j : T \to R [T]$ ~~ind:T~~ j:T \to R[T] representing the function ofgenerators to indeterminants of the polynomial ring
a function $scal s : R \to R [T]$ ~~scal:R~~ s:R \to R[T] representing the function ofscalars 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 (scal s)$ ~~h:isCRingHom(scal)~~ h:isCRingHom(s) representing that $scal s : R \to R [T]$ ~~scal:R~~ s:R \to R[T] is a commutative ring homomorphism?.

The ~~elements~~ terma of a polynomial ring are calledpolynomials.

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

Properties

Partial derivative

Suppose $T$ has decidable equality? and $R$ is an integral domain. For every polynomial ring $R[T]$ , one could define a function called a partial derivative

\frac{\partial}{\partial(-)}: T \to (R[T] \to R[T])

such that there are dependent terms

t : T ⊢ λ (t) : \prod_{a : R [T]} \prod_{b : R [T]} isConstant (a) \times isConstant (b) \times \prod_{p : R [T]} \prod_{q : R [T]} \frac{\partial}{\partial t} (scal (a) \cdot p + scal (b) \cdot q) = scal (a) \cdot \frac{\partial}{\partial t} (p) + scal (b) \cdot \frac{\partial}{\partial t} (q)

t:T \vdash ~~\lambda(t):\prod_{a:R}~~ \lambda(t):\prod_{a:R[T]} ~~\prod_{b:R}~~ \prod_{b:R[T]} isConstant(a) \times isConstant(b) \times \prod_{p:R[T]} \prod_{q:R[T]} \frac{\partial}{\partial ~~t}(scal(a)~~ t}(a \cdot p + ~~scal(b)~~ b \cdot q) = ~~scal(a)~~ a \cdot \frac{\partial}{\partial t}(p) + ~~scal(b)~~ b \cdot \frac{\partial}{\partial t}(q)

t:T \vdash \pi(t): \prod_{p:R[T]} \prod_{q:R[T]} \frac{\partial}{\partial t}(p \cdot q) = p \cdot \frac{\partial}{\partial t}(q) + \frac{\partial}{\partial t}(p) \cdot q

t : T ⊢ ι (t) : \frac{\partial}{\partial t} \prod_{u : R [T]} isIndeterminant (ind u) \times (u = t)) \times = (\frac{\partial}{\partial t} (u) = 1) 1

t:T \vdash \iota(t): ~~\frac{\partial}{\partial~~ \prod_{u:R[T]} ~~t}(ind(t))~~ \isIndeterminant(u) \times (u = 1 t) \times \left(\frac{\partial}{\partial t}(u) = 1\right)

s : T, t : T ⊢ c (s, t) : \prod_{u : R [T]} isIndeterminant (s u) \times (u \neq t) \times (\frac{\partial}{\partial t} (ind u (s)) = 0)

~~s:T,~~ t:T \vdash ~~c(s,~~ c(t): ~~t):~~ \prod_{u:R[T]} (s \isIndeterminant(u) \times (u \neq t) \times \left(\frac{\partial}{\partial ~~t}(ind(s))~~ t}(u) = 0\right)

Thus the polynomial ring $R[T]$ is a differential algebra?.

Homotopy Type Theory polynomial ring > history (Rev #2, changes)

Definition

Properties

Partial derivative

See also