Showing changes from revision #3 to #4: 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 and let

be the set of positive rational numbers. Let $I$ be a directed set and

is the set of all Cauchy nets with index set $I$ and values in $\mathbb{Q}$. Let

be the (large) set of all Cauchy nets in $\mathbb{Q}$ in a universe $\mathcal{U}$, where $DirectedSet_\mathcal{U}$ is the category of all directed sets in $\mathcal{U}$.

Let the relation $\equiv_{I, J}$ in the Cartesian product $C(I, \mathbb{Q}) \times C(J, \mathbb{Q})$ for directed sets $I$ and $J$ be defined as

The Let ageneralized Cauchy real numbersgeneralized Cauchy algebra is be defined as aset ${ℝ}_{𝒰}A$ \mathbb{R}_\mathcal{U} A with a function $\iota \in {{ℝ}_{𝒰}}^A$ \iota \in {\mathbb{R}_\mathcal{U}}^{CauchyNetsIn(\mathbb{Q})} {A}^{CauchyNetsIn(\mathbb{Q})} such that

A generalized Cauchy algebra homomorphism is a function $f:B^A$ between Cauchy algebras $A$ and $B$ such that

$$\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)$$

The category of generalized Cauchy algebras is the category $GCAlg$ whose objects $Ob(GCAlg)$ are generalized Cauchy algebras and whose morphisms $Mor(GCAlg)$ are generalized Cauchy algebra homomorphisms. The set of generalized Cauchy real numbers, denoted $\mathbb{R}$, 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 generalized Cauchy real numbers $\mathbb{R}_\mathcal{U}$ are inductively generated by the following:

• a function $\iota: \left(\sum_{I:\mathcal{U}} C(I, \mathbb{Q})\right) \to \mathbb{R}_\mathcal{U}$, where

  $$C(I, \mathbb{Q}) \coloneqq isDirected(I) \times \sum_{x:I \to \mathbb{Q}} isCauchy(x)$$

  is the type of all Cauchy nets with index type $I$ and values in $\mathbb{Q}$.

• a dependent family of terms

  $$a:C(I, \mathbb{Q}), b:C(J, \mathbb{Q}) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (\iota(a) =_{\mathbb{R}_\mathcal{U}} \iota(b))$$

  where $I$ and $J$ are directed types and the equivalence relation on Cauchy nets $isEq_{\mathbb{R}_\mathcal{U}}(a, b)$ is defined as

  $$isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{M:I} \prod_{i:I} \Vert \sum_{N:J} \prod_{j:J} (i \geq M) \times (j \geq N) \times (\vert a_i - b_j \vert \lt \epsilon) \Vert \Vert$$

• a term $\tau: isSet(\mathbb{R}_\mathcal{U})$

See also

• Cauchy real numbers (disambiguation)
• HoTT book real numbers
• Cauchy real numbers
• premetric space