Homotopy Type Theory UMyn8W7b (Rev #55)

Euclidean semirings

Given a additively cancellative commutative semiring RR, a term e:Re:R is left cancellative if for all a:Ra:R and b:Rb:R, ea=ebe \cdot a = e \cdot b implies a=ba = b.

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

A term e:Re:R is right cancellative if for all a:Ra:R and b:Rb:R, ae=bea \cdot e = b \cdot e implies a=ba = b.

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

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

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

The multiplicative submonoid of cancellative elements in RR is the subset of all cancellative elements in RR

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

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

Non-cancellative and non-invertible elements

Given a ring RR, an element xRx \in R is non-cancellative if: if there is an element yCan(R)y \in \mathrm{Can}(R) with injection i:Can(R)Ri:\mathrm{Can}(R) \to R such that i(y)=xi(y) = x, then 0=10 = 1. An element xRx \in R is non-invertible if: if there is an element yR ×y \in R^\times with injection j:R ×Rj:R^\times \to R such that j(y)=xj(y) = x, then 0=10 = 1.

 On real numbers and square roots

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

Derivatives

Given an Archimedean ordered integral domain AA such that 𝔻A\mathbb{D} \subseteq A, a function f:AAf:A \to A is pointwise differentiable if it comes with a function (f):AA\partial(f):A \to A called the derivative and a function M:𝔻 +𝔻 +M:\mathbb{D}_+ \to \mathbb{D}_+ on the positive dyadic rationals called the modulus of differentiability such that for every positive dyadic rational ϵ:𝔻 +\epsilon:\mathbb{D}_+, for every term h:Ah:A such that 0<max(h,h)<M(ϵ)0 \lt \max(h, -h) \lt M(\epsilon), and for every term x:Ax:A,

max(h(f)(x)+f(x)f(x+h),f(x+h)f(x)h(f)(x))<ϵ\max(h \partial(f)(x) + f(x) - f(x + h), f(x + h) - f(x) - h \partial(f)(x)) \lt \epsilon

Algebra

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

rules for composition:

  • for all a:Ra:R, af=aa \circ f = a
  • for all f:Af:A, fx=ff \circ x = f
  • for all f:Af:A, xf=fx \circ f = f
  • for all f:Af:A, g:Ag:A, and h:Ah:A, f(gh)=(fg)hf \circ (g \circ h) = (f \circ g) \circ h
  • for all f:Af:A, g:Ag:A, and h:Ah:A, (f+g)h=(fh)+(gh)(f + g) \circ h = (f \circ h) + (g \circ h)
  • for all f:Af:A, g:Ag:A, and h:Ah:A, (fg)h=(fh)(gh)(f g) \circ h = (f \circ h) (g \circ h)

rules for shifts:

  • for all a:Ra:R and f:Af:A S af=f(xa)S_a f = f \circ (x - a)

rules for derivatives:

  • (x)=1\partial(x) = 1
  • for all a:Ra:R, (a)=0\partial(a) = 0
  • for all f:Af:A and g:Ag:A, (f+g)=(f)+(g)\partial(f + g) = \partial(f) + \partial(g)
  • for all f:Af:A and g:Ag:A, (fg)=(f)g+f(g)\partial(f g) = \partial(f) g + f \partial(g)

Symbolic representations of formal smooth functions on the entire domain.

Revision on June 4, 2022 at 00:33:48 by Anonymous?. See the history of this page for a list of all contributions to it.