# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 25th 2020
• (edited Mar 29th 2020)

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.

• CommentRowNumber2.
• CommentAuthorDavidRoberts
• CommentTimeMar 26th 2020

Every tried working with the category of smooth manifolds? Not even a $\Pi W$-pretopos.

• CommentRowNumber3.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 26th 2020

Re #2: But the category of sheaves of sets on smooth manifolds is a topos.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeMar 26th 2020

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.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeMar 26th 2020

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.

• CommentRowNumber6.
• CommentAuthorDavidRoberts
• CommentTimeMar 27th 2020

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.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeMar 27th 2020
• (edited Mar 27th 2020)

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?

• CommentRowNumber8.
• CommentAuthorTobyBartels
• CommentTimeMar 27th 2020

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.

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeMar 27th 2020

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.

• CommentRowNumber10.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 27th 2020
• (edited Mar 27th 2020)

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.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeMar 27th 2020

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.

• CommentRowNumber12.
• CommentAuthoratmacen
• CommentTimeMar 27th 2020

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?

• CommentRowNumber13.
• CommentAuthorDavidRoberts
• CommentTimeMar 28th 2020

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.

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeMar 28th 2020

@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.

• CommentRowNumber15.
• CommentAuthorDavidRoberts
• CommentTimeMar 28th 2020

@Mike, sure, but Dmitri also asked about the failure of internal homs to exist.

• CommentRowNumber16.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 29th 2020

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.

• CommentRowNumber17.
• CommentAuthorDavidRoberts
• CommentTimeMar 29th 2020
• (edited Mar 29th 2020)

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?

• CommentRowNumber18.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 29th 2020

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.

• CommentRowNumber19.
• CommentAuthorDavidRoberts
• CommentTimeMar 29th 2020

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.

• CommentRowNumber20.
• CommentAuthorDavidRoberts
• CommentTimeApr 1st 2020

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.

• CommentRowNumber21.
• CommentAuthorTobyBartels
• CommentTimeApr 7th 2020

@Mike #11:

I don't think that it's fair to say that most people doing predicative mathematics assume function sets. Many constructive mathematicians do weakly predicative mathematics, which allows functions sets (but no set of truth values, hence no power sets). But there are also mathematicians doing predicative mathematics with classical logic, so they cannot have function sets either. I would even guess that the latter group is larger, but I might be wrong about that. (And then there is also mathematics using neither excluded middle nor function sets, like Giovanni Sambin's formal topology).

• CommentRowNumber22.
• CommentAuthorTobyBartels
• CommentTimeApr 7th 2020

@Dmitri #9:

OK, so you want a body of predicative mathematics and a doctrine of categories, such that this body of mathematics can be interpreted in this doctrine, and you want the doctrine to include many categories of interest to geometry, such that interpreting this body of mathematics within these categories gives results interesting to geometers. And of course you want this doctrine to be substantially more general than toposes, suitable to the corresponding body of mathematics, so that this isn't simply a restriction of how we can interpret impredicative choice-free constructive mathematics in toposes. Then I can't help you.

I can only say that I think that such a body of mathematics ought to be developed, and I developed some of it for my PhD. The doctrine that I have in mind here is the doctrine of sites. (In my PhD thesis, I actually used sites with a subcanonical singleton pretopology, but the ideas ought to generalize.) But I never developed it further. David may have developed some more. This doctrine is something like the doctrine of locally cartesian categories (but $C^\infty$ is not one so I could not use that). Of course, this is much weaker than $\Pi$-$W$-pretoposes.

• CommentRowNumber23.
• CommentAuthorDavidRoberts
• CommentTimeApr 7th 2020

Subcanonical superextensive sites are indeed, IMHO, a very natural “geometric” (not in the technical sense) setting, whereby one has covers (think: display maps) that are quotients, but also disjoint sums (and the coverage is generated from these two). I’m not sure what Toby means by ’develop’, but certainly I feel I have reasonable intuition how to work in such a setting synthetically. I’m happy to have function spaces that are “proper classes” (in the setting of manifolds: infinite-dimensional), where one is more constrained with what is possible. But that said, working with a reasonable class of inf. dim. manifolds with the correct definitions of various things isn’t too much different, it can just be harder to verify conditions of said definitions. In this case, one might lose function spaces, depending on how general things are. This is familiar from class-set theory, where class functions aren’t gathered into a single object.

I’ve always meant to think a bit harder about what the ’correct’ morphisms between such sites should be, but haven’t.

I should add that Mike’s work on exact completions is totally relevant here, and probably more the sort of thing Toby was envisaging.

• CommentRowNumber24.
• CommentAuthorDavidRoberts
• CommentTimeDec 5th 2020

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

For what it’s worth, Scholze, in a guest post on Kevin Buzzard’s blog, now open states that condensed sets form a locally cartesian closed category.