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 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 sheaves 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.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014
    • (edited Jun 16th 2015)

    In the cohesive topos of sheaves on topological manifolds (or cartesian spaces), we’ve decided now that the Dedekind real number object RR is the sheaf of continous real-valued functions. Moreover, we know that in this case the shape modality ʃʃ is internal nullification of RR, i.e. external localization at all pullbacks of the map R1R\to 1.

    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 \sharp: internally localize at the map ΔR\Delta \mathbb{R} \to R, where Δ\Delta is the “discrete objects” left adjoint to the global sections functor. Externally, this localizes also at projections X×ΔX×RX\times \Delta \mathbb{R} \to X\times R, so that by iteration we also localize at Δ nR n\Delta \mathbb{R}^n \to R^n, which should be enough to be codiscrete. Does that seem right?

    Moreover, Δ\Delta \mathbb{R} 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”.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)

    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

    {R n*} n \left\{ R^n \to \ast \right\}_{n \in \mathbb{N}}

    and that \sharp is localization at the small set of maps

    {R nR n} n \left\{ \flat R^n \to R^n \right\}_{n \in \mathbb{N}}

    i.e. (I suppose)

    {R Cauchy nR Dedekind n} n \left\{ R^n_{Cauchy} \to R^n_{Dedekind} \right\}_{n \in \mathbb{N}}

    That is at least what gives ʃʃ and \sharp in the model on TopMfdTopMfd.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)

    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 R smoothR_{\mathrm{smooth}} is a ring object such that the quotient by the square-0 neighbourhood of its diagonal is a maximal proper subobject of R DedekindR_{\mathrm{Dedekind}}

    {(x,y)R smooth 2|(xy) 2=0} R smooth ʃ infR smooth R Dedekind \array{ \{(x,y) \in R_{\mathrm{smooth}}^2 | (x-y)^2 = 0\} \\ \downarrow \downarrow \\ R_{\mathrm{smooth}} \\ \downarrow \\ ʃ_{inf} R_{\mathrm{smooth}} &\hookrightarrow& R_{\mathrm{Dedekind}} }

    Here I say “proper subobject” to rule out the case that one takes R smoothR DedekindR_{\mathrm{smooth}} \coloneqq R_{\mathrm{Dedekind}} 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 ʃ infR smoothʃ_{inf} R_{\mathrm{smooth}} exhausts what is smooth inside R DedekindR_{\mathrm{Dedekind}}.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014

    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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)

    Sure, it would already be interesting in itself.

    A trivial but maybe suggestive followup-comment to the above:

    what I denoted ʃ infR smoothʃ_{inf} R_{\mathrm{smooth}} 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 R Cauchy=R DedekindR_{\mathrm{Cauchy}} = \flat R_{\mathrm{Dedekind}};

    then the reals with their topological strcuture R DedekindR_{\mathrm{Dedekind}};

    then the reals with their smooth structure ʃ infR smoothʃ_{inf} R_{\mathrm{smooth}};

    then finally the reals with their SDG structure R smoothR_{\mathrm{smooth}}

    The first step is via the \flat-counit, the second is some inclusion that presently I don’t know how to abstractly characterize, and the third is via the ʃ infʃ_{inf}-unit:

    R DedekindR Dedekindʃ infR smoothR smooth \flat R_{\mathrm{Dedekind}} \longrightarrow R_{\mathrm{Dedekind}} \hookleftarrow ʃ_{inf} R_{\mathrm{smooth}} \longleftarrow R_{\mathrm{smooth}}
    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014

    Is ʃ infR smooth&#643;_{inf} R_{\mathrm{smooth}} really a maximal proper subobject of R DedekindR_{\mathrm{Dedekind}}? 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 C kC^k functions for 1k<1\le k\lt \infty?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014

    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.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)

    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 C ()C 0()C^\infty(-) \hookrightarrow C^0(-). 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 R smoothR_{smooth} such that the induced infinitesimal shape has the required properties.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014

    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 R smoothR_{smooth} satisfies the KL axioms. But that doesn’t make any reference to the map to R DedekindR_{Dedekind}. It seems like there should be a canonical such map. Let’s see, theorem 11.2.14 of the HoTT book says that R DedekindR_{Dedekind} is the terminal Archimedean ordered field. So if R smoothR_{smooth} is an Archimedean ordered local ring, then its residue field should be an Archimedean ordered field and hence sit inside R DedekindR_{Dedekind}. 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 1D1\to D as DD ranges over infinitesimal objects? You mentioned only products XX×DX\to X\times D, 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 1N1\to N, where NR smoothN\subset R_{smooth} is the set of all nilpotents, since every 1D1\to D 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.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014

    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 R smoothR_{smooth} or of ʃ infR smooth&#643;_{inf} R_{smooth}, 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?

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)

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

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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. x𝔪n(x n=0)\forall x\in \mathfrak{m} \exists n ( x^n = 0) but not nx𝔪(x n=0)\exists n \forall x\in \mathfrak{m} (x^n = 0). Isn’t this the way R smoothR_{smooth} behaves internally?

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 6th 2014

    I guess you want a local ring RR with the maximal ideal equal to the nilradical of RR. I can’t find anything useful with a quick google search.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    the codiscretes should be the ones that think every smooth real is a Cauchy real. Right?

    Yes.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    What about a “local Jacobson ring”?

    • CommentRowNumber16.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 6th 2014

    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.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    Some further replies, catching up with the above:

    Do you use “smooth real” to mean an element of R smoothR_{smooth} or of ʃ infR smooth&#643;_{inf} R_{smooth}, 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 ʃ infR smooth&#643;_{inf} R_{smooth}, despite the symbols, is the more classical object, while R smoothR_{smooth} 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.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    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 infR smooth\int_{inf} R_{smooth} of the constructed R DedekindR_{Dedekind}.

    Is there no conceivable way to actually construct R smoothR_{smooth} or infR smooth\int_{inf} R_{smooth} internally? Based on R DedekindR_{Dedekind}?

    One should try something like to define what it means to take a “difference quotient” of a term in R DedekindR_{Dedekind} 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?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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 R DedekindR_{Dedekind}. I’m doubtful that it will work because we would hope that “the smooth reals” in Sh(X)Sh(X) for XX a smooth manifold would be the sheaf of smooth real-valued functions on XX, but as I said above, a given space XX 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 Aʃ infAA \to &#643;_{inf} A to not be surjective for some object AA?

    • CommentRowNumber20.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 6th 2014

    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…

    • CommentRowNumber21.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeNov 6th 2014
    • (edited Nov 9th 2014)

    Just a short remark on the question how a local ring with 𝔪=(0)\mathfrak{m} = \sqrt{(0)} can be called: Such a thing is precisely a local ring of Krull dimension zero.

    If we interpret “𝔪=(0)\mathfrak{m} = \sqrt{(0)}” 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”.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    @Ingo thanks. In what sense can 𝔪=(0)\mathfrak{m} = \sqrt{(0)} 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.

    • CommentRowNumber23.
    • CommentAuthorThomas Holder
    • CommentTimeNov 6th 2014

    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!

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    @Thomas: added where?

    • CommentRowNumber25.
    • CommentAuthorThomas Holder
    • CommentTimeNov 6th 2014

    Added at real numbers object, sorry.

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    Wow, thanks, that is a great paper. If only I could read French better. We should start by translating it.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    I am not sure what it would really mean to put a smooth structure on R DedekidR_{Dedekid} internally. But I am thinking that:

    1. externally there is only one smooth structure on \mathbb{R}, up to equivalence;

    2. 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?

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    @Urs, the point is that a smooth structure in Sh(X)Sh(X) corresponds externally to a smooth structure on XX, not \mathbb{R}. (And actually, don’t I remember that there is in fact more than one smooth structure on \mathbb{R}? E.g. you can compose the “usual” one with xx 3x\mapsto x^3. The resulting manifolds are diffeomorphic, of course, but the diffeomorphism is not the identity, so as maximal atlases on a fixed copy of \mathbb{R} they are distinct.)

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    Hm, given that we don’t presently seem to know how to internally put smooth structure on R DedekindR_{Dedekind} 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! :-)

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    I think we can distinguish them internally; they’re just two different subsheafs of R DedekindR_{Dedekind} in Sh()Sh(\mathbb{R}).

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

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

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    [editing now…]

    • CommentRowNumber34.
    • CommentAuthorZhen Lin
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    Well, since the slice Sh(T) /\mathbf{Sh}(\mathbf{T})_{/ \mathbb{R}} is “like” Sh()\mathbf{Sh} (\mathbb{R}), 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 C C^\infty-algebra structures on the Dedekind reals.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    I don’t think we can expect the Dedekind reals to have a C C^\infty-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 R DedekindR_{Dedekind}?

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    On the other hand, looking only at the slice over R DedekindR_{Dedekind} will only give us a smooth structure on \mathbb{R}, whereas we want a smooth structure “on” the whole big topos.

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    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.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    Is his definition of smooth structure just a complicated way of saying it’s an equivalence class of the relation \simeq?

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    Yes, I’d read it as saying that SS is the result of picking a base point and translating it around via “standard functions”.

    • CommentRowNumber40.
    • CommentAuthorZhen Lin
    • CommentTimeNov 6th 2014

    I don’t think we can expect the Dedekind reals to have a C C^\infty-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 C C^\infty-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 R DedekindR_{Dedekind}?

    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 T\mathbf{T} is locally connected), it should be the case that a morphism R D nR DR_D^n \to R_D in Sh(T)\mathbf{Sh} (\mathbf{T}) is standard if and only if for every object XX in T\mathbf{T}, the corresponding morphism T(X, n)T(X,)\mathbf{T}(X, \mathbb{R}^n) \to \mathbf{T}(X, \mathbb{R}) 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 R DedekindR_{Dedekind} will only give us a smooth structure on \mathbb{R}, whereas we want a smooth structure “on” the whole big topos.

    Right. But come to think of it, does having a smooth structure on R DR_D help us recover R smoothR_{smooth}?

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    I am confused by why Fourman defines his equivalence relation using two standard C C^\infty functions f,gf,g 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?

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    why the presheaf of coordinate functions is a sheaf

    I suppose to UXU \subset X it assigns the set of maps UXU \to X 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.

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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?

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    Yes, he means in the internal logic. This becomes more clear in his remark 4.2, and its reference to theorem, 3.8.

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    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!)

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    More explicitly, I could have two functions f:Uf:U\to \mathbb{R} and g:Vg:V\to \mathbb{R} which agree on UVU\cap V and which are individually diffeos onto their image, but such that the glued function UVU\cup V\to \mathbb{R} is not injective; we might have f(x)=g(y)f(x) = g(y) for some xUVx\in U\setminus V and yVUy\in V\setminus U. Maybe what he means is the sheaf of functions that are locally diffeos onto their images?

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    Oh, yes, coordonnées locales is local coordinates, he must mean locally diffeos, true.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    Okay, so suppose h:Uh:U \to \mathbb{R} is locally a diffeo onto its image, and k:Uk:U\to \mathbb{R} is a continuous map such that there exist smooth functions f,g:f,g:\mathbb{R}\to \mathbb{R} such that fh=kf \circ h = k and gk=hg \circ k = h. Why is kk locally a diffeo onto its image?

    • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014
    • (edited Nov 6th 2014)

    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 SS to be the subobject of smooth standard translates (where smooth standard back-translate exists) of 0 D n0 \in \mathbb{R}^n_D. Then the smooth reals would in turn be the image of that in D\mathbb{R}_D under further smooth standard functions.

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    Sorry, have to go offline right now. Seem to be in trouble already…

    • CommentRowNumber51.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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!

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    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.

    • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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 rsr \simeq s is an equivalence relation, we can associate to each global section of R in Top(X)Top(X) 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 x 3x^3 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?)

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    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.

    • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    I think “la droite R” means the standard external real line, now used as the topological space XX

    • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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 Sh(X)Sh(X) is way more general than XX being a manifold. Is it more closely related to any other notion of generalized smooth space?

    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2014

    “la droite” is “the right” one. The real Reals :-)

    • CommentRowNumber58.
    • CommentAuthorMike Shulman
    • CommentTimeNov 6th 2014

    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.

    • CommentRowNumber59.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 6th 2014

    Une droite is just an abbreviation for une ligne droite, what you might find in a French geometry book.

    • CommentRowNumber60.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 7th 2014

    @Mike

    Something like the dual to a smooth structure being determined by curves? Perhaps ’functional’ is the word you are looking for?

    • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2014

    Une droite is just an abbreviation for une ligne droite,

    Oh, so I was wrong.

    • CommentRowNumber62.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2014

    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 q=0q = 0 for instance in Wikipedia’s entry.

    But maybe that’s not what you are after now.

    • CommentRowNumber63.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2014
    • (edited Nov 7th 2014)

    Just for my own sake, record of the key conceptual idea of Fourman:

    the strategy is that

    1. we do know what the internally smooth functions D n D 1\mathbb{R}_D^n \to \mathbb{R}_D^1 are;

    2. so if we could identify D n\mathbb{R}_D^n with charts in the site, then we’d be done;

    3. so therefore the attempt to define a smooth structure as something that gives more control over D n\mathbb{R}_D^n.

    Maybe that makes us want to consider building an internal site CartSp internal={ D n} nCartSp_{internal} = \{\mathbb{R}^n_D\}_{n \in \mathbb{N}}, then consider the internal smooth set-topos and then try to escape from it again?

    • CommentRowNumber64.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2014

    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.

    • CommentRowNumber65.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2014

    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 D\mathbb{R}_D 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 D n\mathbb{R}_D^n?

    • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2014

    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 R CR DR_C \to R_D)? That’s a stronger condition than thinking every smooth real is a Cauchy real (localization at pullbacks of R CR SR_C \to R_S), so these types will be a subtopos of the codiscretes; but the codiscretes are equivalent to Gpd\infty Gpd, which has no nontrivial proper subtoposes.

    • CommentRowNumber67.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2014
    • (edited Nov 7th 2014)

    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 X infXX \to \int_{inf}X.

    Now infR DR D\int_{inf} R_D \simeq R_D. I need to think more about how to say the above paragraph in terms of R DR_D. 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.

    • CommentRowNumber68.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2014

    Mmm, I guess that makes sense, if R DR_D and R CR_C are both coreduced, then nullifying the fibers of R CR DR_C \to R_D won’t be enough to tell you about the images of infinitesimals. How about a model like Sh(SmMfd)Sh(SmMfd) where there are no infinitesimals, though; is it true in that case?

  1. @Mike 22: Sorry, yes. I meant “invertible or nilpotent” instead of “invertible or zero”.

    • CommentRowNumber70.
    • CommentAuthorUrs
    • CommentTimeNov 9th 2014
    • (edited Nov 9th 2014)

    re #66, #68

    So ΓR DΓR SΓR C=\Gamma R_D \simeq \Gamma R_S \simeq \Gamma R_C = \mathbb{R}. Hence codiscrete objects are local with respect to (R SR D)(R_S \to R_D).

    Maybe I misunderstood you. What I worried about above is that the codiscretes are the localization at R CR DR_C \to R_D, in general.

    • CommentRowNumber71.
    • CommentAuthorMike Shulman
    • CommentTimeNov 10th 2014

    No, that makes sense.