Showing changes from revision #8 to #9: Added | Removed | Changed

Contents

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

Definition

In set theory

Let $\mathbb{Q}$ be the rational numbers $\mathbb{Q}$ and let

be the positive rational numbers.

The Let us define aCauchy real numbersCauchy algebra to be a$\mathbb{R}_C$ is a set with a function$\mathrm{<span><del\; class="diffmod">\; \iota </del><ins\; class="diffmod">\; A</ins></span>}\in {{ℝ}_C}^{C(\mathbb{Q})}$ \iota A \in {\mathbb{R}_C}^{C(\mathbb{Q})} , where with a function$\mathrm{<span><del\; class="diffmod">\; C</del><ins\; class="diffmod">\; \iota </ins></span>}<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; \in </ins></span>\mathbb{Q}{A}^{C(\mathbb{Q})})$ C(\mathbb{Q}) \iota \in A^{C(\mathbb{Q})} , is where the set of$C(\mathbb{Q})$ is the set of Cauchy approximations in $\mathbb{Q}$ and ${{ℝ}_C}^A$ {\mathbb{R}_C}^{C(\mathbb{Q})} A^{C(\mathbb{Q})} is the set of functions with domain $C(\mathbb{Q})$ and codomain ${ℝ}_{C}A$ \mathbb{R}_C A, such that

where A thepremetricCauchy algebra homomorphism for is a function$\mathrm{<span><del\; class="diffmod">\; ϵ</del><ins\; class="diffmod">\; f</ins></span>}:{\mathbb{Q}}_{+}{B}^A$ \epsilon:\mathbb{Q}_{+} f:B^A is between defined Cauchy as algebras$A$ and $B$ such that

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

In homotopy type theory

Let $\mathbb{Q}$ be the rational numbers and let

be the positive rational numbers.

The Cauchy real numbers $\mathbb{R}_C$ are inductively generated by the following:

• a function $\iota: C(\mathbb{Q}) \to \mathbb{R}_C$, where $C(\mathbb{Q})$ is the type of Cauchy approximations in $\mathbb{Q}$.

• a dependent family of terms

  $$a:C(\mathbb{Q}),b:C(\mathbb{Q})⊢{\mathrm{eq}}_{{ℝ}_C}(a,b):\left(\prod _{ϵ:{\mathbb{Q}}_{+}}|a_{ϵ}{\sim }_{ϵ}-b_{ϵ}|<4ϵ\right)\to (\iota (a){=}_{{ℝ}_C}\iota (b))$$ a:C(\mathbb{Q}), b:C(\mathbb{Q}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} \vert a_\epsilon \sim_{\epsilon} - b_\epsilon \vert \lt 4 \epsilon \right) \to (\iota(a) =_{\mathbb{R}_C} \iota(b))

  where the premetric for $\epsilon:\mathbb{Q}_{+}$ is defined as

  $$a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon$$

• a family of dependent terms

  $$a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)$$

Comment

The Cauchy real numbers are sometimes defined using sequences $x:\mathbb{N} \to \mathbb{Q}$, $y:\mathbb{N} \to \mathbb{Q}$ with modulus of Cauchy convergence $M:\mathbb{Q}_{+} \to \mathbb{N}$, $N:\mathbb{Q}_{+} \to \mathbb{N}$ respectively. However, the composition of a sequence and a modulus of Cauchy convergence yields a Cauchy approximation, so one could define Cauchy approximations $a:\mathbb{Q}_{+} \to \mathbb{Q}$ as $a \coloneqq x \circ M$ and $b:\mathbb{Q}_{+} \to \mathbb{Q}$ as $b \coloneqq y \circ N$, with $x_{M(\epsilon)} = a_\epsilon$ and $y_{N(\epsilon)} = b_\epsilon$ following from function evaluation. In fact, Cauchy approximations and sequences with a modulus of Cauchy convergence are inter-definable.

See also

• Cauchy real numbers (disambiguation)
• generalized Cauchy real numbers
• HoTT book real numbers
• premetric space
• quotient set
• infinite decimal representation of the Cauchy real numbers?

References

• Auke B. Booij, Analysis in univalent type theory (pdf)
• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)