Homotopy Type Theory UMyn8W7b (Rev #64, changes)

Showing changes from revision #63 to #64: Added | ~~Removed~~ | ~~Chan~~ged

Euclidean semirings

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)$ .

Non-cancellative and non-invertible elements

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$ .

On real numbers and square roots

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…

Commutative rings

Commutative $\mathbb{Q}$ -algebras

A commutative ring $R$ is a commutative $\mathbb{Q}$ -algebra if there is a commutative ring homomorphism $h:\mathbb{Q} \to R$ .

Totally ordered commutative rings

A commutative ring $R$ is a totally ordered commutative ring if it comes with a function $\max:R \times R \to R$ such that

for all elements $a:R$ , $\max(a, a) = a$
for all elements $a:R$ and $b:R$ , $\max(a, b) = \max(b, a)$
for all elements $a:R$ , $b:R$ , and $c:R$ , $\max(a, \max(b, c)) = \max(\max(a, b), c)$
for all elements $a:R$ and $b:R$ , $\max(a, b) = b$ implies that for all elements $c:R$ , $\max(a + c, b + c) = b + c$
for all elements $a:R$ and $b:R$ , $\max(a, 0) = a$ and $\max(b, 0) = b$ implies $\max(a \cdot b, 0) = a \cdot b$
for all elements $a:R$ and $b:R$ , $\max(a, b) = a$ or $\max(a, b) = b$

Totally ordered commutative $\mathbb{Q}$ -algebras

Given totally ordered commutative rings $R$ and $S$ , a commutative ring homomorphism $h:R \to S$ is monotonic if for all $a:R$ and $b:R$ , $\max(h(a), h(b)) = h(\max(a, b))$ .

A totally ordered commutative ring $R$ is a totally ordered commutative $\mathbb{Q}$ -algebra if there is a monotonic commutative ring homomorphism $h:\mathbb{Q} \to R$ .

Strictly ordered integral $\mathbb{Q}$ -algebras

A totally ordered commutative $\mathbb{Q}$ -algebra $R$ is a strictly ordered integral $\mathbb{Q}$ -algebra 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 \max(a, -a)$ and $0 \lt \max(b, -b)$ , then $0 \lt \max(a \cdot b, -a \cdot b)$

Archimedean ordered integral $\mathbb{Q}$ -algebras

…

Modules

Given a commutative ring $R$ , an $R$ -module is an abelian group $M$ with an abelian group homomorphism $\alpha:R \to (M \to M)$ which is also a curried action.

The free $R$ -module on a set $S$ is the initial $R$ -module $M$ with a function $\iota:S \to M$ .

$A_n$ abelian groups

$A_1$ -abelian groups are pointed objects in abelian groups

$A_2$ -abelian groups are unital magma objects in abelian groups

$A_3$ -abelian groups are monoid objects in abelian groups

Algebra

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.

Revision on June 13, 2022 at 12:32:10 by Anonymous?. See the history of this page for a list of all contributions to it.