Are there lightweight foundations for arbitrarily extendable objects?

Question

My experience with foundations is rather scant, but I've run into some types of objects that seem to resist the sort of set-theoretic encoding schemes via Kurowski tuples that are rather common for objects like groups and manifolds. In particular, they tend to be something like functions that can accept arbitrarily large inputs. I am wondering if such objects can be given foundations in a reasonably parsimonious way, so we don't have to include all possible inputs when considering such a function. The following are three examples:

1. Random variables: I read from Gowers's blog post that analysts define random variables as measurable functions satisfying some conditions, but that probabilists use them in a manner inconsistent with that definition. In particular, one has the problem of respecifying the sample space when new random variables come into play. If someone came up to me on the street and asked me to formalize this, I would probably respond by encoding a random variable using a proper class of all possible extensions of sample spaces. Naturally, this seems to be a rather weighty thing to carry around if I want to say that a particular probability manipulation is well-defined. From what I read in Tao's blog post, it seems that in practice, one encloses all mention of random variables in something like a type theory where the only allowable operations and quantities are those that are invariant under extension of sample space. Unfortunately, I know next to nothing about formal type theory - would this yield a decent answer?

2. Presheaves and sheaves on a site: Sometimes in algebraic geometry, one considers Grothendieck topologies like the fpqc topology, where even over a point, the isomorphism types of open sets and open covers form a proper class. One then encounters problems in the literature, where people claim that fpqc sheafification is a functor, but they prove it using a forbidden colimit over all open covers. This is an honest problem: in his paper Basically bounded functors and flat sheaves (Pac. J. Math. 57 no. 2 1975), Waterhouse produces a presheaf that has no fpqc sheafification. However, he also shows that for those presheaves that are left Kan extensions of presheaves on rings with a cardinality bound, sheafification and cohomology are independent of the bound for any topology (e.g., fpqc) satisfying a small approximation property. These left Kan extensions are commonly known as small presheaves, and essentially all geometrically interesting presheaves are small. In less technical and more general terms, we don't really need to make set-theoretic assumptions about the existence of universes, or truncate our presheaves to only take rings of size below some (possibly strongly inaccessible) bound, as long as we are only doing operations that preserve a sense of smallness. It would be nice, though perhaps not of fundamental importance, to have a formalism that made the recognition of such operations straightforward.

3. Supergeometry: While mathematicians often view supermanifolds as manifolds with sheaves of supercommutative rings, physicists doing first variation calculations for superfields often make use of an "odd parameter" that acts like an odd free variable that (as far as I can tell) completely fails to fit into the mathematicians' rings. In his book "Supermanifolds", DeWitt attempts to resolve this problem by adjoining countably infinitely many odd variables to everything in sight, but this seems to make physicists unhappy because infinitely many of those variables are unused and therefore "physically unmeaningful". Presumably, one should have a formalism that allows you to add odd parameters to your superalgebras at will, without carrying all possible extensions around with you all the time.

I hope these examples convey the flavor of what I'm seeking: some method for considering flexible or extendable objects that doesn't require the consideration of all possible extensions all the time.

Answer 1

I don't know enough about (1) or (3) to address them confidently, although I suspect that, as you suggested, some kind of internal type theory will do the trick. (Maybe ask a separate question about each of them, with more details provided?)

For (2), I believe one sort of partial answer, at least, is contained in my paper Exact completions and small sheaves, specifically section 9 and more specifically 9.6-9.10. The idea is that we can give a direct description of "the category of small sheaves on a large site" that doesn't require consideration of "large sheaves" at all. There are several ways to give such a description, which are discussed in the paper in the more general context of a non-inaccessible cardinality bound (in which case it also includes "exact completion"). But in general, the objects of the category (the "small sheaves") are a sort of many-object internal equivalence relation in the site, i.e. a small family of representables "formally glued together".

Lemma 9.1 and Theorem 9.2 show that if we do consider the very-large category of large sheaves, then the category of small sheaves is equivalent to its full subcategory consisting of the objects that are small colimits of sheafified representables, or equivalently are the left Kan extension of a sheaf on some small full subcategory of the site. Thus, for instance, the category of condensed sets is the category of small sheaves on the site of profinite spaces. On the other hand, if the topology is trivial, we obtain the better-known category of small presheaves mentioned in the question. There is thus a sheafification functor from small presheaves to small sheaves --- although there is not in general a right adjoint to it, i.e. the underlying presheaf of a small sheaf may not be a small presheaf.

The category of small sheaves is not in general a topos (neither Grothendieck nor elementary), but it is the next best thing: a locally small infinitary-pretopos, i.e. a category satisfying all the exactness conditions of Giraud's theorem but not the existence of a small generating set. Thus it lacks "higher-order" structure like exponential objects, power objects, and universes, but it has all the same "first-order" structure as an ordinary topos of sheaves; this seems to me a reasonable way to make sense of your idea of "operations that preserve a sense of smallness".

This is fairly specific to the case (2) of sheaves. But it does relate in some way to my guess at the probable answer of (1) and (3). Namely, any object of any category determines its representable functor, and if the category is large, the representable functor will take a proper class of possible inputs --- but in most cases, the object of the category can be described by a small amount of data. Thus, if we have a "large function" of some sort, we can try to view it as the representable functor of an object of some category, for which we can give a more direct "small" presentation. Type-theoretic internal languages can be viewed as a way of working conveniently with representable functors or generalized elements (the type-theoretic "context" being the domain of a generalized element).

Answer 2

For (2), Colin McLarty has written papers about using higher order arithmetic as a foundation for Grothendieck-style constructions. His "The large structures of Grothendieck founded on finite order arithmetic" [arXiv link] is the primary reference here, but see also "A univalent universe in finite order arithmetic" [arXiv link].

This is similar to the approach mentioned in Alec Rhea's answer, but using arithmetic as the base rather than set theory. In either approach, you start with type $0$ objects—integers or sets—and build upward from there to have one type for every $n \in \mathbb N$, with type $n+1$ objects being more-or-less collections of type $n$ objects. Higher-order set theory is overkill in terms of consistency strength for a lot of results, as McLarty's work shows. But depending on what you're doing it may be more convenient to work in the stronger setting.

Answer 3

I am not familiar with (1) and only have passing familiarity with superalgebra, but for (2) you may find the foundation laid out in my paper An axiomatic approach to higher order set theory satisfying.

Working in this theory we have countably many levels of 'largeness' for 'collections', with sets as $0$-collections, classes as $1$-collections, so on and so forth.

This foundation was originally developed to handle things like topology/analysis/measure theory etc. over the surreals; they form a proper class so a topology on the surreals would be a collection of proper classes, etc., and working in this foundation we can collect that stuff up no problem without relying on things like Scott's trick.

In this context, the isomorphism class you want to consider is a proper $1$-collection assuming you want the fpqc topology on all set-sized affine schemes -- more generally, the isomorphism classes for the fpqc topology on affine schemes whose underlying rings are all $n$-collections will be proper $n+1$-collections, and we can collect these up no problemo.

This foundation also makes explicit the notion of "small vs. large-ness" at the axiomatic level, allowing us to collect up all $n$-collections satisfying some predicate as an $n+1$-collection which sometimes also forms an $n$-collection if replacement applies.

Answer 4

Concerning (1): In 2020 Alex Simpson gave a talk on synthetic probability theory: https://youtu.be/XtsBsLM9ofk where he provides foundations of probability theory in which random variables are treated as a primitive notion. I assume that there's no difficulty in adding new random variables in this setting. But I haven't found any publication of his on this yet.