Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 26th 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 ΠW\Pi W-pretopos.

    • CommentRowNumber3.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 27th 2020

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

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 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 27th 2020

    Perhaps the most general categorical construction I know of for producing ΠW\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 ΠW\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 ΠW\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 PP (and binary relation ε\epsilon from \mathbb{N} to PP) such that each subset of \mathbb{N} is the preimage (under ε\epsilon) of a unique element of PP (and then fail to prove that any such PP exists). You could even prove that any such PP 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 PP 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 CC, one could reply that the category of sheaves on CC is a topos. But if you're doing mathematics within CC, then you're not doing it in Sh(C)Sh(C), and you're not doing general constructive mathematics (since CC is not a topos). David and I have both had cause to try to do mathematics within the category C C^\infty of smooth manifolds, and this was necessarily both predicative and constructive. (Indeed, since C 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 ΠW\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 AffAff 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 29th 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 ZF^-, not ZF(C)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 WW-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 C^\infty is not one so I could not use that). Of course, this is much weaker than Π\Pi-WW-pretoposes.

    • CommentRowNumber23.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 8th 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 6th 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.