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: Minima and maxima in Archimedean ordered fields

Madeleine Birchfield (Feb 07 2024 at 15:10):

In constructive mathematics, does every Archimedean ordered (Heyting) field have binary meets (minima) and joins (maxima) for the poset relation defined by the negation of the strict order $x \lt y \coloneqq \neg (y \lt x)$? (Unlike some authors, for the purposes of this question we assume that Archimedean ordered fields do not have binary meets and joins)

Andrew Swan (Feb 07 2024 at 23:58):

In the topos of sheaves on $\mathbb{R}$ you have an object of the sheaf of smooth functions $\mathbb{R} \to \mathbb{R}$. I think that would work as an ordered field where you don't have meets and joins. I'll think about it again in the morning and see if that still makes sense.

Madeleine Birchfield (Feb 08 2024 at 01:11):

The sheaf of smooth functions $\mathbb{R} \to \mathbb{R}$ in the topos may be an ordered field without meets and joins, but is it Archimedean?

Andrew Swan (Feb 08 2024 at 09:59):

Yes, it is also Archimedean. It's a subsheaf of continuous functions $\mathbb{R} \to \mathbb{R}$, which is the Dedekind real numbers in the topos. Since it's a sub ordered field of $\mathbb{R}_d$ and that is Archimedean, it would be as well, I think, but you can also see it directly - you just have to show that for every point $x$ of $\mathbb{R}$ there is a number $n$ and an open neighbourhood $U$ such that $f(x') < n$ for $x' \in U$.

Andrew Swan (Feb 08 2024 at 10:27):

Oh, I see you posted on mathoverflow as well - I'll put the same answer there for reference.

Madeleine Birchfield (Feb 08 2024 at 10:29):

My followup question would be whether it is consistent that there is a Archimedean ordered field $R$ such that every function $f:R \to R$ on $R$ is smooth using the traditional $\epsilon$-$\delta$ definition of smooth function.

Madeleine Birchfield (Feb 08 2024 at 10:35):

Is the Kock-Lawvere axiom logically equivalent to the fact that every function $f:R \to R$ is smooth in the $\epsilon$-$\delta$ sense?

Andrew Swan (Feb 08 2024 at 11:35):

The Kock-Lawvere axiom implies the existence of infinitesimals, which I think shouldn't be necessary for every function to be smooth.

Andrew Swan (Feb 08 2024 at 12:39):

I think the example I gave would satisfy the internal statement that all functions are smooth, but I would have to sit down with a pad of paper and check in details to be sure. I think this should be in a textbook or old paper somewhere, but I don't know specifically where. It's worth checking in Moerdijk-MacLane in case they mentioned it (I don't have a copy with me at the moment).

Madeleine Birchfield (Feb 08 2024 at 14:25):

Also, do the Cauchy real numbers form an ordered subfield of your example Archimedean ordered field in your topos?

Andrew Swan (Feb 08 2024 at 15:04):

Yes, the Cauchy reals are the constant functions $\mathbb{R} \to \mathbb{R}$, which are smooth.

Madeleine Birchfield (Feb 08 2024 at 21:18):

I'd have to start using "Heyting field" instead of "field" when referring to that particular concept in constructive mathematics. In synthetic differential geometry they use a different notion of field in which the apartness relation of the local ring is logically equivalent to negation of equality, rather than being tight as in Heyting fields.