Homotopy Type Theory Eudoxus real numbers > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Contents

< Eudoxus real numbers

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

An endofunction f: f:\mathbb{Z}^\mathbb{Z} over the integers is bounded if

C.m.|f(m)|<C\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) \vert \lt C

and ff is almost linear if

C.m.n.|f(m+n)f(m)f(n)|<C\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C

Let the set of almost linear endofunctions over the integers be defined as

AL(){f |C.m.n.|f(m+n)f(m)f(n)|<C}AL(\mathbb{Z}) \coloneqq \{f\in \mathbb{Z}^\mathbb{Z} \vert \exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C \}

Let us define a Eudoxus algebra as a set AA with a function ιA AL()\iota \in A^{AL(\mathbb{Z})} such that

fAL().gAL().(C.m.|f(m)g(m)|<C)(ι(f)=ι(g))\forall f \in AL(\mathbb{Z}). \forall g \in AL(\mathbb{Z}). (\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) - g(m) \vert \lt C) \implies (\iota(f) = \iota(g))

An Eudoxus algebra homomorphism between two Eudoxus algebras AA and BB is a function fB Af \in B^A such that

aAL().f(ι A(a))=ι B(a)\forall a \in AL(\mathbb{Z}). f(\iota_A(a)) = \iota_B(a)

The category of Eudoxus algebras is the category EudoxusAlgEudoxusAlg whose objects Ob(EudoxusAlg)Ob(EudoxusAlg) are Eudoxus algebras and whose morphisms Mor(EudoxusAlg)Mor(EudoxusAlg) are Eudoxus algebra homomorphisms. The set of Eudoxus real numbers, denoted \mathbb{R}, is defined as the initial object in the category of Eudoxus algebras.

In homotopy type theory

Let the proposition that an endofunction f:f:\mathbb{Z} \to \mathbb{Z} over the integers is bounded be defined as follows:

isBounded(f) C: m:|f(m)|<CisBounded(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \vert f(m) \vert \lt C \ \right\Vert

and let the proposition that ff is almost linear be defined as follows:

isAlmostLinear(f) C: m: n:|f(m+n)f(m)f(n)|<CisAlmostLinear(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \vert f(m + n) - f(m) - f(n) \vert \lt C \ \right\Vert

Let the type of almost linear endofunctions over the integers be defined as

AL() f:isAlmostLinear(f)AL(\mathbb{Z}) \coloneqq \sum_{f:\mathbb{Z} \to \mathbb{Z}} isAlmostLinear(f)

The type of Eudoxus real numbers, denoted as \mathbb{R}, is a higher inductive type generated by:

  • a function ι:AL()\iota: AL(\mathbb{Z}) \to \mathbb{R}

  • a dependent product of functions from propositions to identities:

η: f:AL() g:AL()isBounded(fg)(ι(f)=ι(g)) \eta : \prod_{f:AL(\mathbb{Z})} \prod_{g:AL(\mathbb{Z})} isBounded(f - g) \to (\iota(f) = \iota(g))
  • A set-truncator
    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{R}} \prod_{b:\mathbb{R}} isProp(a=b)

See also

References

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