Homotopy Type Theory
polynomial ring > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Definition
Given a commutative ring and a type , the polynomial ring is the free commutative algebra generated by , or equivalently, it is a higher inductive type inductively generated by
- a function representing the function of generators to indeterminants of the polynomial ring
- a function representing the function of scalars to constant polynomials of the polynomial ring
- a term representing that the polynomial ring is a commutative ring.
- a term representing that is a commutative ring homomorphism?.
The terma of a polynomial ring are called polynomials.
A term is a constant polynomial if the fiber of at is inhabited
A term is an indeterminant if the fiber of at is inhabited
Properties
Partial derivative
Suppose has decidable equality? and is an integral domain. For every polynomial ring , one could define a function called a partial derivative
such that there are dependent terms
Thus the polynomial ring is a differential algebra?.
See also
Revision on June 15, 2022 at 22:57:17 by
Anonymous?.
See the history of this page for a list of all contributions to it.