Homotopy Type Theory generalized Cauchy real numbers > history (Rev #3, changes)

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

Contents

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

Definition

Let RR be a dense integral subdomain of the rational numbers \mathbb{Q} and let R +R_{+} be the positive terms of RR.

In set theory

The Letgeneralized Cauchy real numbers\mathbb{Q} be the 𝒰\mathbb{R}_\mathcal{U}rational numbers are and inductively let generated by the following:

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

    C(I,R)isDirected(I)× x:IRisCauchy(x)C(I, R) \coloneqq isDirected(I) \times \sum_{x:I \to R} isCauchy(x)

    is the type of all Cauchy nets with index type II and values in RR.

  • a dependent family of terms

    a:C(I,R),b:C(J,R)eq 𝒰(a,b):isEq 𝒰(a,b)(inj(a)= 𝒰inj(b))a:C(I, R), b:C(J, R) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (inj(a) =_{\mathbb{R}_\mathcal{U}} inj(b))

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

    isEq 𝒰(a,b) ϵ:R + M:I i:I N:J j:J(iM)×(jN)×(|a ib j|<ϵ)isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:R_{+}} \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 τ:isSet( 𝒰)\tau: isSet(\mathbb{R}_\mathcal{U})

+{x|0<x}\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}

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

C(I,){x I|ϵ +.NI.iI.jI.(iN)(jN)(x i ϵx j)}C(I, \mathbb{Q}) \coloneqq \{x \in \mathbb{Q}^I \vert \forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (x_i \sim_{\epsilon} x_j)\}

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

CauchyNetsIn() IOb(DirectedSet 𝒰)C(I,)CauchyNetsIn(\mathbb{Q}) \coloneqq \bigcup_{I \in Ob(DirectedSet_\mathcal{U})} C(I, \mathbb{Q})

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

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

a I,Jbϵ +,MI.iI.NJ.jJ.(iM)(jN)(|a ib j|<ϵ)a \equiv_{I, J} b \coloneqq \forall \epsilon \in \mathbb{Q}_{+}, \exists M \in I. \forall i \in I. \exists N \in J. \forall j \in J. (i \geq M) \wedge (j \geq N) \wedge (\vert a_i - b_j \vert \lt \epsilon)

The generalized Cauchy real numbers is a set 𝒰\mathbb{R}_\mathcal{U} with a function ι 𝒰 CauchyNetsIn()\iota \in {\mathbb{R}_\mathcal{U}}^{CauchyNetsIn(\mathbb{Q})} such that

IOb(DirectedSet 𝒰).JOb(DirectedSet 𝒰).aC(I,).bC(J,).(a I,Jb)(ι(a)= 𝒰ι(b))\forall I \in Ob(DirectedSet_\mathcal{U}). \forall J \in Ob(DirectedSet_\mathcal{U}). \forall a \in C(I, \mathbb{Q}). \forall b \in C(J, \mathbb{Q}). (a \equiv_{I, J} b) \implies (\iota(a) =_{\mathbb{R}_\mathcal{U}} \iota(b))

In homotopy type theory

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

+ x:0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

be the positive rational numbers.

The generalized Cauchy real numbers 𝒰\mathbb{R}_\mathcal{U} are inductively generated by the following:

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

    C(I,)isDirected(I)× x:IisCauchy(x)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 II and values in \mathbb{Q}.

  • a dependent family of terms

    a:C(I,),b:C(J,)eq 𝒰(a,b):isEq 𝒰(a,b)(ι(a)= 𝒰ι(b))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 II and JJ are directed types and the equivalence relation on Cauchy nets isEq 𝒰(a,b)isEq_{\mathbb{R}_\mathcal{U}}(a, b) is defined as

    isEq 𝒰(a,b) ϵ: + M:I i:I N:J j:J(iM)×(jN)×(|a ib j|<ϵ)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 τ:isSet( 𝒰)\tau: isSet(\mathbb{R}_\mathcal{U})

See also

Revision on April 14, 2022 at 01:28:52 by Anonymous?. See the history of this page for a list of all contributions to it.