9

I recently learnt from David Roberts' answer that, there is a way, due to Colin McLarty, to set up the foundations on finite order arithmetic for EGA & SGA. In particular, all usages of Grothendieck universes or inaccessible cardinals in EGA & SGA are supposed to be realizable in a (conservative extension of) finite order arithmetic (or ETCS).

I am no logician, but after a glimpse at McLarty's paper, it seems that this is very different from the usual approach of choosing cut-off cardinals in, say, Stacks Project. If I understand correctly, due to lack of axiom of replacement, the usual cardinal arithmetic does not seem to work well, at least a class "being small" cannot be simply tested by its cardinality. In other words, we cannot simply understand this as a "size issue" as in ZFC.

Now I wonder whether/how much condensed mathematics can be founded on such a weaker system? If I understand correctly, there are some issues about constructing "large rings" there, so to avoid extra complications, let me restrict to the content of chapters 1-6 of Lectures on Condensed Mathematics, i.e. up to solid abelian groups. And also, to avoid complications from higher categories, I would first look at the 1-categorical structures instead of derived $\infty$-categories.

Update: For example, I wonder whether the proof of Prop 2.9 can be founded, or interpreted in ETCS, with some modifications of the proposition itself?

Here is a motivation for seeking such weaker systems. When we use condensed mathematics to reproduce some classical theorems (such as coherent duality and basic theorems in complex analysis), or some slight generalizations, it seems probable that their classical proofs only rely on something much weaker than ZFC, and I hope that the proof using condensed mathematics can be interpreted in at least a not-much-stronger system.

Z. M
  • 2,003
  • 1
    Generally speaking, the order of arithmetic needed to formalize something is going to correspond to how many iterated power sets you need. In order to talk about arbitrary subsets of a Polish space, you would need at least third-order arithmetic, for instance. What are the constructions in condensed math that end up needing bigger objects? Do the profinite sets need to be arbitrarily big, or could they all be metrizable? – James Hanson Sep 24 '22 at 19:54
  • 1
    @JamesHanson A priori not metrizable (at least, in the current proof, one should consider the space $\beta X$ of ultrafilters and its iterations, to produce resolutions, but maybe one could consider some smaller ones instead). I am not sure whether I understand McLarty's paper correctly, but seemingly one takes all finite orders, and it is closely related to Lawvere's ETCS? – Z. M Sep 24 '22 at 22:40
  • 1
    $\omega$th-order arithmetic (as in the theory with a sort for $\mathcal{P}^n(\mathbb{N})$ for each $n$) is mutually interpretable with a Boolean topos with natural numbers object, which I think is basically the same as ETCS. – James Hanson Sep 25 '22 at 02:41
  • 1
    What is the simplest proof you know of that uses $\beta X$ to produce a resolution? – James Hanson Sep 25 '22 at 02:42
  • 1
    @JamesHanson The key property is that they are extremally disconnected sets, and every extremally disconnected set is a retract of such. Extremally connected sets are precisely compact projective objects (aka. strongly of finite presentation) of the category of condensed sets. Consequently, say, in the category of condensed abelian groups, you have enough projective objects. – Z. M Sep 25 '22 at 08:08
  • 1
    @JamesHanson Another fact: sheaves on profinite sets is essentially same as sheaves on extremally disconnected sets (since the latter form a base), and the topology on the latter is simply the extensive topology: covers are generated by ${U\to U\sqcup V,V\to U\sqcup V}$, and everything covers empty. However, it is unclear whether this is essential, since the proofs use that maybe just for sake of simplification. – Z. M Sep 25 '22 at 08:12
  • 1
    Something I’ve been wondering about is whether condensed mathematics uses in any essential way that profinite sets can be concretely realised as topological spaces. Put it another way, could we use the formal $\textbf{Pro}(\textbf{FinSet})$ or even $\textbf{Bool}^\textrm{op}$ instead of profinite topological spaces? – Zhen Lin Sep 25 '22 at 08:24
  • 1
    @ZhenLin I suspect that you're right and that we do not "really" need the relationship with topological spaces, although I haven't checked it in detail. You probably need it to compare the theory of condensed sets to the preexisting theory of topological spaces though... – Denis Nardin Sep 25 '22 at 08:47
  • 1
    @ZhenLin I am not sure about your context. For example, they are not necessarily equivalent without AC, but developping condensed math without AC seems to be harder than what I asked. My question is somehow "simply" about applying McLarthy's paper to condensed math. – Z. M Sep 25 '22 at 09:04
  • 1
    Yes, but in the same way it may be that these categories are inequivalent if we don’t have sufficiently complex sets. Or maybe they are equivalent but a particular choice is easier to work with in finite-order arithmetic. At the very least the different categories have completely different “natural” codings… – Zhen Lin Sep 25 '22 at 11:44
  • 1
    @ZhenLin I do wonder if one could use locales instead of topological spaces when undertaking such an exercise. – David Roberts Sep 25 '22 at 13:43
  • 1
    Peter Scholze wondered if one could set up other work he's done in weaker axioms than ZFC.

    One might wonder what the effect of not having strong limit cardinals would have on building condensed sets; strong limits are essentially like inaccessibles for ETCS, so it might be closer to how pyknotic sets work.

     – David Roberts Sep 25 '22 at 13:54
  • 1
    @Z.M $\beta X$ is still just a subset of $\mathcal{P}^2(X)$. Are there many proofs that require building some inductive sequence of resolutions? Something where you start with $X_0$, then you build $X_{n+1}$ that is comparable in size to $\beta X_n$ for all $n$? This is the kind of thing that would end up pushing you outside of $\omega$th-order arithmetic. – James Hanson Sep 25 '22 at 16:29
  • 1
    @JamesHanson If you build projective resolutions in condensed abelian groups, this will happen, so it's definitely convenient. Whether the proofs really require you to choose a full projective resolution may be a different matter. And I'm sure much of the theory works in much weaker fragments. – Peter Scholze Oct 28 '22 at 09:32

0 Answers0