9
$\begingroup$

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.

Improve this question
$\endgroup$
14
  • 1
    $\begingroup$ 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? $\endgroup$
    – James E Hanson
    Commented Sep 24, 2022 at 19:54
  • 1
    $\begingroup$ @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? $\endgroup$
    – Z. M
    Commented Sep 24, 2022 at 22:40
  • 1
    $\begingroup$ $\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. $\endgroup$
    – James E Hanson
    Commented Sep 25, 2022 at 2:41
  • 1
    $\begingroup$ What is the simplest proof you know of that uses $\beta X$ to produce a resolution? $\endgroup$
    – James E Hanson
    Commented Sep 25, 2022 at 2:42
  • 1
    $\begingroup$ @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. $\endgroup$
    – Z. M
    Commented Sep 25, 2022 at 8:08

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .