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 S S be a premetric space . A Cauchy approximation is a function x ∈ S ℚ + x \in S^{\mathbb{Q}_{+}} , where S ℚ + S^{\mathbb{Q}_{+}} is the set of functions with domain ℚ + \mathbb{Q}_{+} and codomain S S , 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 ) ≔ { x ∈ S ℚ + | ∀ δ ∈ ℚ + . ∀ η ∈ ℚ + . 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 S S 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
x x is a Cauchy approximation if
x : ℚ + → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:\mathbb{Q}_{+} \to S \vdash c(x): isCauchyApproximation(x)
The type of Cauchy approximations in S S is defined as
C ( S ) ≔ ∑ x : ℚ + → S isCauchyApproximation ( 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 : ℚ + → S ⊢ n ( x ) : isCauchyApproximation ( x ) → isCauchyNet ( x ) x:\mathbb{Q}_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)
A Cauchy approximation is the composition x ∘ M x \circ M of a net x x and an modulus of Cauchy convergence M M .
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.