Not signed in (Sign In)

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

  • 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 beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive constructive-mathematics cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics planar 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 string string-theory subobject 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 25th 2020
    • (edited 6 days ago)

    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 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 Π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
    • CommentTime7 days ago

    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
    • CommentTime7 days ago

    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
    • CommentTime7 days ago

    @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
    • CommentTime6 days ago

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

    • CommentRowNumber16.
    • CommentAuthorDmitri Pavlov
    • CommentTime6 days ago

    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
    • CommentTime6 days ago
    • (edited 6 days ago)

    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
    • CommentTime6 days ago

    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
    • CommentTime5 days ago

    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
    • CommentTime2 days ago

    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.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)