Homotopy Type Theory
modulated Cauchy real numbers > history (Rev #8, changes)
Showing changes from revision #7 to #8:
Added | Removed | Changed
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 ℚ \mathbb{Q} and let
ℚ + ≔ { x ∈ ℚ | 0 < x } \mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}
be the positive rational numbers.
The Cauchy real numbers ℝ C \mathbb{R}_C is a set with a function ι ∈ ℝ C C ( ℚ ) \iota \in {\mathbb{R}_C}^{C(\mathbb{Q})} , where C ( ℚ ) C(\mathbb{Q}) is the set of Cauchy approximation s in ℚ \mathbb{Q} and ℝ C C ( ℚ ) {\mathbb{R}_C}^{C(\mathbb{Q})} is the set of functions with domain C ( ℚ ) C(\mathbb{Q}) and codomain ℝ C \mathbb{R}_C , such that
∀ a ∈ C ( ℚ ) . ∀ b ∈ C ( ℚ ) . ( ∀ ϵ ∈ ℚ + . a ϵ ∼ ϵ b ϵ ) ⇒ ( ι ( a ) = ι ( b ) ) \forall a \in C(\mathbb{Q}). \forall b \in C(\mathbb{Q}). \left( \forall \epsilon \in \mathbb{Q}_{+}. a_\epsilon \sim_{\epsilon} b_\epsilon \right) \implies (\iota(a) = \iota(b))
where the premetric for ϵ : ℚ + \epsilon:\mathbb{Q}_{+} is defined as
a ∼ ϵ b ≔ | a ϵ − b ϵ | < 4 ϵ a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon
In homotopy type theory
Let R ℚ R \mathbb{Q} be a dense integral subdomain of the rational numbers and let ℚ \mathbb{Q} and let R + R_{+} be the positive terms of R R .
The Cauchy real numbers ℝ C \mathbb{R}_C are inductively generated by the following:
ℚ + ≔ ∑ x : ℚ 0 < x \mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x
a function ι : C ( R , R + ) → ℝ C \iota: C(R, R_{+}) \to \mathbb{R}_C , where C ( R , R + ) C(R, R_{+}) is the type of R + R_{+} -indexed net s in R R that are R + R_{+} -Cauchy approximation s.
a dependent family of terms
a : C ( R , R + ) , b : C ( R , R + ) ⊢ eq ℝ C ( a , b ) : ( ∏ ϵ : R + a ϵ ∼ ϵ b ϵ ) → ( ι ( a ) = ℝ C ι ( b ) ) a:C(R, R_{+}), b:C(R, R_{+}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:R_{+}} a_\epsilon \sim_{\epsilon} b_\epsilon \right) \to (\iota(a) =_{\mathbb{R}_C} \iota(b))
where the R + R_{+} -premetric for ϵ : R + \epsilon:R_{+} is defined as
a ∼ ϵ b ≔ | a ϵ − b ϵ | < 4 ϵ a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon
a family of dependent terms
a : ℝ C , b : ℝ C ⊢ τ ( a , b ) : isProp ( a = ℝ C b ) a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)
be the positive rational numbers.
The Cauchy real numbers ℝ C \mathbb{R}_C are inductively generated by the following:
a function ι : C ( ℚ ) → ℝ C \iota: C(\mathbb{Q}) \to \mathbb{R}_C , where C ( ℚ ) C(\mathbb{Q}) is the type of Cauchy approximation s in ℚ \mathbb{Q} .
a dependent family of terms
a : C ( ℚ ) , b : C ( ℚ ) ⊢ eq ℝ C ( a , b ) : ( ∏ ϵ : ℚ + a ϵ ∼ ϵ b ϵ ) → ( ι ( a ) = ℝ C ι ( b ) ) a:C(\mathbb{Q}), b:C(\mathbb{Q}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} a_\epsilon \sim_{\epsilon} b_\epsilon \right) \to (\iota(a) =_{\mathbb{R}_C} \iota(b))
where the premetric for ϵ : ℚ + \epsilon:\mathbb{Q}_{+} is defined as
a ∼ ϵ b ≔ | a ϵ − b ϵ | < 4 ϵ a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon
a family of dependent terms
a : ℝ C , b : ℝ C ⊢ τ ( a , b ) : isProp ( a = ℝ C b ) a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)
The Cauchy real numbers are sometimes defined using sequence s x : ℕ → R ℚ x:\mathbb{N} \to R \mathbb{Q} , y : ℕ → R ℚ y:\mathbb{N} \to R \mathbb{Q} with modulus of Cauchy convergence M : R ℚ + → ℕ M:R_{+} M:\mathbb{Q}_{+} \to \mathbb{N} , N : R ℚ + → ℕ N:R_{+} N:\mathbb{Q}_{+} \to \mathbb{N} respectively. However, the composition of a sequence and a modulus of Cauchy convergence yields a Cauchy approximation, so one could define Cauchy approximations a : R ℚ + → R ℚ a:R_{+} a:\mathbb{Q}_{+} \to R \mathbb{Q} as a ≔ x ∘ M a \coloneqq x \circ M and b : R ℚ + → R ℚ b:R_{+} b:\mathbb{Q}_{+} \to R \mathbb{Q} as b ≔ y ∘ N b \coloneqq y \circ N , with x M ( ϵ ) = a ϵ x_{M(\epsilon)} = a_\epsilon and y N ( ϵ ) = b ϵ y_{N(\epsilon)} = b_\epsilon following from function evaluation. In fact, Cauchy approximations and sequences with a modulus of Cauchy convergence are inter-definable.
See also
References
Revision on April 14, 2022 at 00:31:02 by
Anonymous? .
See the history of this page for a list of all contributions to it.