nLab Cauchy structure

Contents

Contents

Definition

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

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

be the set of positive rational numbers.

A Cauchy structure is a Booij premetric space (S,)(S, \sim) with a function rat: +Srat:\mathbb{Q}_{+} \to S and a function lim:C(S)Slim:C(S) \to S, where C(S)C(S) is the set of Cauchy approximations in SS, such that

  • for all elements aSa \in S and bSb \in S and all positive rational numbers ϵ\epsilon, a ϵba \sim_\epsilon b implies a=ba = b.

  • for all elements aSa \in S and bSb \in S and all positive rational numbers ϵ\epsilon, |ab|<ϵ\vert a - b \vert \lt \epsilon implies that rat(a) ϵrat(b)rat(a) \sim_\epsilon rat(b)

  • for all elements aSa \in S and Cauchy approximations bC(S)b \in C(S) and all positive rational numbers ϵ\epsilon and η\eta, rat(a) ϵb(η)rat(a) \sim_\epsilon b(\eta) implies that rat(a) ϵ+ηlim(b)rat(a) \sim_{\epsilon + \eta} lim(b)

  • for all Cauchy approximations aC(S)a \in C(S) and elements bSb \in S and all positive rational numbers δ\delta and ϵ\epsilon, a(δ) ϵrat(b)a(\delta) \sim_\epsilon rat(b) implies that lim(a) δ+ϵrat(b)lim(a) \sim_{\delta + \epsilon} rat(b)

  • for all Cauchy approximations aC(S)a \in C(S) and bC(S)b \in C(S) and all positive rational numbers δ\delta, ϵ\epsilon and η\eta, a(δ) ϵb(η)a(\delta) \sim_\epsilon b(\eta) implies that lim(a) δ+ϵ+ηlim(b)lim(a) \sim_{\delta + \epsilon + \eta} lim(b)

For two Cauchy structures SS and TT, a Cauchy structure homomorphism is a function f:STf:S \to T such that

  • for all elements aSa \in S and bSb \in S and all positive rational numbers ϵ\epsilon, a ϵba \sim_{\epsilon} b implies f(a) ϵf(b)f(a) \sim_{\epsilon} f(b).

  • for all rational numbers rr \in \mathbb{Q}, f(rat(r))=rat(r)f(rat(r)) = rat(r)

  • for all Cauchy approximations rC(S)r \in C(S), f(lim(r))=lim(fr)f(lim(r)) = lim(f \circ r)

  • for all elements aSa \in S and aSa \in S, suppose P(a,b)P(a, b) is the predicate that if for all positive rational numbers ϵ\epsilon a ϵba \sim_\epsilon b is true, then a=ba = b, and Q(a,b)Q(a, b) is the predicate that for all positive rational numbers ϵ\epsilon f(a) ϵf(b)f(a) \sim_\epsilon f(b) is true, then f(a)=f(b)f(a) = f(b). Then for all elements aSa \in S and aSa \in S, P(a,b)P(a, b) implies Q(a,b)Q(a, b)

The category of Cauchy structures is a category CauchyStrCauchyStr whose objects Ob(CauchyStr)Ob(CauchyStr) are Cauchy structures and whose morphisms Mor(A,B)Mor(A, B), for objects AOb(CauchyStr)A \in Ob(CauchyStr) and BOb(CauchyStr)B \in Ob(CauchyStr), are Cauchy structure homomorphisms. The initial object in the category of Cauchy structures is the HoTT book real numbers.

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.

A Cauchy structure is a Booij premetric space SS with

  • a function inj:Sinj: \mathbb{Q} \to S

  • a function lim:C(S)Slim: C(S) \to S, where C(S)C(S) is the type of R +R_{+}-Cauchy approximations in SS

  • dependent families of terms

a:S,b:Seq(a,b): ϵ: +(a ϵb)(a= Sb)a:S, b:S \vdash eq(a, b): \Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S b)
a:,b:,ϵ: +μ ,(a,b,ϵ):(|ab|<ϵ)(inj(a) ϵinj(b))a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, \mathbb{Q}}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))
a:,b:C(S),ϵ: +,η: +μ ,C(S)(a,b,ϵ,η):(inj(a) ϵb η)(inj(a) ϵ+ηlim(b))a:\mathbb{Q}, b:C(S), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(S)}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))
a:C(S),b:,δ: +,ϵ: +μ C(S),(a,b,δ,ϵ):(a δ ϵinj(b))(lim(a) δ+ϵinj(b))a:C(S), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(S), \mathbb{Q}}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))
a:C(S),b:C(S),δ: +,ϵ: +,η: +μ C(S),C(S)(a,b,δ,ϵ,η):(a δ ϵb η)(lim(a) δ+ϵ+ηlim(b))a:C(S), b:C(S), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(S), C(S)}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))

For two Cauchy structures SS and TT, a Cauchy structure homomorphism consists of

  • a function f:STf:S \to T

  • a dependent family of functions

    a:S,b:S,ϵ: +π(a,b,ϵ):(a Sϵb)(f(a) Tϵf(b))a:S, b:S, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): (a \sim_{S\epsilon} b) \to (f(a) \sim_{T\epsilon} f(b))
  • a dependent family of types

    r:ι(r):f(inj S(r))=inj T(r)r:\mathbb{Q} \vdash \iota(r): f(inj_S(r)) = inj_T(r)
  • a dependent family of types

    r:C(S)λ(r):f(lim S(r))=lim T(fr)r:C(S) \vdash \lambda(r): f(lim_S(r)) = lim_T(f \circ r)
  • a dependent family of types

    a:S,b:S,c: ϵ: +(a ϵb)η(a,b,c):f(eq S(a,b,c))=eq T(f(a),f(b),f(c))a:S, b:S, c:\Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \vdash \eta(a, b, c): f(eq_S(a, b, c)) = eq_T(f(a), f(b), f(c))

See also

References

  • Auke B. Booij, Analysis in univalent type theory (pdf)

Last revised on May 31, 2022 at 17:28:16. See the history of this page for a list of all contributions to it.