Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 20 of 20
The category of sheaves of sets on a topological space is a topos that need not satisfy the law of excluded middle or the axiom of choice.
Doing mathematics in the topos of sheaves of sets on a topological space amounts to doing mathematics in continuous families over this topological space. Likewise, doing mathematics in the topos of G-sets amounts to doing mathematics G-equivariantly.
Many geometers do not care about logic, but they do care about doing mathematics in families or G-equivariantly. Thus, such a hypothetical geometer would still care about constructive mathematics.
Furthermore, the failure of the law of excluded middle and the axiom of choice admits really simple geometric explanations: the union of an open set and the interior of its complement need not be equal to the entire space; not every surjective etale map has a continuous section.
Suppose now that this hypothetical geometer encounters predicative mathematics. Is there an easy geometric way to convince him that he should care about predicative mathematics?
For instance, is there a geometric construction that naturally produces a ΠW-pretopos that is not a topos?
Is there an easy geometric way to see how the existence of powerobjects can fail in this construction?
If geometric examples for ΠW-pretoposes are unavailable, I would also be interested in geometric examples for pretoposes together with a simple geometric explanation for the nonexistence of (local) internal homs.
Every tried working with the category of smooth manifolds? Not even a $\Pi W$-pretopos.
Re #2: But the category of sheaves of sets on smooth manifolds is a topos.
Yes, I agree with Dmitri: there’s a big gap between impredicative toposes, on the one hand, and categories with much weaker internal logics, on the other. In a topos you can do “all of mathematics, as long as it’s constructive”. In a category that’s not even LCC, you have to be very careful about what you can and can’t say. Predicative constructive mathematics is, like impredicative constructive mathematics, a context in which you can claim to do “all of mathematics”, but categories whose internal logic is this and no more are thin on the ground.
Perhaps the most general categorical construction I know of for producing $\Pi W$-pretoposes that are not toposes is exact completion. The ex/lex completion of a topos is not always a topos, but it is always a $\Pi W$-pretopos. However, I don’t really know of any geometric motivation for such things.
Ok, here’s a less snide example: class-set theory like MK or NBG. You don’t have many internal homs and no power-objects. And a model of algebraic set theory in general can be even worse, with no EM or AC.
David, Dmitri is asking the following question:
Consider the perspective on toposes as categories of generalized geometric spaces, as a topic in geometry. From that perspective what, if any, is the relevance of $\Pi W$-pretoposes?
Re being careful what you can say in Mike's #4:
Roughly speaking, constructive mathematics uses the same language as classical mathematics but proves fewer theorems in that language, while predicative mathematics uses a less expressive language to begin with. For example, in constructive mathematics, you cannot prove that a power set is a Boolean algebra; but in predicative mathematics, you cannot even talk about power sets in the first place!
I don't see how to make this precise. In constructive mathematics, you cannot talk about the Boolean algebra $\mathcal{P}\mathbb{N}$, although you can talk about the Heyting algebra $\mathcal{P}\mathbb{N}$ (and then fail to prove that it's Boolean). Conversely, although you can't talk about $\mathcal{P}\mathbb{N}$ directly in predicative mathematics, you could still talk about a hypothetical set $P$ (and binary relation $\epsilon$ from $\mathbb{N}$ to $P$) such that each subset of $\mathbb{N}$ is the preimage (under $\epsilon$) of a unique element of $P$ (and then fail to prove that any such $P$ exists). You could even prove that any such $P$ is a Heyting algebra (and a Boolean algebra if your logic is classical). But intuitively, it seems that $\mathcal{P}\mathbb{N}$ in constructive mathematics is something that is simply lacking some of its classical properties, while this $P$ in predicative mathematics is a phantom.
Re David #2 and Dmitri #3:
David's answer may have been snide, but it has value, and Dmitri's response is inadequate. For any example of a geometrically interesting non-topos category $C$, one could reply that the category of sheaves on $C$ is a topos. But if you're doing mathematics within $C$, then you're not doing it in $Sh(C)$, and you're not doing general constructive mathematics (since $C$ is not a topos). David and I have both had cause to try to do mathematics within the category $C^\infty$ of smooth manifolds, and this was necessarily both predicative and constructive. (Indeed, since $C^\infty$ is not even a pretopos, we had even more restrictions than that.) But of course we were doing geometry.
Re #9, #2: As far as I am aware, there is no paper that explicitly states the internal logic of smooth manifolds, nor there are any papers that would prove theorems using this logic.
My question, on the other hand, is concerned with practical matters. There is a large body of literature that proves theorems constructively, and instantiating these theorems in some topos immediately gives relevant geometric results. For example, instantiating constructive theorems about dualizable vector spaces yields theorems about finite-dimensional vector bundles.
There is also a sizable body of literature (not as large) that proves theorems predicatively. The question is whether one could instantiate these theorems in some topos-like construction and obtain some relevant geometric results.
While the points made above may be formally valid to some extent, they are not relevant to this question, which is concerned with (re)using a large body of existing knowledge.
The point I was trying to make in #4 is that while there are plenty of categories that are not toposes in which a geometer (or set theorist, as in #6) might want to work internally, I can’t think of any of them that are $\Pi$-pretopoi. Of course “predicative mathematics” is an umbrella term including everything that is not impredicative, hence also including these categories with very impoverished internal logics (not intended as a perjorative word, merely descriptive), but usually people who claim to be doing predicative mathematics do assume that they have function-sets and quotients, and Dmitri specifically asked about $\Pi W$-pretopoi.
Is there something like a “prequasitopos” or “quasipretopos” which intuitively has both the “quasi” and “pre” restrictions (on the logic)? So a general one is neither a pretopos nor a quasitopos, but it has everything (or many things) that the two have in common. So, for example, I guess it should have finite colimits. I’m thinking of models of extensional type theory without either impredicativity or exactness. Are such categories significantly more common?
Alright, here’s another attempt: the Stacks Project insists on working purely with ZFC, no universes. As a result every site must be small. However, I suspect that if instead of working with all sheaves on a site, small sheaves on a large site were used, then one could get away with using the base site of all affine schemes and still get all the schemes and algebraic spaces and algebraic stacks etc that one wanted. So the internal logic in the Stacks project might implicitly be that of a category of small sheaves. I don’t know if small sheaves on $Aff$ form a pretopos, but it seems reasonable. If one wants to say “well, but I could use a universe”, then number theorists and algebraic geometers really care about not having their theorems about concrete arithmetic objects rely on axioms additional to ZFC. They will say (like Brian Conrad) “it’s ok, I’ve thought about it, and no proofs for concrete objects use universes”. But this analysis should be done properly, and not on a case-by-case basis. And my feeling is that using a pretopos of small sheaves is a/one good way to approach it.
@David: A pretopos of small sheaves is also not LCC.
@Matt: I don’t think I’ve seen such a definition written down, but it certainly could be. But I can’t think offhand of any examples that aren’t quasitopoi.
@Mike, sure, but Dmitri also asked about the failure of internal homs to exist.
I clarified my question to also ask about pretoposes, in case ΠW-pretoposes prove to be too difficult.
Re #13: Barwick and Haine already identified what the resulting category of sheaves is (in practical example, such as affine schemes): it is a macrotopos. See Section 1.4 of their paper “Pyknotic objects I”.
A macrotopos is, in particular, a filtered colimit of toposes under fully faithful left exact left adjoints, so in that sense it does have powerobjects and internal homs.
Dmitri #16
a filtered colimit of toposes under fully faithful left exact left adjoints, so in that sense it does have powerobjects and internal homs.
so something like Theorem 3 in this?
Re 17: Yes, if your result is applicable, then it would show that macrotoposes are cocomplete elementary toposes.
Which means that we still do not have a geometric example of a ΠW-pretopos that is not a topos.
I’m not sure this is always true, though. To borrow some jargon, there are plenty of pretame class forcing models that only give $ZF^-$, not $ZF(C)$. I’m willing to bet that such class forcing notions fall under the scope of macrotoposes.
Scholze seems to be confirming that condensed sets only form a pretopos, as the putative subobject classifier is not a small sheaf. I’m probing to see if it locally cartesian closed (it is cartesian closed, he says, and well-powered), and Scholze thinks it might satisfy WISC. This might allow us to show all $W$-types exist, using recent work of Andrew Swan.
1 to 20 of 20