Homotopy Type Theory Cauchy approximation > history (Rev #12)

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

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

be the set of positive rational numbers. Let SS be a premetric space. A Cauchy approximation is a function xS +x \in S^{\mathbb{Q}_{+}}, where S +S^{\mathbb{Q}_{+}} is the set of functions with domain +\mathbb{Q}_{+} and codomain SS, such that

δ +.η +.x(δ) δ+ηx(η)\forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)

The set of all Cauchy approximations is defined as

C(S){xS +|δ +.η +.x(δ) δ+ηx(η)}C(S) \coloneqq \{x \in S^{\mathbb{Q}_{+}} \vert \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)\}

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. Let SS be a premetric space. We define the predicate

isCauchyApproximation(x) δ: + η: +x δ δ+ηx ηisCauchyApproximation(x) \coloneqq \prod_{\delta:\mathbb{Q}_{+}} \prod_{\eta:\mathbb{Q}_{+}} x_\delta \sim_{\delta + \eta} x_\eta

xx is a Cauchy approximation if

x: +Sc(x):isCauchyApproximation(x)x:\mathbb{Q}_{+} \to S \vdash c(x): isCauchyApproximation(x)

The type of Cauchy approximations in SS is defined as

C(S) x: +SisCauchyApproximation(x)C(S) \coloneqq \sum_{x:\mathbb{Q}_{+} \to S} isCauchyApproximation(x)

Properties

Every Cauchy approximation is a Cauchy net indexed by +\mathbb{Q}_{+}. This is because +\mathbb{Q}_{+} is a strictly ordered type, and thus a directed type and a strictly codirected type, with N: +N:\mathbb{Q}_{+} defined as NδηN \coloneqq \delta \otimes \eta for δ: +\delta:\mathbb{Q}_{+} and η: +\eta:\mathbb{Q}_{+}. ϵ: +\epsilon:\mathbb{Q}_{+} is defined as ϵδ+η\epsilon \coloneqq \delta + \eta.

Thus, there is a family of dependent terms

x: +Sn(x):isCauchyApproximation(x)isCauchyNet(x)x:\mathbb{Q}_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)

A Cauchy approximation is the composition xMx \circ M of a net xx and an modulus of Cauchy convergence MM.

See also

References

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