What are external sets, internally?

[dwarn]

At various points, we would like to quantify internally not over all types, but over "locally locally constant sheaves" (?). For example, naively we would say a general (not necessarily quasi-compact) open proposition is one of the form $\exists (i : I), f(i) \ne 0$, where $I$ is some type and $f : I \to R$. But if we allow all types, then every proposition $P$ is open (take $I = P$ and $f$ constantly $1$). Instead we restrict to finite types.

But how about the following more general notion. (I think we discussed something like this at SAG 2 with @iblech.) We define what it means for a (0-truncated) type $I$ to be external. It is a general fact that $I$ is the filtered colimit of $[n]$ over all $n : \mathbb N$ and maps $[n] \to I$. Say $I$ is external if this colimit is preserved by the functor $(-)^X$ for every affine scheme $X$. I think this means that any map $X \to I$ factors through $[n]$ for some $[n]$, and that two maps $X \to [n] \to I$ and $X \to [m] \to I$ are equal only if there is a common co-refinement $X \to [k] \to I$ (via maps $[n] \to [k]$, $[m] \to [k]$ making everything commute). For example $\mathbb N$ (by boundedness) and any finite set should be external.

I don't know if this is exactly the right definition. But my question is: can we use some definition like this to go beyond finiteness restrictions in SAG, to define general opens and perhaps general schemes (not necessarily finitely presented)?

[iblech]

First thoughts:

1. I like this proposed definition!
2. Your definition would not generalize to sites which have non-finite coverings. For instance we don't have boundedness in toposes over such sites. But this need not block us. In all the sites we study (Zariski, and perhaps etale, fppf, ...), all coverings are finite.

Let me also, just for reference, share other proposed conditions I know of:

• A set I is external iff for every f.p. R-algebra A, the canonical map Hom(Spec(A), I_discrete) → I^Sp(A) is bijective, where Spec(A) is the pointfree spectrum of A, I_discrete is I regarded as a discrete pointfree space and Sp(A) is the usual SAG-spectrum.
• A set I is external iff the free module R⟨I⟩ is strongly quasicoherent.

[xuanruiqi]

Sorry if this is a silly question - what is the intuition for "external"?

[dwarn]

Not a silly question! The idea is that, in the intended semantics, any set determines a sheaf on the big Zariski topos, the "constant sheaf", i.e. sheafification of the constant presheaf. These are the sheaves which deserve to be called "external" (more precisely, if we try to define an internal property, it has to respect the topology, so we can only hope to describe sheaves that Zariski-locally are constant), and they look very different from most sheaves of interest. The question is if we can do anything meaningful with this. I mostly wanted to record the question (which is not new, but I'm not sure it was recorded before).