Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Universal properties of lower and upper Dedekind reals

Madeleine Birchfield (Dec 20 2024 at 01:35):

The usual two-sided Dedekind real numbers can be characterised by the universal property of the terminal Archimedean ordered field, and this remains true constructively (i.e. in the absence of excluded middle), provided we use the right definition of Archimedean ordered field.

What are the universal properties of the lower Dedekind real numbers and the upper Dedekind real numbers?

David Michael Roberts (Dec 20 2024 at 02:45):

What's the constructively correct definition of Archimedean ordered field, again?

Madeleine Birchfield (Dec 20 2024 at 15:47):

David Michael Roberts said:

What's the constructively correct definition of Archimedean ordered field, again?

A constructively valid definition of Archimedean ordered field can be found in definition 11.2.7 of Homotopy Type Theory: Univalent Foundations of Mathematics, but the axioms given there are not a minimal set of axioms for an Archimedean ordered field. The proof that the Dedekind real numbers are the terminal Archimedean ordered field can be found in section 11.2.3 of the same text. (The authors talk about Archimedean ordered fields admissible for a sublattice $\Sigma \subseteq \Omega$ of the subset classifier $\Omega$, but you can assume $\Sigma$ to be $\Omega$ itself for the purposes of this discussion.)

There is actually some debate in constructive real analysis whether the $\leq$ poset relation needs to have binary meets and joins (i.e. $\min$ and $\max$) or not for Archimedean ordered fields, but regardless either way the Dedekind real numbers are still the terminal Archimedean ordered field.