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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #11 to #12: Added | Removed | Changed

Contents

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

Definition

In set theory

A LetCauchy approximationℚ\mathbb{Q} in be a the premetric rational space numbers and letSS 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 SS, such that

∀δ∈ℚ + . ≔ ∀ { η x∈ℚ +ℚ . |0<x ( }δ)∼ δ+ηx(η) \forall \mathbb{Q}_{+} \delta \coloneqq \{x \in \mathbb{Q}_{+}.\forall \mathbb{Q} \eta \vert \in 0 \mathbb{Q}_{+}.x(\delta) \lt \sim_{\delta x\} + \eta} x(\eta)

be the set of positive rational numbers. Let SS 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 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)≔{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 R ℚ R \mathbb{Q} be a dense integral subdomain of therational numbers and letℚ\mathbb{Q} and let R +R_{+} be the positive terms of RR.

Let SS be a R +R_{+}-premetric space. We define the predicate

ℚ +≔∑ x:ℚ0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x
isCauchyApproximation(x)≔∏ δ:R +∏ η:R +x δ∼ δ+ηx ηisCauchyApproximation(x) \coloneqq \prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta

be the positive rational numbers. Let SS be a premetric space. We define the predicate

xx is a R +R_{+}-Cauchy approximation if

isCauchyApproximation(x)≔∏ δ:ℚ +∏ η:ℚ +x δ∼ δ+ηx ηisCauchyApproximation(x) \coloneqq \prod_{\delta:\mathbb{Q}_{+}} \prod_{\eta:\mathbb{Q}_{+}} x_\delta \sim_{\delta + \eta} x_\eta
x:R +→S⊢c(x):isCauchyApproximation(x)x:R_{+} \to S \vdash c(x): isCauchyApproximation(x)

xx is a Cauchy approximation if

The type of R +R_{+}-Cauchy approximations in SS is defined as

x:ℚ +→S⊢c(x):isCauchyApproximation(x)x:\mathbb{Q}_{+} \to S \vdash c(x): isCauchyApproximation(x)
C(S,R +)≔∑ x:R +→SisCauchyApproximation(x)C(S, R_{+}) \coloneqq \sum_{x:R_{+} \to S} 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 aR +R_{+}-Cauchy approximation is a Cauchy net indexed by R ℚ + R_{+} \mathbb{Q}_{+}. This is because R ℚ + R_{+} \mathbb{Q}_{+} is a strictly ordered type, and thus a directed type and a strictly codirected type, with N: R ℚ + N:R_{+} N:\mathbb{Q}_{+} defined as N≔δ⊗ηN \coloneqq \delta \otimes \eta for δ: R ℚ + \delta:R_{+} \delta:\mathbb{Q}_{+} and η: R ℚ + \eta:R_{+} \eta:\mathbb{Q}_{+}. ϵ: R ℚ + \epsilon:R_{+} \epsilon:\mathbb{Q}_{+} is defined as ϵ≔δ+η\epsilon \coloneqq \delta + \eta.

Thus, there is a family of dependent terms

x: R ℚ +→S⊢n(x):isCauchyApproximation(x)→isCauchyNet(x) x:R_{+} x:\mathbb{Q}_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)

An A Cauchy approximation is the compositionR +x∘M R_{+} x \circ M -Cauchy approximation of is a the net compositionx∘M x \circ M of and a an netxx and an R +R_{+}-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.

DiscussNext revision (to current)Previous revision (11 more)Current version of pageHide changesHistory (12 revisions)Rollback Source