Homotopy Type Theory
generalized Cauchy real numbers > history (Rev #4, changes)
Showing changes from revision #3 to #4:
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 and let
ℚ + ≔ { x ∈ ℚ | 0 < x } \mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}
be the set of positive rational numbers. Let I I be a directed set and
C ( I , ℚ ) ≔ { x ∈ ℚ I | ∀ ϵ ∈ ℚ + . ∃ N ∈ I . ∀ i ∈ I . ∀ j ∈ I . ( i ≥ N ) ∧ ( j ≥ N ) ∧ ( x i ∼ ϵ x j ) } C(I, \mathbb{Q}) \coloneqq \{x \in \mathbb{Q}^I \vert \forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (x_i \sim_{\epsilon} x_j)\}
is the set of all Cauchy net s with index set I I and values in ℚ \mathbb{Q} . Let
CauchyNetsIn ( ℚ ) ≔ ⋃ I ∈ Ob ( DirectedSet 𝒰 ) C ( I , ℚ ) CauchyNetsIn(\mathbb{Q}) \coloneqq \bigcup_{I \in Ob(DirectedSet_\mathcal{U})} C(I, \mathbb{Q})
be the (large) set of all Cauchy nets in ℚ \mathbb{Q} in a universe 𝒰 \mathcal{U} , where DirectedSet 𝒰 DirectedSet_\mathcal{U} is the category of all directed sets in 𝒰 \mathcal{U} .
Let the relation ≡ I , J \equiv_{I, J} in the Cartesian product C ( I , ℚ ) × C ( J , ℚ ) C(I, \mathbb{Q}) \times C(J, \mathbb{Q}) for directed sets I I and J J be defined as
a ≡ I , J b ≔ ∀ ϵ ∈ ℚ + , ∃ M ∈ I . ∀ i ∈ I . ∃ N ∈ J . ∀ j ∈ J . ( i ≥ M ) ∧ ( j ≥ N ) ∧ ( | a i − b j | < ϵ ) a \equiv_{I, J} b \coloneqq \forall \epsilon \in \mathbb{Q}_{+}, \exists M \in I. \forall i \in I. \exists N \in J. \forall j \in J. (i \geq M) \wedge (j \geq N) \wedge (\vert a_i - b_j \vert \lt \epsilon)
The Let a generalized Cauchy real numbers generalized Cauchy algebra is be defined as a set ℝ 𝒰 A \mathbb{R}_\mathcal{U} A with a function ι ∈ ℝ 𝒰 A CauchyNetsIn ( ℚ ) \iota \in {\mathbb{R}_\mathcal{U}}^{CauchyNetsIn(\mathbb{Q})} {A}^{CauchyNetsIn(\mathbb{Q})} such that
∀ I ∈ Ob ( DirectedSet 𝒰 ) . ∀ J ∈ Ob ( DirectedSet 𝒰 ) . ∀ a ∈ C ( I , ℚ ) . ∀ b ∈ C ( J , ℚ ) . ( a ≡ I , J b ) ⇒ ( ι ( a ) = ℝ 𝒰 = ι ( b ) ) \forall I \in Ob(DirectedSet_\mathcal{U}). \forall J \in Ob(DirectedSet_\mathcal{U}). \forall a \in C(I, \mathbb{Q}). \forall b \in C(J, \mathbb{Q}). (a \equiv_{I, J} b) \implies (\iota(a) =_{\mathbb{R}_\mathcal{U}} = \iota(b))
A generalized Cauchy algebra homomorphism is a function f : B A f:B^A between Cauchy algebras A A and B B such that
∀ a ∈ C ( ℚ ) . f ( ι A ( a ) ) = ι B ( a ) \forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)
The category of generalized Cauchy algebras is the category GCAlg GCAlg whose objects Ob ( GCAlg ) Ob(GCAlg) are generalized Cauchy algebras and whose morphisms Mor ( GCAlg ) Mor(GCAlg) are generalized Cauchy algebra homomorphisms. The set of generalized Cauchy real numbers , denoted ℝ \mathbb{R} , is defined as the initial object in the category of Cauchy algebras.
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.
The generalized Cauchy real numbers ℝ 𝒰 \mathbb{R}_\mathcal{U} are inductively generated by the following:
a function ι : ( ∑ I : 𝒰 C ( I , ℚ ) ) → ℝ 𝒰 \iota: \left(\sum_{I:\mathcal{U}} C(I, \mathbb{Q})\right) \to \mathbb{R}_\mathcal{U} , where
C ( I , ℚ ) ≔ isDirected ( I ) × ∑ x : I → ℚ isCauchy ( x ) C(I, \mathbb{Q}) \coloneqq isDirected(I) \times \sum_{x:I \to \mathbb{Q}} isCauchy(x)
is the type of all Cauchy net s with index type I I and values in ℚ \mathbb{Q} .
a dependent family of terms
a : C ( I , ℚ ) , b : C ( J , ℚ ) ⊢ eq ℝ 𝒰 ( a , b ) : isEq ℝ 𝒰 ( a , b ) → ( ι ( a ) = ℝ 𝒰 ι ( b ) ) a:C(I, \mathbb{Q}), b:C(J, \mathbb{Q}) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (\iota(a) =_{\mathbb{R}_\mathcal{U}} \iota(b))
where I I and J J are directed types and the equivalence relation on Cauchy nets isEq ℝ 𝒰 ( a , b ) isEq_{\mathbb{R}_\mathcal{U}}(a, b) is defined as
isEq ℝ 𝒰 ( a , b ) ≔ ∏ ϵ : ℚ + ‖ ∑ M : I ∏ i : I ‖ ∑ N : J ∏ j : J ( i ≥ M ) × ( j ≥ N ) × ( | a i − b j | < ϵ ) ‖ ‖ isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{M:I} \prod_{i:I} \Vert \sum_{N:J} \prod_{j:J} (i \geq M) \times (j \geq N) \times (\vert a_i - b_j \vert \lt \epsilon) \Vert \Vert
a term τ : isSet ( ℝ 𝒰 ) \tau: isSet(\mathbb{R}_\mathcal{U})
See also
Revision on April 14, 2022 at 15:38:51 by
Anonymous? .
See the history of this page for a list of all contributions to it.