nLab
Cauchy structure
Redirected from "Cauchy structure homomorphisms".
Contents
Contents
Definition
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.
A Cauchy structure is a Booij premetric space ( S , ∼ ) (S, \sim) with a function rat : ℚ + → S rat:\mathbb{Q}_{+} \to S and a function lim : C ( S ) → S lim:C(S) \to S , where C ( S ) C(S) is the set of Cauchy approximation s in S S , such that
for all elements a ∈ S a \in S and b ∈ S b \in S and all positive rational numbers ϵ \epsilon , a ∼ ϵ b a \sim_\epsilon b implies a = b a = b .
for all elements a ∈ S a \in S and b ∈ S b \in S and all positive rational numbers ϵ \epsilon , | a − b | < ϵ \vert a - b \vert \lt \epsilon implies that rat ( a ) ∼ ϵ rat ( b ) rat(a) \sim_\epsilon rat(b)
for all elements a ∈ S a \in S and Cauchy approximations b ∈ C ( S ) b \in C(S) and all positive rational numbers ϵ \epsilon and η \eta , rat ( a ) ∼ ϵ b ( η ) rat(a) \sim_\epsilon b(\eta) implies that rat ( a ) ∼ ϵ + η lim ( b ) rat(a) \sim_{\epsilon + \eta} lim(b)
for all Cauchy approximations a ∈ C ( S ) a \in C(S) and elements b ∈ S b \in S and all positive rational numbers δ \delta and ϵ \epsilon , a ( δ ) ∼ ϵ rat ( b ) a(\delta) \sim_\epsilon rat(b) implies that lim ( a ) ∼ δ + ϵ rat ( b ) lim(a) \sim_{\delta + \epsilon} rat(b)
for all Cauchy approximations a ∈ C ( S ) a \in C(S) and b ∈ C ( S ) b \in C(S) and all positive rational numbers δ \delta , ϵ \epsilon and η \eta , a ( δ ) ∼ ϵ b ( η ) a(\delta) \sim_\epsilon b(\eta) implies that lim ( a ) ∼ δ + ϵ + η lim ( b ) lim(a) \sim_{\delta + \epsilon + \eta} lim(b)
For two Cauchy structures S S and T T , a Cauchy structure homomorphism is a function f : S → T f:S \to T such that
for all elements a ∈ S a \in S and b ∈ S b \in S and all positive rational numbers ϵ \epsilon , a ∼ ϵ b a \sim_{\epsilon} b implies f ( a ) ∼ ϵ f ( b ) f(a) \sim_{\epsilon} f(b) .
for all rational numbers r ∈ ℚ r \in \mathbb{Q} , f ( rat ( r ) ) = rat ( r ) f(rat(r)) = rat(r)
for all Cauchy approximations r ∈ C ( S ) r \in C(S) , f ( lim ( r ) ) = lim ( f ∘ r ) f(lim(r)) = lim(f \circ r)
for all elements a ∈ S a \in S and b ∈ S b \in S , suppose P ( a , b ) P(a, b) is the predicate that if for all positive rational numbers ϵ \epsilon a ∼ ϵ b a \sim_\epsilon b is true, then a = b a = b , and Q ( a , b ) Q(a, b) is the predicate that for all positive rational numbers ϵ \epsilon f ( a ) ∼ ϵ f ( b ) f(a) \sim_\epsilon f(b) is true, then f ( a ) = f ( b ) f(a) = f(b) . Then for all elements a ∈ S a \in S and b ∈ S b \in S , P ( a , b ) P(a, b) implies Q ( a , b ) Q(a, b)
The category of Cauchy structures is a category CauchyStr CauchyStr whose objects Ob ( CauchyStr ) Ob(CauchyStr) are Cauchy structures and whose morphisms Mor ( A , B ) Mor(A, B) , for objects A ∈ Ob ( CauchyStr ) A \in Ob(CauchyStr) and B ∈ Ob ( CauchyStr ) B \in Ob(CauchyStr) , are Cauchy structure homomorphisms. The initial object in the category of Cauchy structures is the HoTT book real numbers .
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.
A Cauchy structure is a Booij premetric space S S with
a function inj : ℚ → S inj: \mathbb{Q} \to S
a function lim : C ( S ) → S lim: C(S) \to S , where C ( S ) C(S) is the type of R + R_{+} -Cauchy approximation s in S S
dependent families of terms
a : S , b : S ⊢ eq ( a , b ) : ‖ ∏ ϵ : ℚ + ( a ∼ ϵ b ) ‖ → ( a = S b ) a:S, b:S \vdash eq(a, b): \Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S b) a : ℚ , b : ℚ , ϵ : ℚ + ⊢ μ ℚ , ℚ ( a , b , ϵ ) : ( | a − b | < ϵ ) → ( inj ( a ) ∼ ϵ inj ( b ) ) a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, \mathbb{Q}}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b)) a : ℚ , b : C ( S ) , ϵ : ℚ + , η : ℚ + ⊢ μ ℚ , C ( S ) ( a , b , ϵ , η ) : ( inj ( a ) ∼ ϵ b η ) → ( inj ( a ) ∼ ϵ + η lim ( b ) ) a:\mathbb{Q}, b:C(S), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(S)}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b)) a : C ( S ) , b : ℚ , δ : ℚ + , ϵ : ℚ + ⊢ μ C ( S ) , ℚ ( a , b , δ , ϵ ) : ( a δ ∼ ϵ inj ( b ) ) → ( lim ( a ) ∼ δ + ϵ inj ( b ) ) a:C(S), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(S), \mathbb{Q}}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b)) a : C ( S ) , b : C ( S ) , δ : ℚ + , ϵ : ℚ + , η : ℚ + ⊢ μ C ( S ) , C ( S ) ( a , b , δ , ϵ , η ) : ( a δ ∼ ϵ b η ) → ( lim ( a ) ∼ δ + ϵ + η lim ( b ) ) a:C(S), b:C(S), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(S), C(S)}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))
For two Cauchy structures S S and T T , a Cauchy structure homomorphism consists of
a function f : S → T f:S \to T
a dependent family of functions
a : S , b : S , ϵ : ℚ + ⊢ π ( a , b , ϵ ) : ( a ∼ S ϵ b ) → ( f ( a ) ∼ T ϵ f ( b ) ) a:S, b:S, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): (a \sim_{S\epsilon} b) \to (f(a) \sim_{T\epsilon} f(b))
a dependent family of types
r : ℚ ⊢ ι ( r ) : f ( inj S ( r ) ) = inj T ( r ) r:\mathbb{Q} \vdash \iota(r): f(inj_S(r)) = inj_T(r)
a dependent family of types
r : C ( S ) ⊢ λ ( r ) : f ( lim S ( r ) ) = lim T ( f ∘ r ) r:C(S) \vdash \lambda(r): f(lim_S(r)) = lim_T(f \circ r)
a dependent family of types
a : S , b : S , c : ‖ ∏ ϵ : ℚ + ( a ∼ ϵ b ) ‖ ⊢ η ( a , b , c ) : f ( eq S ( a , b , c ) ) = eq T ( f ( a ) , f ( b ) , f ( c ) ) a:S, b:S, c:\Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \vdash \eta(a, b, c): f(eq_S(a, b, c)) = eq_T(f(a), f(b), f(c))
See also
References
Auke B. Booij, Analysis in univalent type theory (pdf )
Last revised on September 2, 2024 at 13:12:44.
See the history of this page for a list of all contributions to it.