Homotopy Type Theory Sandbox (Rev #58, changes)

Showing changes from revision #57 to #58: Added | Removed | Changed

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 with element γ:A\gamma:A, p:0<γp:0 \lt \gamma, and q:γ<1q:\gamma \lt 1, a function f:AAf:A \to A is pointwise smooth differentiable if it comes with a function sequenceDD ()(f):(AA) D(f):A D^{(-)}(f):\mathbb{N} \to A (A \to A) called the iterated derivative sequence and a function sequence of functionsMM ():(A +A +) M:A_+ M^{(-)}:\mathbb{N} \to A_+ (A_+ \to A_+) on in the positive elements ofAA called the modulus moduli sequence of iterated differentiability , such that for every positive elementϵ:A +\epsilon:A_+, for every element h:Ah:A such that 0<max(h,h)<M(ϵ)0 \lt \max(h, -h) \lt M(\epsilon), and for every element x:Ax:A,

max(hD(f)(x)+f(x)f(x+h),f(x+h)f(x)hD(f)(x))<ϵ\max(h D(f)(x) + f(x) - f(x + h), f(x + h) - f(x) - h D(f)(x)) \lt \epsilon
  • D 0(f)=fD^{0}(f) = f

  • for every natural number n:n:\mathbb{N}, for every positive element ϵ:A +\epsilon:A_+, for every element h:Ah:A such that 0<max(h,h)<M n+1(ϵ)0 \lt \max(h, -h) \lt M^{n+1}(\epsilon), and for every element x:Ax:A,

    max(hD n+1(f)(x)+D n(f)(x)D n(f)(x+h),D n(f)(x+h)D n(f)(x)hD n+1(f)(x))<M n(ϵ)\max(h D^{n + 1}(f)(x) + D^{n}(f)(x) - D^{n}(f)(x + h), D^{n}(f)(x + h) - D^{n}(f)(x) - h D^{n + 1}(f)(x)) \lt M^{n}(\epsilon)

Given an Archimedean ordered integral domain AA with element γ:A\gamma:A, p:0<γp:0 \lt \gamma, and q:γ<1q:\gamma \lt 1, a function f:AAf:A \to A is smooth if it comes with a sequence D ()(f):(AA)D^{(-)}(f):\mathbb{N} \to (A \to A) called the iterated derivative sequence and a sequence of functions M ():(A +A +)M^{(-)}:\mathbb{N} \to (A_+ \to A_+) in the positive elements of AA called the moduli sequence of iterated differentiability, such that

  • D 0(f)=fD^{0}(f) = f

  • for every natural number n:n:\mathbb{N}, for every positive element ϵ:A +\epsilon:A_+, for every element h:Ah:A such that 0<max(h,h)<M n+1(ϵ)0 \lt \max(h, -h) \lt M^{n+1}(\epsilon), and for every element x:Ax:A,

    max(hD n+1(f)(x)+D n(f)(x)D n(f)(x+h),D n(f)(x+h)D n(f)(x)hD n+1(f)(x))<M n(ϵ)\max(h D^{n + 1}(f)(x) + D^{n}(f)(x) - D^{n}(f)(x + h), D^{n}(f)(x + h) - D^{n}(f)(x) - h D^{n + 1}(f)(x)) \lt M^{n}(\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 10, 2022 at 18:21:46 by Anonymous?. See the history of this page for a list of all contributions to it.