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 71 of 71
In the cohesive topos of sheaves on topological manifolds (or cartesian spaces), we’ve decided now that the Dedekind real number object is the sheaf of continous real-valued functions. Moreover, we know that in this case the shape modality is internal nullification of , i.e. external localization at all pullbacks of the map .
I have been wondering whether we can construct other parts of cohesion internally like this. Here’s a guess at how to construct the codiscrete reflection : internally localize at the map , where is the “discrete objects” left adjoint to the global sections functor. Externally, this localizes also at projections , so that by iteration we also localize at , which should be enough to be codiscrete. Does that seem right?
Moreover, also has an internal description in this topos: it’s the set of Cauchy real numbers. (This should be true in any locally connected topos, by the argument of D4.7.12(a).) So internally, the codiscrete objects would be “the types that believe every Dedekind real is a Cauchy real”.
That’s a good point, thanks.
I think we might also forget about the product maps and just say that is localization at the small set of maps
and that is localization at the small set of maps
i.e. (I suppose)
That is at least what gives and in the model on .
For this to be interesting, we really need to bring in the smooth reals internally. Maybe one should say something like this:
a smooth real line is a ring object such that the quotient by the square-0 neighbourhood of its diagonal is a maximal proper subobject of
Here I say “proper subobject” to rule out the case that one takes which has no square-0 elements and hence would fit that definition. And I say “maximal” to rule out other trivial choices. Maybe instead of “maximal” one could add other conditions that ensure that exhausts what is smooth inside .
Well, I think the purely topological case is already “interesting”. (-: Although I would also like to bring in the smooth reals; I need to think more about your proposal.
Sure, it would already be interesting in itself.
A trivial but maybe suggestive followup-comment to the above:
what I denoted is really the “traditional smooth reals”, namely the real line with its smooth structure but without any infinitesimal neighbourhoods of classical points.
From this perpective the situation maybe harmonizes rather well with the historical development:
first we have the reals with just their discrete geometric structure ;
then the reals with their topological strcuture ;
then the reals with their smooth structure ;
then finally the reals with their SDG structure
The first step is via the -counit, the second is some inclusion that presently I don’t know how to abstractly characterize, and the third is via the -unit:
Is really a maximal proper subobject of ? The former is the sheaf of smooth real-valued functions and the latter the sheaf of continuous real-valued functions, right? Shouldn’t there be plenty of other proper subobjects in between, like functions for ?
It would be really nice if there were some internal topos-theoretic way to define what “a smooth real number” is. But that seems unlikely, I guess.
I meant maximal subject to the condition of being the quotient by nilpotents, i.e. maximal subject to the condition of having smooth structure, thinking of the inclusion . But this was just a rough idea and won’t work without fine tuning.
Maybe one needs no maximality principle at all, maybe one should allow exotic cases. What really matters of course is whether there is a condition on such that the induced infinitesimal shape has the required properties.
Oh, ok.
I also realized there can’t be a purely topos-theoretic way to define “smooth real number” because one topos (e.g a topological space) could have multiple different “smooth structures”.
One obvious condition would be that satisfies the KL axioms. But that doesn’t make any reference to the map to . It seems like there should be a canonical such map. Let’s see, theorem 11.2.14 of the HoTT book says that is the terminal Archimedean ordered field. So if is an Archimedean ordered local ring, then its residue field should be an Archimedean ordered field and hence sit inside . Does that work?
Also, about the infinitesimal shape, did I get correctly from your response here that we can regard it as localization at the class of pullbacks of the point-inclusions as ranges over infinitesimal objects? You mentioned only products , but since it’s a left-exact localization, the inverted morphisms should be stable under pullback. And then we could simplify further by just saying pullbacks of , where is the set of all nilpotents, since every is a pullback of that. Then it would have the nice internal description of saying that the coreduced types are “the ones that think 0 is the only nilpotent”, analogously to how the codiscretes are the ones that think every Dedekind real is a Cauchy real.
Oh, since we’re in the smooth context now, the codiscretes should be the ones that think every smooth real is a Cauchy real. Right?
Do you use “smooth real” to mean an element of or of , and in either case what do you call an element of the other one?
Is there a standard name for a local ring whose maximal ideal consists of (all) nilpotents?
Interesting points, but no time here, therefore just telegraphically on “Is there a standard name for…” yes: “local Artin ring”. In SDG they also say “Weil algebra” for this (while elsewhere this means something else).
Hmm, in an Artin ring the maximal ideal is itself nilpotent, so there is a finite upper bound on the nilpotency of its elements. I was thinking of where every element of the maximal ideal is nilpotent, but there could be elements of arbitrarily high nilpotency, i.e. but not . Isn’t this the way behaves internally?
I guess you want a local ring with the maximal ideal equal to the nilradical of . I can’t find anything useful with a quick google search.
the codiscretes should be the ones that think every smooth real is a Cauchy real. Right?
Yes.
What about a “local Jacobson ring”?
Ah, that looks ok. So the logic is: the nilradical is the intersection of all prime ideals, and in a Jacobson ring each prime ideal is the intersection of all maximal ideas containing it - but there is only one maximal ideal, so it is prime, and so the nilradical is equal to this maximal ideal. Excellent.
Some further replies, catching up with the above:
Do you use “smooth real” to mean an element of or of , and in either case what do you call an element of the other one?
I don’t have a convention even just with myself on this. But my suggestion in #5 was that , despite the symbols, is the more classical object, while is what only a small circle of people knows about, so that maybe the former should get a more traditional name like “smooth real line”.
Then it would have the nice internal description of saying that the coreduced types are “the ones that think 0 is the only nilpotent”, analogously to how the codiscretes are the ones that think every Dedekind real is a Cauchy real.
Yes.
This thread is titled “internal definition of cohesion”. Wouldn’t it more properly be called “constructive definition of cohesion”?
Because, also the definition via axiomatizing the existence of the modalities, that we used to discuss previously, is internal. The difference is rather that here the idea is to not just postulate the modalities, but to actually construct them. Right? (or in jargon, I suppose: “To make them compute.”)
This has a chance to work for topological cohesion. For smooth cohesion we seem to be back to postulating. The improvement is (or might be) that we are not postulating smooth shape directly, but are postulating a subtype of the constructed .
Is there no conceivable way to actually construct or internally? Based on ?
One should try something like to define what it means to take a “difference quotient” of a term in and then take its subtype of terms for which the limit of the difference quotients exists. This is just a vague idea. Could something like this work?
Perhaps “internal construction of cohesion” would be closer to what I meant: not to postulate the cohesive structure, but to define/construct it internally.
It’s certainly tempting to try to define smooth reals internally from . I’m doubtful that it will work because we would hope that “the smooth reals” in for a smooth manifold would be the sheaf of smooth real-valued functions on , but as I said above, a given space can have multiple smooth structures. Put differently, smoothness of a space seems irreducibly to be extra structure rather than a mere property, so internally the same is probably true of the real numbers: we have to choose a “notion of smoothness” before we can say what a smooth real number is. But we can hope to define what a “notion of smoothness” is.
A question: is it possible (in models) for the map to not be surjective for some object ?
Would a choice of smooth reals, if such a thing could be specified, determine the smooth structure? Then perhaps manifolds with only one smooth structure (2-dimensional ones, for instance) would have up to iso just one “smooth reals object” in their sheaf topos…
Just a short remark on the question how a local ring with can be called: Such a thing is precisely a local ring of Krull dimension zero.
If we interpret “” as “any element is invertible or zero”, the equivalence even holds constructively (using the definition of Krull dimension as in this paper, Thm. 1.2(5), page 3).
Edit: I mean “invertible or nilpotent” instead of “invertible or zero”.
@Ingo thanks. In what sense can be interpreted as “any element is invertible or zero”? Do you mean “any element is invertible or nilpotent”?
@David: well, it maybe depends on what you/we mean by “smooth structure”… (-: but I think probably yes, since externally a smooth manifold structure on a space is determined by its sheaf of smooth real-valued functions.
I’ve added a reference to a paper of Fourman that presumably discusses smooth structure on the reals. Hopefully the reading repays the trouble I had digging that out with the reference in the elephant wrong and only the complete proceedings accessible on numdam!
@Thomas: added where?
Added at real numbers object, sorry.
Wow, thanks, that is a great paper. If only I could read French better. We should start by translating it.
I am not sure what it would really mean to put a smooth structure on internally. But I am thinking that:
externally there is only one smooth structure on , up to equivalence;
internally it would be nice to have any one construction. If there is more than one construction, all the better, but here it seems the key bonus would be to have any one construction at all.
No?
@Urs, the point is that a smooth structure in corresponds externally to a smooth structure on , not . (And actually, don’t I remember that there is in fact more than one smooth structure on ? E.g. you can compose the “usual” one with . The resulting manifolds are diffeomorphic, of course, but the diffeomorphism is not the identity, so as maximal atlases on a fixed copy of they are distinct.)
Hm, given that we don’t presently seem to know how to internally put smooth structure on such that it corresponds externally to what one would think it is, I don’t see on which basis any such conclusion would be possible. Also I don’t think we’ll be wanting or even be able to distinguish diffeomorphic smooth reals.
But I’ll better read Fourman 75 now to maybe get an idea of what’s actually going on! :-)
I think we can distinguish them internally; they’re just two different subsheafs of in .
I’ll go and translate Fourman into an entry smooth structure on a topos.
But his definition 4.1 of a smooth structure again does not seem to give the construction of a subobject of the Dedekind reals, but just the characterization of those that would qualify. (Not unexpectedly maybe, just saying.)
Right; he’s defining a set of smooth reals, not the set of smooth reals.
Thanks for the translation effort! Once we understand what he’s doing, the next step will be to modify it into something that applies to a big topos rather than a little one. A quick glance suggested to me that his definition involves fixing a natural number (the “dimension” of the smooth structure), which wouldn’t really make sense for a big topos; but maybe we can do it locally somehow.
[editing now…]
Well, since the slice is “like” , perhaps one should think about smooth structures on the slice over the Dedekind reals?
One thing I can’t help but wonder about is the connection between Fourman’s definition and -algebra structures on the Dedekind reals.
I don’t think we can expect the Dedekind reals to have a -algebra structure, since in models they are the sheaf of continuous real-valued functions; we seem to have to restrict to a smaller object of reals. Looking at the slice over them is a good thought, though; I had been thinking instead of looking at “all” slices, but that’s a problem since not every object can be expected to be finite-dimensional. So what does Fourman’s definition give us, in the case of dimension 1, when interpreted in the slice over ?
On the other hand, looking only at the slice over will only give us a smooth structure on , whereas we want a smooth structure “on” the whole big topos.
typed a bit at smooth structure on a topos. Didn’t get to the meat of it yet, but have to make a telephone call now.
Is his definition of smooth structure just a complicated way of saying it’s an equivalence class of the relation ?
Yes, I’d read it as saying that is the result of picking a base point and translating it around via “standard functions”.
I don’t think we can expect the Dedekind reals to have a -algebra structure, since in models they are the sheaf of continuous real-valued functions; we seem to have to restrict to a smaller object of reals.
Actually, the ring of continuous real-valued functions on a topological has a canonical -algebra structure, because smooth functions are in particular continuous. But it’s not so clear how useful that is.
Looking at the slice over them is a good thought, though; I had been thinking instead of looking at “all” slices, but that’s a problem since not every object can be expected to be finite-dimensional. So what does Fourman’s definition give us, in the case of dimension 1, when interpreted in the slice over ?
First we need to understand what “standard functions” are. Hopefully in the situations of interest “Brouwer’s theorem” applies so that the continuity condition is trivial. Because the direct image of local geometric morphisms preserve both Dedekind and Cauchy real numbers (and assuming every object in is locally connected), it should be the case that a morphism in is standard if and only if for every object in , the corresponding morphism sends locally constant functions to locally constant functions.
What’s not so obvious to me is the definition of “smooth standard function”.
On the other hand, looking only at the slice over will only give us a smooth structure on , whereas we want a smooth structure “on” the whole big topos.
Right. But come to think of it, does having a smooth structure on help us recover ?
I am confused by why Fourman defines his equivalence relation using two standard functions without requiring them to be inverses of each other. In particular, I don’t immediately see why the sheaf of coordinate functions is closed under his equivalence relation. In fact, I don’t even see why the presheaf of coordinate functions is a sheaf; mightn’t gluing two coordinate patches produce a non-injective function?
why the presheaf of coordinate functions is a sheaf
I suppose to it assigns the set of maps that are diffeos onto their image. Restricting such is still a diffeo onto its image and the sheaf condition is just gluing of these functions.
By the way, that equivalence relation is, as Zhen Lin highlights, by “smooth standard functions”. I didn’t have the “smooth” qualifier in a version of the entry a few minutes back.
I’m not worrying about restricting but about gluing.
Fourman doesn’t define “smooth standard function”, does he? I assume that he means a standard function which is moreover smooth in the internal logic?
Yes, he means in the internal logic. This becomes more clear in his remark 4.2, and its reference to theorem, 3.8.
I know you mean the sheaf condition, but I thought you must be thinking of a different presheaf. How is the gluing not the obvious gluing of functions? (Maybe its me who is thinking of the wrong presheaf!)
More explicitly, I could have two functions and which agree on and which are individually diffeos onto their image, but such that the glued function is not injective; we might have for some and . Maybe what he means is the sheaf of functions that are locally diffeos onto their images?
Oh, yes, coordonnées locales is local coordinates, he must mean locally diffeos, true.
Okay, so suppose is locally a diffeo onto its image, and is a continuous map such that there exist smooth functions such that and . Why is locally a diffeo onto its image?
I have added the to the entry the actual definition of the smooth reals.
I am wondering (might be really missing something, though): doesn’t that give a construction after all: may we not define to be the subobject of smooth standard translates (where smooth standard back-translate exists) of . Then the smooth reals would in turn be the image of that in under further smooth standard functions.
Sorry, have to go offline right now. Seem to be in trouble already…
Re #49, that does seem to satisfy Fourman’s definition, but it’s totally not what we want in the models, because the constant function at 0 is not locally a diffeo onto its image!
Ah right, if we take the translates of a constant we’ll probably get the Cauchy reals as the smooth reals, corresponding to the discrete smooth structure.
I need help with Fourman’s Example 4.3(2) which seems to be relevant to this question. With some help from Google translate I get
Since is an equivalence relation, we can associate to each global section of R in a smooth structure. If X is the right R, a and b give us different smooth structures on T but the associated smooth topoi are equivalent. They correspond to R with its usual differential structure. Section c gives us a smooth topos not equivalent to the corresponding structure induced smooth paper [??]
I guess he’s referring to the functions a,b,c that he’s drawn at the bottom of the page. I can see that a and b are like the example that I mentioned before: they give different smooth structures that are diffeomorphic by a nonidentity diffeomorphism. But what does he mean re: section c by ’la structure lisse induite du papier”?
(Also, how should “la droite R” be translated?)
I was wondering,too, I guess he means the smooth structure induced by regaring the figure on the bottom right as being the depicted embedding of the real line into the plane, as induced by its drawing on the paper.
I think “la droite R” means the standard external real line, now used as the topological space
I think “la droite R” means the standard external real line, now used as the topological space X
That was my guess too, but I don’t know how “droite” means that.
I guess he means the smooth structure induced by regaring the figure on the bottom right as being the depicted embedding of the real line into the plane, as induced by its drawing on the paper.
Okay. So his notion of “smooth structure” on is way more general than being a manifold. Is it more closely related to any other notion of generalized smooth space?
“la droite” is “the right” one. The real Reals :-)
Isn’t there a notion of generalized smooth space that’s determined by a sheaf of smooth real-valued functions on the space? I thought there was but I can’t find it.
Une droite is just an abbreviation for une ligne droite, what you might find in a French geometry book.
@Mike
Something like the dual to a smooth structure being determined by curves? Perhaps ’functional’ is the word you are looking for?
Une droite is just an abbreviation for une ligne droite,
Oh, so I was wrong.
Isn’t there a notion of generalized smooth space that’s determined by a sheaf of smooth real-valued functions on the space? I thought there was but I can’t find it.
So there is of course the definition of a smooth manifold in the fashion of locally ringed spaces, with the sheaf of smooth real valued functions as the structure sheaf. Are you thinking of that?
That is the definition most commonly used in the context of supermanifolds, as it goes, which subsumes the ordinary case. Take for instance in Wikipedia’s entry.
But maybe that’s not what you are after now.
Just for my own sake, record of the key conceptual idea of Fourman:
the strategy is that
we do know what the internally smooth functions are;
so if we could identify with charts in the site, then we’d be done;
so therefore the attempt to define a smooth structure as something that gives more control over .
Maybe that makes us want to consider building an internal site , then consider the internal smooth set-topos and then try to escape from it again?
Does Fourman make any use of non-smooth standard functions? If not, then we could simplify the nlab entry by omitting the continuity hypothesis and only defining the smooth ones.
I wonder whether we should consider a more general notion that Fourman’s: just define a set of smooth reals to be a subset of that’s closed under the action of smooth standard functions. That would apply easily to the big-topos case, and also to infinite-dimensional cases etc., and it would include the “maximal case” where we declare all continuous functions to be “smooth”. Does he get anything concrete from assuming that the smooth reals are determined by some equivalence class of elements of ?
Oh, and going back to #14, shouldn’t the codiscretes also be the types that think every Dedekind real is a Cauchy real (i.e. localization at all pullbacks of )? That’s a stronger condition than thinking every smooth real is a Cauchy real (localization at pullbacks of ), so these types will be a subtopos of the codiscretes; but the codiscretes are equivalent to , which has no nontrivial proper subtoposes.
re #66
In the models I know of the codiscretes are the reduced objects that think every smooth real is Cauchy. And the reduced objects are those that think every infinitesimal disk is a point. And the infinitesimal disks are the fibers of .
Now . I need to think more about how to say the above paragraph in terms of . But it would seem to me one needs more than what you just suggested.
I am in a rush once more here, hope to find time to think about this with more leisure later today.
Mmm, I guess that makes sense, if and are both coreduced, then nullifying the fibers of won’t be enough to tell you about the images of infinitesimals. How about a model like where there are no infinitesimals, though; is it true in that case?
@Mike 22: Sorry, yes. I meant “invertible or nilpotent” instead of “invertible or zero”.
re #66, #68
So . Hence codiscrete objects are local with respect to .
Maybe I misunderstood you. What I worried about above is that the codiscretes are the localization at , in general.
No, that makes sense.
1 to 71 of 71