Showing changes from revision #59 to #60:
Added | ~~Removed~~ | ~~Chan~~ged

Given a additively cancellative commutative semiring $R$, a term $e:R$ is *left cancellative* if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$.

$\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (a = b)$

A term $e:R$ is *right cancellative* if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$.

$\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)$

An term $e:R$ is *cancellative* if it is both left cancellative and right cancellative.

$\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)$

The **multiplicative submonoid of cancellative elements in $R$** is the subset of all cancellative elements in $R$

$\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)$

A **Euclidean semiring** is a additively cancellative commutative semiring $R$ for which there exists a function $d \colon \mathrm{Can}(R) \to \mathbb{N}$ from the multiplicative submonoid of cancellative elements in $R$ to the natural numbers, often called a *degree function*, a function $(-)\div(-):R \times \mathrm{Can}(R) \to R$ called the *division function*, and a function $(-)\;\%\;(-):R \times \mathrm{Can}(R) \to R$ called the remainder function, such that for all $a \in R$ and $b \in \mathrm{Can}(R)$, $a = (a \div b) \cdot b + (a\;\%\; b)$ and either $a\;\%\; b = 0$ or $d(a\;\%\; b) \lt d(g)$.

Given a ring $R$, an element $x \in R$ is non-cancellative if: if there is an element $y \in \mathrm{Can}(R)$ with injection $i:\mathrm{Can}(R) \to R$ such that $i(y) = x$, then $0 = 1$. An element $x \in R$ is non-invertible if: if there is an element $y \in R^\times$ with injection $j:R^\times \to R$ such that $j(y) = x$, then $0 = 1$.

There is a significant difference between square roots and $n$-th roots. Square roots are the inverse operation of the diagonal $f(x, x)$ for any binary operation $f$, while $n$-th roots are inverse operations of the $n$-dimensional diagonals $g(x, x, \ldots, x)$ for $n$-ary operations, which we typically do not formally talk about in typical practice for rings, etc…

A commutative ring $R$ is a strictly ordered integral domain if it comes with a strict order $\lt$ such that

- $0 \lt 1$
- for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a + b$
- for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a \cdot b$
- for all elements $a:R$ and $b:R$, if $0 \lt \vert a \vert$ and $0 \lt \vert b \vert$, then $0 \lt \vert a \cdot b \vert$

Given a commutative ring $R$, there is a commutative ring $A$ where $R$ is a subring of $A$, with a function $(-)\circ(-):A \times A \to A$ called composition, a term $x:A$ called the composition identity, a function $S_{(-)}:R \times A \to A$ called the shift, and a function $\partial:A \to A$ called the derivative such that

rules for composition:

- for all $a:R$, $a \circ f = a$
- for all $f:A$, $f \circ x = f$
- for all $f:A$, $x \circ f = f$
- for all $f:A$, $g:A$, and $h:A$, $f \circ (g \circ h) = (f \circ g) \circ h$
- for all $f:A$, $g:A$, and $h:A$, $(f + g) \circ h = (f \circ h) + (g \circ h)$
- for all $f:A$, $g:A$, and $h:A$, $(f g) \circ h = (f \circ h) (g \circ h)$

rules for shifts:

- for all $a:R$ and $f:A$ $S_a f = f \circ (x - a)$

rules for derivatives:

- $\partial(x) = 1$
- for all $a:R$, $\partial(a) = 0$
- for all $f:A$ and $g:A$, $\partial(f + g) = \partial(f) + \partial(g)$
- for all $f:A$ and $g:A$, $\partial(f g) = \partial(f) g + f \partial(g)$

Symbolic representations of formal smooth functions on the entire domain.