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

Discussion Tag Cloud

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.
    • CommentAuthorUrs
    • CommentTimeOct 25th 2014
    • (edited Nov 16th 2014)

    For XX a manifold of dimension nn, there is a canonical map τ X:XBGL(n)\tau_X \colon X \longrightarrow \mathbf{B}\mathrm{GL}(n) to the moduli stack of the smooth general linear group, modulating the bundle to which the tangent bundle is associated.

    I would like to formulate this construction axiomatically in differential cohesion.

    It is clear to me how the formalization ought to proceed, but there are some gaps where I know what to do “informally”, but not yet how to do it fully axiomatically.

    Here is how I imagine to start:

    First, we fix some types that are to play the role of the local model spaces. One option is to ask for a type 𝔸 1\mathbb{A}^1 that exhibits the cohesion in that the shape modality is 𝔸 1\mathbb{A}^1-localization. Then take the nn-dimensional model space to be 𝔸 n(𝔸 1) × n\mathbb{A}^n \coloneqq (\mathbb{A}^1)^{\times_n}.

    Then an nn-dimensional manifold is a type XX such that there exists a morphism (the atlas)

    i𝔸 nX \coprod_i \mathbb{A}^n \longrightarrow X

    which is 1) a 1-epimorphism and 2) is formally étale in that it is modal for the infinitsimal shape modality Π inf\Pi_{inf}.

    Next we need to axiomatize the group GL(n)\mathrm{GL}(n). In the standard model of differential cohesion this group is the following:

    First, the formal disk D nD^n around the origin in 𝔸 n\mathbb{A}^n is the homotopy fiber of the unit 𝔸 nΠ inf(𝔸 n)\mathbb{A}^n \longrightarrow \Pi_{inf}(\mathbb{A}^n) of the infinitesimal shape modality

    D nfib(𝔸 n𝔸 n) D^n \coloneqq \mathrm{fib}(\mathbb{A}^n \longrightarrow \mathbb{A}^n)

    Then, GL(n)\mathrm{GL}(n) is just the automorphism group of that:

    GL(n)Aut(D n). \mathrm{GL}(n) \coloneqq \mathbf{Aut}(D^n) \,.

    To produce the canonical morphism

    XBGL(n) X \longrightarrow \mathbf{B} \mathrm{GL}(n)

    we should proceed by producing a canonical morphism from the Cech nerve of 𝔸 nX\coprod\mathbb{A}^n\to X to the Cech nerve of *BGL(n)\ast \to \mathbf{B}\mathrm{GL}(n), hence a map of simplicial types that starts out looking like this:

    ( i𝔸 n)×X( i𝔸 n) (τ X) 1 GL(n) i𝔸 n * \array{ \vdots && \vdots \\ \downarrow \downarrow \downarrow && \downarrow \downarrow \downarrow \\ (\coprod_i \mathbb{A}^n) \underset{X}{\times} (\coprod_i \mathbb{A}^n) &\stackrel{(\tau_X)_1}{\longrightarrow}& \mathrm{GL}(n) \\ \downarrow\downarrow && \downarrow\downarrow \\ \coprod_i \mathbb{A}^n &\longrightarrow& \ast }

    This is where I am presently stuck. I know how to proceed rigorously, but not how to proceed fully formally, if you see what I mean.

    Rigorously, what I am supposed to say is that (τ X) 1(\tau_X)_1 is the map which to a point

    x^:*( i𝔸 n)×X( i𝔸 n) \hat x \;\colon\; \ast \longrightarrow (\coprod_i \mathbb{A}^n) \underset{X}{\times} (\coprod_i \mathbb{A}^n)

    assigns the element in GL(n)\mathrm{GL}(n) obtained by first forming the formal disk D X^ nD^n_{\hat X} around that point, as above, and then using the induced diagram

    D x^ n i 1 i 2 𝔸 n 𝔸 n X \array{ && D^n_{\hat x} \\ & {}^{\mathllap{i_1}}\swarrow && \searrow^{\mathrlap{i_2}} \\ \mathbb{A}^n && && \mathbb{A}^n \\ & \searrow && \swarrow \\ && X }

    together with the fact that all maps here are formally étale to form something that one would denote

    (i 1 1)i 2Aut(D x^ n)GL(n). (i_1^{-1}) \circ i_2 \in \mathbf{Aut}(D^n_{\hat x}) \simeq \mathrm{GL}(n) \,.

    where “i 1 1i_1^{-1}” means the inverse of the corestriction of p 1p_1 onto its image, and where some kind of rigid translation 𝔸 n𝔸 n\mathbb{A}^n \stackrel{\simeq}{\longrightarrow} \mathbb{A}^n making the base points coincide is implicit.

    But here I am a little stuck with the formalization. How would one formalize this “obvious” construction of (τ X) (\tau_X)_\bullet?

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 26th 2014
    • (edited Oct 26th 2014)

    Random thoughts:

    The first thing that comes to mind is some sort of canonical ’difference’ map, as one has in the case of a GG-torsor PP: P×PGP\times P \to G.

    I would expand out your diamond-shaped diagram to a pentagon, with the top span being replaced by 𝔸 nD L nD R n𝔸 n\mathbb{A}^n \leftarrow D^n_L \stackrel{\simeq}{\to} D^n_R \to \mathbb{A}^n, where the isomorphism is what you want to assign to x^\hat{x}. I don’t see why you can a priori identify the two formal discs, one in each copy of 𝔸 n\mathbb{A}^n.

    Actually, if you take the formal discs D L nD^n_L and D R nD^n_R in the left and right 𝔸 n\mathbb{A}^n respectively, and the formal disc D x^ nD^n_\hat{x} in XX around the image of x^\hat{x}, we should have isomorphisms D L nD x^ nD R nD^n_L \stackrel{\simeq}{\to} D^n_\hat{x} \stackrel{\simeq}{\leftarrow} D^n_R, using Π inf\Pi_{inf} or similar, so getting the isomorphism you want.

    Does this work?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2014
    • (edited Oct 26th 2014)

    Thanks! Yes, that should be the right idea.

    I was just thinking something similar. So it follows from the definition of formal disks as the pullback of the Π inf\Pi_{inf}-unit along the inclusion of points that:

    Fact. If Π inf(X)\Pi_{inf}(X) is 0-truncated, then the pullback of the inclusion of a formal disk into XX along that of another formal disk is either empty (if the basepoints don’t match) or is an equivalence (if they do).

    (Π inf(X)\Pi_{inf}(X) being 0-truncated says that XX looks like a “derived 0-truncated space” or “L L_\infty-algebroid”, with all stacky morphisms being infinitesimal).

    Let’s write FormalDisks()FormalDisks(-) for the fiber product of the Π inf\Pi_{inf}-unit with the \flat-counit composed with the Π inf\Pi_{inf}-unit. This is the disjoint union of formal disks around all global points.

    The above fact implies for 0-truncated XX that when on top of the fiber product of 𝔸 nX\coprod \mathbb{A}^n \to X with itself we consider the fiber product – let’s call it QQ – of

    FormalDisks(𝔸 n)𝔸 nX FormalDisks(\coprod \mathbb{A}^n) \hookrightarrow \coprod \mathbb{A}^n \to X

    with itself, then we get maps

    Q ι 1 q ι 2 FormalDisks(𝔸 n) (𝔸 n)×X(𝔸 n) FormalDisks(𝔸 n) \array{ && Q \\ & {}^{\mathllap{\iota_1}} \swarrow &\downarrow^{\mathrlap{q}}& \searrow^{\mathrlap{\iota_2}} \\ FormalDisks(\coprod \mathbb{A}^n) && (\coprod \mathbb{A}^n) \underset{X}{\times} (\coprod \mathbb{A}^n) && FormalDisks(\coprod \mathbb{A}^n) }

    with the following property: over each point yy of (𝔸 n)×X(𝔸 n)(\coprod \mathbb{A}^n) \underset{X}{\times} (\coprod \mathbb{A}^n) the preimage D y nD^n_y under qq is the formal disk around that point and under ι 1\iota_1 and ι 2\iota_2 this is identified in two different ways with the corresponding formal disk D x nD_x^n in XX. Composition gives an equivalence (D x nD x n)Aut(D n)GL(n)(D^n_x \simeq D^n_x) \in \mathbf{Aut}(D^n) \simeq \mathrm{GL}(n).

    Now I suppose we will have to assume that 𝔸 n\mathbb{A}^n is concrete. If that is the case, then functions out of (𝔸 n)×X(𝔸 n)(\coprod \mathbb{A}^n) \underset{X}{\times} (\coprod \mathbb{A}^n) are fixed by what they do on all global points. This we know by the above construction. So all that remains then is to argue that the above construction indeed gives a function on global points that descends to a smooth function. Still need to think about this. (And need to streamline the above idea.)

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 26th 2014

    Yeah, I was wondering how this works with generalised points: I can’t think how one would do that just now.

    • CommentRowNumber5.
    • CommentAuthorTim_Porter
    • CommentTimeOct 26th 2014

    Could someone put a new entry on ‘modulating stack’. I was wanting to check up on this and could not find it, yet there are plenty of uses of it.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2014

    @David, I’d be content to have the construction just for concrete objects. That is a very reasonable assumption in this context, anyway.

    But even in that case, the above argument gives me so far only a map

    (Σ)(BGL(n)). \flat(\Sigma) \longrightarrow \flat(\mathbf{B}\mathrm{GL}(n)) \,.

    One will still need to add an argument that the \flat-signs may be removed here.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2014

    @Tim:

    I have created modulating morphism with some discussion.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2014
    • (edited Oct 26th 2014)

    I should add the remark that the homotopy fibers of the Π inf\Pi_{inf}-unit may, in the models, be anything between the first-order infinitesimal neighbourhood of points, to second-, third-order, etc. to actually being formal (unbounded order). Only in the case that it is first order is my notation GL(n)GL(n) above justified. Generally what the above construction gives (or ought to give) is not the tangent bundle, but it’s nnth order jet bundle.

    One should ultimately consider a hierarchy of Π inf\Pi_{inf}-modalities (and its adjoints), one for each order of infinitesimality, and a limiting one for formal geometry.

    • CommentRowNumber9.
    • CommentAuthorTim_Porter
    • CommentTimeOct 26th 2014
    • (edited Oct 26th 2014)

    @Urs #7. Thanks. Sometimes I get confused when terms that are current in physics infiltrate mathematics. An instance of this is the use of gauge group for something that had an honest mathematical name beforehand. I am not against names such as this being used but they all too often are introduced without the necessary underpinning of intuition and motivation for that word being used. (and I still do not know why ‘gauge’ was used.)

    (Edit: It reads nicely and clears things up for me, so again thanks.)

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2014
    • (edited Oct 26th 2014)

    @Tim: this is hardly used in physics. But maybe we should move further discussion of this issue, if necessary, to a dedicated thread.

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 26th 2014

    Hmm, would we likely be able to get D-modules this way? That would excite some people, I’m sure.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2014
    • (edited Oct 26th 2014)

    Yes, D-modules on XX are quasicoherent sheaves on the de Rham stack Π inf(X)\Pi_{inf}(X) of XX (e.g. Lurie, above theorem 0.4) and that’s just what the infinitesimal shape modality gives.

    (Remarks to this extent are around 3.10.2 in dcct, but I haven’t really done much with it yet.)

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 27th 2014

    Ah, yes, thanks.

    Regarding the map in, #6, out of (Σ)\flat(\Sigma), how does one recognise maps out of (X)\flat(X) that factor through (X)X\flat(X) \to X? But (X)X\flat(X) \to X almost always fails to be an epimorphism, is that not right?

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    Sorry for asking a very elementary question, but why do you consider atlases only consisting of copies of 𝔸 n\mathbb{A}^n rather than “open subsets” of the same?

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    @David: yes, but between concrete objects (e.g. sheaves which are diffeomological spaces), functions are fixed on what they do on the global points. The maps between concrete spaces are a subset of the maps on global points. So in principle we could assume concreteness, build a map on global points, and then show that it is in this subset. But I don’t presently see how to complete this strategy, so it may be a dead-end. (Also the map I wrote in #6 should be replaced by the map on global points of the double intersection to GL(n)\mathrm{GL}(n)).

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    Also I do not understand the point of modulating morphism. It seems to be saying that while the classifying space BO(n)B O(n) classifies O(n)O(n)-principal bundles, the classifying stack BO(n)\mathbf{B} O(n) classifies bundles with extra structure. Why can’t we just say that? Why is there a need for a new word “modulating” instead of “classifying” for something that is classified by a stack rather than a space?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    And while I haven’t digested most of this discussion, in general my intuition is that when you have some construction that works on global points and you want it to work more generally, what you should do is phrase that construction in the internal logic. Does that not work here?

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    @Mike, yes, one could consider much more general local model spaces. I was just sticking to some simple choice for definiteness. For all purposes of the present discussion (at least as far as we got), I could just take any set {U i} i\{U_i\}_i of model spaces instead of writing {𝔸 n} n\{\mathbb{A}^n\}_n.

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014

    re #16: I like the word “modulating” and Tim asked me to explain it, so that’s what I did. As far as I know this is actually the origin of the word “moduli” and so it makes sense. But I won’t insist on anyone using it.

    re #17: so how would it work?

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    But is there some reason you prefer to say “modulating” rather than “classifying”?

    I can’t tell you how it would work, since I haven’t understood your argument yet! I’m just suggesting an idea that you might try.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014

    is there some reason you prefer to say “modulating” rather than “classifying”?

    You are right that when I am talking to people and in a context where higher toposes need no further comment, then taking the point of view that BG\mathbf{B}G classifies bundle with structure would be just excellent. But when I am speaking in a less idealistic context of the map that classifies a bundle, everyone will think of maps to the classifying space BGB G. When I say “modulating” then my hope was (but Tim sort of killed that hope) that people would think “ah, he probably is talking about the map to the moduli stack now” :-) Probably just me being very naive.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    (By the way, where is the internal incarnation of the infinitesimal modalities recorded? We have two coreflective subcategories and a reflective subcategory, but there is some interaction among them, and they also have to interact with the ordinary cohesive modalities.)

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    Well, I wouldn’t have known what you meant either. (-: And you did say in the same sentence “to the moduli stack” so I don’t see how “classifying” could have been misunderstood.

    • CommentRowNumber24.
    • CommentAuthorTim_Porter
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    Note: Modulate from a Google search means:

    ‘ 1. exert a modifying or controlling influence on.

    "the state attempts to modulate private business's cash flow"
    
    synonyms:   regulate, adjust, set, attune, balance, harmonize, temper, modify, moderate
    
    "the cells modulate the body's immune response"
    
    2.
    vary the strength, tone, or pitch of (one's voice).
    
    "we all modulate our voice by hearing it"
    
    synonyms:   adjust, change the tone of, vary, inflect
    
    "she modulated her voice so as to speak more gently"
    
        alter the amplitude or frequency of (an electromagnetic wave or other oscillation) in accordance with the variations of a second signal, typically one of a lower frequency.
    
        "radio waves are modulated to carry the analogue information of the voice"
    
        Music
        change from one key to another.
    
        "the first half of the melody, modulating from E minor to G"
    
        change from one form or condition into (another).
    
        "the fraught silence would modulate into conciliatory monosyllables"
    

    (Origin

    mid 16th century (in the sense ‘intone a song’): from Latin modulat- ‘measured, made melody’, from the verb modulari, from modulus ‘measure’ (see modulus).)


    These do not necessarily give the right intuition to the word, ’modulating’ as it suggests some form of variation or change to me. This does not really matter as a definition is given, but perhaps some addition thought needs to be put into whether some other term might not capture the intuition (which is an important one). The first meaning that Google gave may be the nearest and ’regulating’ might be a synonym.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    @Tim, do you think there’s a value in having a term other than “classifying” then?

    • CommentRowNumber26.
    • CommentAuthorTim_Porter
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    I am more worried about the choice of the term with regard to the intuition if engender, but oto answer your question, ’classifcation’ is a very very general term and so is difficult to make more precise e.g. by adding strong' oriso’ or something like that. ’Classifying space’ is now well understood as is ’classifying map’. The extra precision indicated by Urs may be very useful e.g. for me, using classifying stacks instead of classifying spaces in Turaev’s HQFTs may be something that would be nice to follow through, although it may already be subsummed under the more general theories already available. Just to say ’classifying’ may not be precise enough.

    (Perhaps we should shift this to another dedicated thread.???)

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    We should really move the discussion about modulating maps into another thread. The last thing that I will say here is to repeat the term “modulate” is not my invention, but that when one traces the origin of the word “moduli space” it appears that the intuition was that maps into it modulate bundles (of curves) in the way that in electronics a wave is modulated in time. I think that makes very good sense. But let’s further discuss it in another thread!

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    re #22

    (By the way, where is the internal incarnation of the infinitesimal modalities recorded? We have two coreflective subcategories and a reflective subcategory, but there is some interaction among them, and they also have to interact with the ordinary cohesive modalities.)

    I think the internal formulation of differential cohesion is a system of modalities of this form:

    id ʃ ʃ inf id inf * \array{ && && \Re &\subset & id \\ && && \bot && \bot \\ && ʃ & \subset & ʃ_{inf} & \subset & id \\ && \bot && \bot \\ \emptyset &\subset& \flat & \subset & \flat_{inf} \\ \bot & & \bot && \\ \ast & \subset& \sharp }

    Here the inclusion sign is to mean that the modal types for the modality on the left include into those for the modality on the right.

    This wasn’t well reflected on the nnLab. Until a minute ago the only place where this appeared on the nnLab was, hold your breath, the entry Science of Logic. Now I have also added it to differential cohesion in the section Definition (scroll down a bit).

    • CommentRowNumber29.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 27th 2014

    Re #8,

    One should ultimately consider a hierarchy of Π inf\Pi_{inf}-modalities (and its adjoints), one for each order of infinitesimality, and a limiting one for formal geometry.

    Does differential cohesion always come with such a hierarchy? There was the jet (infinity,1)-category hierarchy, but didn’t we have the codomain fibration H IH\mathbf{H}^I \to \mathbf{H}, not differentially cohesive?

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2014
    • (edited Oct 27th 2014)

    Yes, the Goodwillie tangent cohesion is “infinitesimal cohesion”. In good cases this is the “homotopy cofiber” of differential cohesion.

    The general situation is a fiber sequence of cohesive \infty-toposes of the form

    H reducedHH infinitesimal \mathbf{H}_{reduced} \hookrightarrow \mathbf{H} \longrightarrow \mathbf{H}_{infinitesimal}

    where the left inclusion exhibits differential cohesion on H\mathbf{H} and the rightmost item is infinitesimally cohesive (over the given base). (An example is here at differential cohesion and idelic structure ).

    Given the left inclusion H reducedH\mathbf{H}_{reduced} \hookrightarrow \mathbf{H} then H infinitesimal\mathbf{H}_{infinitesimal} follows. But given just H infinitesimal\mathbf{H}_{infinitesimal} (as is the case for Goodwillie tangents) I am not sure if there is a good canonical way to complete to a full sequence as above. But this is an interesting question to ask!

    • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 27th 2014

    Oh yes, I was wondering about such things back here, and two comments later thought I had an answer for the second jet for Grpd\infty Grpd.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2014

    Re #28 Thanks!

    So for the cohesive modalities, we have the adjunction ʃʃ \dashv \flat\dashv\sharp, where \sharp and ʃʃ are monadic modalities, the former left exact and the latter with stable units, and \flat is a comonadic modality (“comodality”?). Moreover, the ʃʃ-modal types are the same as the \flat-comodal ones, and the canonical functor from the \flat-comodal types to the \sharp-modal ones is an equivalence of categories.

    What additional properties like these characterize the infinitesimal modalities? Obviously ʃ infʃ_{inf} is a left exact modality, since it is a right adjoint. Do \Re and inf\flat_{inf} have any special properties qua comodalities, and how are the subcategories of (co)modal types related?

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2014
    • (edited Oct 28th 2014)

    Oh, I see. I regard all of this as implicit (apart from extra exactness of the outer left adjoints). Should have said so.

    So where I display

    LR L \dashv R

    with LL an idempotent monad, then I am always thinking (in the present context) of this as induced from an adjoint triple L˜iR˜\tilde L \dashv i \dashv \tilde R with fully faithful ii. So the modal types are the same.

    Conversely, when

    LR L \dashv R

    with LL an idempotent comonad, then I am always thinking of this as induced from an adjoint triple i Lpi Ri_L \dashv p \dashv i_R with i Li_L and i Ri_R fully faithful. And so the modal types are equivalent via the canonical map.

    That’s anyway what I want to mean when I draw

    id ʃ ʃ inf id inf * \array{ && && \Re &\subset & id \\ && && \bot && \bot \\ && ʃ & \subset & ʃ_{inf} & \subset & id \\ && \bot && \bot \\ \emptyset &\subset& \flat & \subset & \flat_{inf} \\ \bot & & \bot && \\ \ast & \subset& \sharp }

    The leftmost column indicates what are monads and what are comonads (and is otherwise a hat tip to two giants on whose shoulders we stand). The next two columns really stand for adjoint triples that are induced from adjoint quadruples. (And the rightmost column is just for fun.)

    That’s what I mean anyway. Should have said so. Maybe there should be some dedicated notation for adjoint pairs that come from adjoint triples. (BTW, is there a good way to characterize how much room there is for an adjoint idempotent modality not to come from an adjoint triple?)

    On the extra exactness properties of the leftmost adjoints I keep changing my mind.

    I used to say that \Re should preserve finite products. But when for some proposition I wanted it to preserve finite limits and since it did so in the models I had, I started to demand that. (Because this assumtion implies that all étale \infty-toposes over all objects in differential cohesion to have reduced-stucture-sheaves instead of unreduced-structure sheaf, which seems desireable, see this remark).

    These extra exactness properties bug me a bit. From the point of view of diagrams as above, they seem an odd add-on. Like an unrelated afterthought. I keep hoping that there’ll be some neat principle which would imply or at least make more natural that and how one would impose such extra conditions. (Well, of course full lect exactness is preferred from the internal point of view, so maybe the real oddity is just the shape modality…)

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2014

    Ok, thanks. Doesn’t \Re automatically preserve all limits since it is a coreflector? Do you mean instead to assume that the \Re-comodal types are closed under (finite) limits?

    • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 28th 2014

    Re #33, you once had a triple of co/monads in the right column (the ones just for fun). I managed to convince myself once that adding a lower modality on the left hand side, then the resulting 6 rows had something to do with the 6 co/monads resulting from the string of 7 adjunctions in the context of pointed objects (with all limits and colimits).

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2014
    • (edited Oct 28th 2014)

    @Mike, hm, so \Re is composition of a right adjoint followed by a fully faithful left adjoint. In the notation of this definition it is =i !i *\Re = i_! \circ i^\ast. (Sorry, we are maybe talking past each other, or maybe I am missing something.)

    @David, right, but in that comment which you point to, in the rightmost column I depict generic modalities, just indicating the pattern by which we might continue to the right. Here I am doing something which one might call “similarly, but oppositely, empty” by adding the identity modalities.

    But actually that makes some sense: the identity modalities represent the entire \infty-topos and the diagram we are looking at depicts, in particular and from left to right, an increasing filtration of that \infty-topos by full subcategories, starting from the smallest ones. So it sort of makes sense to display the full topos as its maximal subcategory on the right. While it carries no information, it makes for a bit of conceptional symmetry.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2014

    Ah, it’s a difference in what is meant by “limits”. The functor :H thIm(i !)\Re : \mathbf{H}_{th} \to Im(i_!) preserves limits since it is a right adjoint to the inclusion, which under the identification i !:HIm(i !)i_! : \mathbf{H} \simeq Im(i_!) just says that i *i^* preserves limits. But limits in the category Im(i !)Im(i_!) may not be the same as limits in H th\mathbf{H}_{th}, which is to say that i !i_! may not preserve limits. In fact, limits in Im(i !)Im(i_!) are computed by applying \Re to limits in H th\mathbf{H}_{th}. So saying that Im(i !)Im(i_!) is closed under limits is the same as saying that \Re takes limits in H th\mathbf{H}_{th} to limits in H th\mathbf{H}_{th} (rather than limits in Im(i !)Im(i_!), which it automatically does), which is I guess what you meant.

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2014

    I see, thanks. So then, as you just deduced, the answer to your #34 is that I used to think one should just demand that \Re-comodal types are closed under finite product but later thought one should rather demand them to be closed under all finite limits.

    Of course, as you know, one could consider any such condition and carefully keep track of which conclusions require which assumption. Somehow these exactness conditions are an add-on, which don’t so much get to the core of what (differential) cohesion is about. Not sure. I feel I may well be missing some important insight here.

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2014

    Yes, it’s a bit puzzling. I got a lot happier with the requirement that ʃ preserve finite products when we realized that it was equivalent to saying that it could be represented internally as a reflective subuniverse. I wonder whether something similar could be going on here.

    It’s a pity that differential cohesion has to introduce two new comodalities, when the one existing comodality \flat is the least satisfactorily internalized part of ordinary cohesion. Is it worth thinking about whether either of those have any better internalization? E.g. is there a natural “fiberwise” version of either \Re or inf\flat_{inf}?

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2014
    • (edited Oct 28th 2014)

    The infinitesimal shape ʃ infʃ_{inf} is certainly the workhorse of the three (as far as I have explored this).

    Moreover, in proofs I have been using the existence of \Re and inf\flat_{inf} mostly in the guise of ʃ infʃ_{inf} preserving all limits and colimits. Notably in the series of propositions that construct and characterize the étale \infty-toposes Et(X)Et(X) of any type XX in differential cohesion (here), this is used repeatedly in this form, and only in this form.

    On the other hand, for the discussion of those étale \infty-toposes, I really need to preserve all \infty-colimits, not just finite ones. Generally, these proofs make heavy use of “external” \infty-topos theory, so maybe they either all fail internally or need to be entirely reworked internally anyway.

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2014

    Does it help with the comodalities to assume an 𝔸 1\mathbb{A}^1-object such that the modality is localization at that object, as we discussed elsewhere?

    Because it certainly also makes sense for the infinitesimal shape modality, to assume that it is localization at an infinitesimal line.

    (As I mentioned elsewhere, in usual models one will want maybe a hierarchy of infinitesimal shape modalities, containing first order infinitesimals and all-order infinitesimals (i.e. “formal” elements) , but certainly just the case of first order infinitesimals is interesting enough in itself to deserve attention. )

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2014

    Regarding the rightmost “for fun” column above: in the HoTT book the identity mode in fact has a name, “purely”. Is there such a name for the *\ast-modality? (The one constant on the unit type.)

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2014

    Does it help with the comodalities to assume an 𝔸 1\mathbb{A}^1-object such that the modality is localization at that object, as we discussed elsewhere?

    I haven’t been able to think of a way in which it helps with the comodalities.

    Am I right that in the case X=1X=1, the right adjoint Et:(H th) /X(H th) /X fetEt:(H_{th})_{/X} \to (H_{th})^{fet}_{/X} becomes inf\flat_{inf}? If so, then the issue for internalizing inf\flat_{inf} is that EtEt doesn’t necessarily commute with pullback. I presume that it actually doesn’t?

    mostly in the guise of ʃ infʃ_{inf} preserving all limits and colimits

    Interesting. Does it also preserve all limits and colimits fiberwise? It probably won’t preserve “internal” or “indexed” limits and colimits, since that would imply that \Re and inf\flat_{inf} extend to indexed functors, but it might at least preserve fiberwise limits and colimits, and that (at least in the case of finite limits and colimits) could be formulated as an internal property. Of course, if you’re mainly using it as input to an adjoint functor theorem, then internalizing the finite case wouldn’t help. It would be nice to see how much of this theory could be done internally.

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeOct 29th 2014
    • (edited Oct 29th 2014)

    Am I right that in the case X=1X=1, the right adjoint Et:(H th) /X(H th) /X fetEt:(H_{th})_{/X} \to (H_{th})^{fet}_{/X} becomes inf\flat_{inf}?

    Yes. And the text should say so, as this is conceptually important. I have added a brief remark.

    (I thought I had added this somewhere before, but maybe I didn’t.(?))

    Which reminds me: there might be a better symbol for inf\flat_{inf}. Any suggestions? When I started to write \Re for the reduction modality (which not only matches well with the sound of Re-duction, but also with the idea that the reduced part is the “real” part, as in the established use of “body” (as opposed to “soul”) for the reduced part in supergeometry ) then I was naturally led to write \Im for inf\flat_{inf}, just for the symmetry of the symbols. But not sure.

    Does it also preserve all limits and colimits fiberwise?

    Fiberwise colimits, yes (by applying preservation of \infty-colimits under pullback to the pullback-characterization of the action of the modality on the slice.) For limits I may need to think, as limits in the slice are not reflected under dependent sum. (This seems the kind of question that you would answer in your sleep!)

    It would be nice to see how much of this theory could be done internally.

    Yes. I wish I had resources to look into it. The next best thing is hoping that some young energetic students find interest in this. Such as the topostheorist here maybe…

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeOct 29th 2014

    (Also, elsewhere I experimented with writing \oint for inf\int_{inf} or rather ʃ inf ʃ_{inf}. Not sure though.)

    • CommentRowNumber46.
    • CommentAuthorUrs
    • CommentTimeOct 29th 2014
    • (edited Oct 29th 2014)

    Regarding the comodalities: I suppose what you have in mind here is that the approach via sharp-externalization may seem less elegant than direct internal implementation? Is that what you mean?

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeOct 29th 2014

    Less elegant, but also more tedious to code.

    I don’t really like the subscripts “inf”, so it would be nice to find symbols that don’t require them. But I don’t really have a good enough feel yet for what those modalities mean to suggest anything.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeOct 29th 2014

    Fiberwise colimits, yes (by applying preservation of ∞\infty-colimits under pullback to the pullback-characterization of the action of the modality on the slice.) For limits I may need to think

    Oh, yes, a similar argument should work for limits: limits in the slice are the same as limits in the ambient category of the diagram with an added terminal object, so that latter limit is preserved by the global functor, then pullback preserves limits in the slices. Thanks.

    • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeOct 29th 2014
    • (edited Oct 29th 2014)

    Less elegant, but also more tedious to code.

    Regarding \flat: suppose we axiomatize ʃʃ via 𝔸 1\mathbb{A}^1-localization so that it has a direct axiomatization along with \sharp.

    Here a vague feeling, please bear with me:

    It seems that for types that we want to call X\flat X we have both “introduction rules” and “elimination rules”, because, by adjunction, we know how to map into X\flat X and how to map out of it.

    In other words, given modalities ʃʃ, \sharp, directly implemented, shouldn’t they elegantly be able to support/induce a comodality in between them?

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTimeOct 29th 2014

    That’s an interesting point; I wonder if there is something there. The problem actually starts with the formation rule, though, before we even get to intro and elim: we don’t have a map :TypeType\flat : Type\to Type (or equivalently a rule allowing us to deduce X:Type\flat X : Type from X:TypeX : Type) because \flat isn’t a pullback-stable operation on slice categories.

    • CommentRowNumber51.
    • CommentAuthorMike Shulman
    • CommentTimeOct 29th 2014

    I find it curious that ʃ infʃ_{inf} is so important, since the coreduced objects don’t seem to be the ones that I’m used to thinking about in SDG. But maybe that is the similar sort of thing to how we may be more familiar with discrete objects, but in ordinary cohesion it turns out that the codiscrete objects are very important.

    How do the notions of reduced/coreduced interact with “classical” SDG notions like microlinear space?

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeOct 30th 2014
    • (edited Oct 30th 2014)

    I have two aspects to offer in reply to this question.

    First, it is noteworthy that in classical SDG the infinitesimal objects such as D𝔸 1D \hookrightarrow \mathbb{A}^1 need the assumption of ring structure on 𝔸 1\mathbb{A}^1 for their definition and need an axiom (the KL-axiom) to ensure their intended behaviour. In differential cohesion neither of this appears, but it is ʃ infʃ_{inf} which does an analogous job: given any type XX and a point x:*Xx : \ast \to X, then the infinitesimal disk x:D xXx : D_x \hookrightarrow X in XX at that point is the homotopy fiber product D x*×ʃ infXD_x \simeq \ast \underset{ʃ_{inf}}{\times} X.

    (To see that this is the right characterization in the models, take a sheaf model on a site of classical SDG objects such as the site for the Cahiers topos. Test on objects on the form U×DU \times D with UU reduced. Use the fact that by adjunction Hom(U×D,ʃ infX)Hom(U,X)Hom(U \times D, ʃ_{inf} X) \simeq Hom(U,X) to find that a map U×DD xU \times D \to D_x is equivalently a map DXD \to X with the given basepoint.)

    So introducing ʃ infʃ_{inf} seems to me to be the answer to a question that is left curiously open in “Axiomatic Cohesion”, namely: suppose we want something like SDG, but suppose we want to fomulate it in terms of adjoint modalities, how would we have to adopt the axiomatics of SDG?

    Second, the use of synthetic infinitesimals in algebraic geometry, which inspied SDG back in the 60s, has much evolved since then, and one might ask SDG to go along with this evolution of its motivating example. Namely the modern way of talking about Grothendieck’s original ideas of infinitesimals, leading to crystalline cohomology, is D-geometry and in 𝒟\mathcal{D}-geometry, the central construction is that of the de Rham stack X dRX_{dR} of a scheme XX, and that it just what ʃ infʃ_{inf} produces: in standard models ʃ infX=X dRʃ_{inf} X = X_{dR}.

    • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2014

    Hmm. Far be it from me to criticize the modern way of doing anything, but how with this language do I do something simple like differentiate a function?

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeOct 30th 2014
    • (edited Oct 30th 2014)

    how with this language do I do something simple like differentiate a function?

    That was what my first item was meant to answer.

    Given a function f:XYf : X \to Y, and a point x:*Xx : \ast \to X, the derivative of ff at xx is its restriction to D x:=*×ʃ infXXD_x := \ast \underset{ʃ_{inf} X}{\times} X.

    Concretely, once you specify your 𝔸 1\mathbb{A}^1 with an origin 0:*𝔸 10 : \ast \to \mathbb{A}^1, then D 1:=*×ʃ inf𝔸 1𝔸 1D^1 := \ast \underset{ʃ_{inf} \mathbb{A}^1}{\times} \mathbb{A}^1 is your standard infinitesimal interval. (In standard models this is the usual Spec([ε]/(ε 2))Spec(\mathbb{R}[\epsilon]/(\epsilon^2))). Then the tangent bundle/differentiation functor is [D 1,][D^1,-], as usual.

    Let me maybe say more concisely what my two points above were:

    1. ʃ infʃ_{inf} is a replacement of the KL-axiomatics in terms of adjoint modalities;

    2. and it happens to be an axiomatics for synthetic differentials that has already been much explored by people other than K and L.

    • CommentRowNumber55.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2014

    With KL-axiomatics, I can say internally what the derivative of f:RRf:R\to R is at a point x:Rx:R as an element of RR, not just a map out of the infinitesimal neighborhood of xx.

    • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2014

    (There are, of course, people other than Kock and Lawvere who have studied classical SDG.)

    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeOct 30th 2014
    • (edited Oct 30th 2014)

    Sorry, somehow we are speaking past each other now, or maybe I am missing some point, let me know.

    What I am trying to say is that the kind of objects that the KL-axioms characterize are also axiomatized by the infinitesimal shape modality (and may be talked about internally, if desired) and that this alternative axiomatization has passed some practice test.

    • CommentRowNumber58.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2014

    I get that in models, the kind of objects described by the KL-axioms turn out to be the same kind of objects detectable by ʃ infʃ_{inf}. I’m wondering whether there is any internal connection between the two.

    Differential cohesion lets us say some sorts of things conveniently, while KL-axioms let us say other sorts of things conveniently. You seemed to be saying that you thought differential cohesion was “better” or “more modern” than the KL-axioms, so I was pointing out in contrast that the KL-axioms let us do some things that differential cohesion doesn’t, so it doesn’t make sense to discard them completely.

    One precise form of my question would be, can differential cohesion be enhanced in a natural way to include the KL-axioms?

    • CommentRowNumber59.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 31st 2014

    It sounds like a good opportunity to revisit synthetic differential geometry applied to algebraic geometry, which hasn’t been touched for 5 years. Currently there’s a string of questions raised there.

    Come to look at it, the page synthetic differential geometry itself is raising similar issues:

    Models of smooth toposes tend to be inspired, but more general than, constructions familiar from algebraic geometry. In particular the old insight promoted by Grothendieck in his work, that nilpotent ideals in rings are formal duals of spaces with infinitesimal extension is typically used to model infinitesimal spaces in synthetic differential geometry.

    The main difference between models for smooth toposes and algebraic geometry from this perspective is that models for smooth topos tend to employ test spaces that are richer than plain formal duals to commutative rings or algebras, as in algebraic geometry: typical models for synthetic differential geometry use test spaces given by formal duals of generalized smooth algebras that remember “smooth structure” in the usual sense of differential geometry (and different from, though not entirely unrelated, to the notion of smooth scheme in algebraic geometry). This is in particular true for the well adapted models.

    However, with a a sufficiently general perspective on higher geometry one finds that algebraic geometry and synthetic differential geometry are both special cases of a more general notion of theories of generalized spaces. For more on this see generalized scheme.

    But does generalized scheme, which presents a range of things the term might mean, give us a clear sense of algebraic geometry and synthetic differential geometry as special cases of something?

    And none of these pages has heard of differential cohesion.

    • CommentRowNumber60.
    • CommentAuthorMichael_Bachtold
    • CommentTimeOct 31st 2014
    • (edited Oct 31st 2014)

    One precise form of my question would be, can differential cohesion be enhanced in a natural way to include the KL-axioms?

    This might be related to a question raised by Lawvere: can we naturally axiomatize the infinitesimal interval D 1D^1 in such a way to obtain the “real line” RR with its commutative ring structure from it? Johnstone talks a few minutes about the question here and on the last slide.

    • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2014
    • (edited Oct 31st 2014)

    @Mike, re#58

    Regarding the relation of the axioms:

    I think of the KL-axiomatics as being something to add on top of an infinitesimal shape modality.

    The infinitesimal shape modality gives objects which are infinitesimal in the very elementary sense that the only maps out of reduced objects into them are constant. This is sufficient for many purposes of differential geometry.

    The KL-axiomatics adds to this the requirement that these infinitesimal objects are the objects of nilpotent elements with respect to a given ring structure. This adds to the geometric characterization of infinitesimals an algebraic characterization.

    I haven’t tried to make this relation a formal statement, but it shouln’t be hard. In fact I haven’t felt much need for the KL-axiomatics since working with infinitesimal shape.

    Regarding the words “modern” and “better”:

    I see that my comment about D-geometry being more “modern” than plain nilpotent algebra caused a misunderstanding. This comment of mine was meant in reply to the remark in #51 that you (Mike) are “not used to” thinking about SDG in terms of reduction \dashv infinitesimal shape. That seemed to be an appeal to common practice and a request to “get a feeling” for what’s going on, and so my remark was to say that in fact reduction/infinitesimal shape is common practice (in different terminology) in a development that has been taking place somwhat parallel to SDG in the math community, and hence is well explored.

    (I don’t think that being “modern” is a virtue in itself, but where mathematics is a healthy discipline the more modern (more contemporary) ways of thinking about the subject at least tend to incorporate the advances and insights of the past. I.e. I think in mathematics there is, by and large, net progress and so when wondering about how formalisms compare, it doesn’t hurt to check which of them have a modern development. Of course that’s not a law and many good ideas of the past get lost in the course of time, too. )

    • CommentRowNumber62.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2014
    • (edited Oct 31st 2014)

    @David, re #59

    true, these entries would deserve to be expanded further. There was in the past some debate with Zoran as to what “generalized scheme” should point to. If I remember well, I had originally have it point concretely to the concept in “Structured Spaces” (which is what the paragraphs you quote have in mind) but Zoran insisted that there are other generalizations, too.

    The axiomatics in Structured Spaces is the natural homotopy-theoretic version of the theory of locally ringed toposes of Grothendieck and Hakim. That’s the context in which one may start stating Kock-Lawvere-type axioms.

    @Michael Bachtold, re #60

    thanks for reminding us of Johnstone 08. This maybe serves to amplify the remark in #61 regarding the algebraic perspctive:

    In that note Peter Johnstone sticks to “the continuum” as being something equipped with at least a ring structure. And of course that is the traditional meaning of the word. And this is what the KL-axiomatics is closely related to.

    But from some point of view at least there is a “more elementary” level at which one may consider the continuum, a level at which one does not add algebraic structure yet. That’s what differential cohesion axiomatizes.

    In differential cohesion, one may axiomatize the continuum as follows: it is the object 𝔸 1\mathbb{A}^1 which (if it exists) is such that the shape modality restricted to the reduced objects is equivalent to 𝔸 1\mathbb{A}^1-localization.

    This does not say anything yet about a ring structure on 𝔸 1\mathbb{A}^1, but it already captures a considerable aspect of what the continuum is going to be good for in applications. In a second step one may then ask if there is ring structure on 𝔸 1\mathbb{A}^1, and whether its compatible with the monoid structure on (D 1) (D 1)(D^1)^{(D^1)}, etc.

    • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2014

    Regarding the words “modern” and “better”

    Thanks for clarifying! I think I didn’t realize what you were responding to specifically.

    it is the object 𝔸 1\mathbb{A}^1 which (if it exists) is such that the shape modality restricted to the reduced objects is equivalent to 𝔸 1\mathbb{A}^1-localization.

    Only on the reduced objects? Why is that? Can we construct the shape modality on all objects as some more general localization?

    I think of the KL-axiomatics as being something to add on top of an infinitesimal shape modality.

    That’s also helpful. But we could also think about going the other direction. Suppose given a ring object RR, or 𝔸 1\mathbb{A}^1 if you prefer, satisfying some KL-axioms; how much of differential cohesion can we reconstruct? We can construct the 𝔸 1\mathbb{A}^1-localization which ought to be (part of?) the shape modality. We can construct the family of infinitesimal subobjects of 𝔸 1\mathbb{A}^1 and localize at those; will that be the infinitesimal shape modality? Is there any natural candidate for a localization that should give the \sharp-modality? Is there any way to construct comodalities internally?

    Something else related that I’ve been wondering about: in any topos we have the internally defined real numbers object. My argument in the other thread should give a way to characterize that in the models of differential cohesion. It can’t be the KL-ring 𝔸 1\mathbb{A}^1, since the reals provably don’t contain infinitesimals (even constructively); but what about its reduction? If \Re preserves finite limits, then it preserves ring objects; is \Re \mathbb{R} related to 𝔸 1\mathbb{A}^1?

    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2014
    • (edited Oct 31st 2014)

    it is the object A1 which (if it exists) is such that the shape modality restricted to the reduced objects is equivalent to A1-localization.

    Only on the reduced objects?

    Yes, so schematically it helps to think of objects as modeled on the site of objects of the form {𝔸 n×D q} n,q\{\mathbb{A}^n \times D^q\}_{n,q} (which is literally true in some models). The reduced objects are modeled on the {𝔸 n} n\{\mathbb{A}^n\}_n.

    Then for H reduced=Sh ({A n})\mathbf{H}_{reduced} = Sh_\infty(\{A^n \}) shape is 𝔸 1\mathbb{A}^1-localization. For H=Sh ({𝔸 n×D q} n,q)\mathbf{H} = Sh_\infty(\{\mathbb{A}^n \times D^q\}_{n,q}) shape is localization at 𝔸 1\mathbb{A}^1 and at D 1D^1.

    (Displaying only one first order infinitesimals here, for simplicity.)

    But we could also think about going the other direction. Suppose given a ring object R, or A1 if you prefer, satisfying some KL-axioms; how much of differential cohesion can we reconstruct?

    That’s exactly what I am thinking: given KL, then at least roughly one has differential cohesion implied (I would need to think about how much can be gotten precisely). In this sense KL is more, is a stronger axiom than differential cohesion. Hence it makes sense to have just differential cohesion and only later add KL, if desired, on top of it, but not the other way round (up to details).

    Is \Re \mathbb{R} related to 𝔸 1\mathbb{A}^1.

    In the standard models (i.e. the Cahiers topos) this is certainly so. But in fact also =𝔸 1\mathbb{R} = \mathbb{A}^1, whether it “provably contains infinitesimals” will depend on in which ambient topos we look at it:

    consider the coreflection H reducedH\mathbf{H}_{reduced} \hookrightarrow \mathbf{H} (with H\mathbf{H}, being, say, the Cahiers topos) and the ordinary real line (under Yoneda) H reduced\mathbb{R} \in \mathbf{H}_{reduced}, where it contains no infinitesimal elements. However, under the embedding H reducedH\mathbb{R} \in \mathbf{H}_{reduced} \hookrightarrow \mathbf{H} this is now the SDG real line and here it does suddenly contain infinitesimals! :-)

    • CommentRowNumber65.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2014

    In this sense KL is more, is a stronger axiom than differential cohesion. Hence it makes sense to have just differential cohesion and only later add KL, if desired, on top of it,

    Ok, I took your comment to mean that KL was an extra axiom to be added to differential cohesion, rather than a stronger axiom from which one could prove differential cohesion.

    whether it “provably contains infinitesimals” will depend on in which ambient topos we look at it

    Right, so there is the real numbers object of H\mathbf{H} and also the real numbers object of H reduced\mathbf{H}_{reduced}. Neither of them contains infinitesimals in the topos wherein it’s defined, but if you map the real numbers object of H reduced\mathbf{H}_{reduced} into H\mathbf{H} then it becomes some other ring 𝔸 1\mathbb{A}^1 that contains infinitesimals. But does \Re map the real numbers object of H\mathbf{H} to the real numbers object of H reduced\mathbf{H}_{reduced}?

    • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2014

    (Just to be clear, here H\mathbf{H} and H reduced\mathbf{H}_{reduced} are what are elsewhere called H th\mathbf{H}_{th} and H\mathbf{H} respectively, right?)

    • CommentRowNumber67.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2014
    • (edited Nov 1st 2014)

    Regarding the relation of the axioms:

    So if KL implies differential cohesion (or to the extent it does) then we may ask if we may lift differential cohesion to KL. But not the other way around. KL is “higher in the hierarchy”.

    Regarding the reduction:

    yes, as I said, the SDG line in the Cahiers topos H\mathbf{H} is the inclusion H reducedH\mathbb{R} \in \mathbf{H}_{reduced} \hookrightarrow \mathbf{H} of the external real line under yoneda. Hence it is reduced.

    Beware of the following subtlety: there are “infinitesimals in between classical points” and then there is “infinitesimal directions”. Reduction removes the latter, not the former.

    Every ordinary manifold Σ\Sigma is reduced in the Cahiers topos, and yet each of its points has infinitesimal neighbours.

    The objects without any infinitesimals whatsoever are instead the coreduced ones.

    • CommentRowNumber68.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2014
    • (edited Nov 1st 2014)

    If this seems mysterious, go back to the original definition of all this in terms of rings of functions. Reduced means that the ring of functions has no nilpotent elements. So C ()C^\infty(\mathbb{R}) is reduced, but C (D)=[ε]/(ε 2)C^\infty(D) = \mathbb{R}[\epsilon]/(\epsilon^2) is not. Accordingly we have ()=\Re(\mathbb{R}) = \mathbb{R} but (D)=*\Re(D) = \ast.

    Nevertheless, there “are infinitesimals inside \mathbb{R}”, reflected by the fact that there are non-constant maps DD \to \mathbb{R} hence surjective algebra homomorphisms C ()[ε](ε 2)C^\infty(\mathbb{R}) \to \mathbb{R}[\epsilon](\epsilon^2).

    • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeNov 1st 2014

    as I said, the SDG line in the Cahiers topos H\mathbf{H} is the inclusion H reducedH\mathbb{R} \in \mathbf{H}_{reduced} \hookrightarrow \mathbf{H} of the external real line under yoneda. Hence it is reduced.

    That’s not what I asked. I got that; I was asking whether it is also the reduction of the real numbers object of H\mathbf{H}.

    • CommentRowNumber70.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2014

    Ah, I see where our misunderstanding is. You mean the Dedekind real number object, right? I mean the real line object that appears in the KL axioms.

    You are asking maybe if the latter is the reduction of the former? I don’t know what the Dedekind real number obect is in a smooth topos.

    • CommentRowNumber71.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    Yes, of course; I started out by saying “in any topos we have the internally defined real numbers object”.

    • CommentRowNumber72.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2014

    I am sorry Mike. Somehow in the context of SDG the smooth reals overshadow any other reals. But I see your point.

    I feel I may be forgetting something, but right now I don’t remember seeing much discussion of Dedekind or Cauchy reals in smooth toposes at all. Or maybe I never cared enough earlier to remember.

    Looking around I find arXiv:quant-ph/0202079 which in its section 2 has a little bit of reflection on the relation of the smooth reals to the Cauchy reals. But maybe all that article observes is that the latter is decidable while the former is not.

    So I don’t know. Need to think about it. What do we know about about Dedekind of Cauchy reals in smooth contexts? Even ignoring SDG, what do we known about these reals in Sh(SmthMfd)Sh(\mathrm{SmthMfd})? Does the argument from Sh(TopMfd)Sh(\mathrm{TopMfd}) go through here? (And did you meanwhile make any progress on closing the apparent gap in that argument, in the first place?)

    • CommentRowNumber73.
    • CommentAuthorMike Shulman
    • CommentTimeNov 2nd 2014

    Yeah, this potential confusion is why I never refer to the KL-ring in SDG as “the reals”. I’ve never seen much or any discussion of the Dedekind or Cauchy real numbers objects in smooth toposes either. I haven’t made any progress on Sh(TopMfd)Sh(TopMfd) even.

    • CommentRowNumber74.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    Given Thomas’ answer in the other thread, I think it should work just as well for smooth manifolds. For SDG, the question becomes something like: given a smooth locus L𝕃L\in \mathbb{L}, does the slice topos Sh(𝕃)/LSh(\mathbb{L})/L admit a local geometric morphism to a topos where we understand the reals, like Sh(X)Sh(X) for some topological space XX?

    • CommentRowNumber75.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014

    Combining your first sentence with your second, would a local geometric morphism to a slice of Sh(SmthMfd)\mathrm{Sh}(SmthMfd) do it, too?

    (That could work by base changing with \Re.)

    • CommentRowNumber76.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    Let’s see, so by the argument of C2.3.23, to have a local geometric morphism Sh(C,J)Sh(D,K)Sh(C,J) \to Sh(D,K) between sheaf toposes on sites, it suffices to have a fully faithful functor DCD\to C that both preserves and reflects covers.

    Now for an object L= n×WL =\mathbb{R}^n \times \ell W of ThCartSp (the site for the Cahiers topos), consider the functor 𝒪( n)ThCartSp/L\mathcal{O}(\mathbb{R}^n) \to ThCartSp/L that takes UU to U×WU\times \ell W. I’m going to guess that this is fully faithful, i.e. that if UVU\subseteq V there is only one map U×WV×WU\times \ell W\to V\times \ell W over n×W\mathbb{R}^n \times \ell W. And it clearly preserves and reflects covers. So we have a local geometric morphism 𝒞𝒯/LSh( n)\mathcal{CT}/L \to Sh(\mathbb{R}^n). Thus, by the argument in the other thread, the real numbers object of the Cahiers topos is the sheaf taking n×W\mathbb{R}^n \times \ell W to the set of continuous real-valued functions on n\mathbb{R}^n. This a coreduced object, right? What is its reduction?

    • CommentRowNumber77.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    Ah, I didn’t see your comment before posting mine. Yes, that would work too.

    Can we think a little bit about whether \Re could by any chance be implemented directly internally (i.e. without Type\sharp Type)? I’m pretty well convinced that ʃʃ can’t be (in general), but I don’t have as good a feel for \Re. Specifically, is there a “fiberwise” notion of reduction, and is it stable under pullback?

    • CommentRowNumber78.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)

    I’m going to guess that this is fully faithful, i.e. that if UVU\subseteq V there is only one map U×WV×WU\times \ell W\to V\times \ell W over n×W\mathbb{R}^n \times \ell W.

    Yes.

    Thus, by the argument in the other thread, the real numbers object of the Cahiers topos is the sheaf taking n×W\mathbb{R}^n \times \ell W to the set of continuous real-valued functions on n\mathbb{R}^n.

    Oh, That’s interesting.

    This a coreduced object, right?

    Yes.

    • CommentRowNumber79.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014

    Regarding \Re: as we discussed elsewhere, it seems fine to assume that it is lex. Doesn’t that solve what you need?

    • CommentRowNumber80.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014

    Regarding the reals: so in particular you are saying that the internal reals in Sh(SmthMfd)\mathrm{Sh}(\mathrm{SmthMfd}) is the sheaf of continuous real valued functions?

    (Have to rush off now. More later.)

    • CommentRowNumber81.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    so in particular you are saying that the internal reals in Sh(SmthMfd)\mathrm{Sh}(\mathrm{SmthMfd}) is the sheaf of continuous real valued functions?

    Yep. It does seem odd, doesn’t it? One would hope of course to get the sheaf of smooth real-valued functions. But I guess the point is that a topos, considered on its own, is only a topological object. The topos Sh(SmthMfd)\mathrm{Sh}(\mathrm{SmthMfd}), like the topos Sh(X)Sh(X) when XX is a smooth manifold, carries additional “smooth structure”, but nothing defined only in terms of the topos structure can “see” the smoothness.

    Regarding \Re: as we discussed elsewhere, it seems fine to assume that it is lex. Doesn’t that solve what you need?

    No, the situation with \Re is different than that for \sharp and ʃ infʃ_{inf} because it is a comonad rather than a monad.

    • CommentRowNumber82.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)

    I am really behind now with reacting. Getting back to #76:

    I don’t know if ( n×Spec(W)C 0( n, 1))(\mathbb{R}^n \times Spec(W)\mapsto C^0(\mathbb{R}^n, \mathbb{R}^1)) is reduced. But at least it seems not to be equivalent to

    C 0(, 1)Sh(CartSp)i !Sh(FormalCartSp) C^0(-,\mathbb{R}^1) \in \mathrm{Sh}(CartSp) \stackrel{i_!}{\hookrightarrow} \mathrm{Sh}(FormalCartSp)

    because that sheaf does have nontrivial maps Spec(W)i !C 0(, 1)Spec(W) \to i_!C^0(-,\mathbb{R}^1), namely those factoring through the smooth functions inside the continuous functions.

    • CommentRowNumber83.
    • CommentAuthorUrs
    • CommentTimeNov 16th 2014
    • (edited Nov 16th 2014)

    Finally coming back to the question in #1, here is a way to do it:

    For XX any type, its “infinitesimal disk bundle” T infXXT_{inf} X \to X whose fiber over a point is the infintesimal disk around that point is the pullback

    T infX X X infX \array{ T_{inf} X &\longrightarrow& X \\ \downarrow && \downarrow \\ X &\longrightarrow& \int_{inf} X }

    If ι:𝔸 nX\iota \colon \mathbb{A}^n \to X is formally etale, then it follows that

    ι *T infXT inf𝔸 n. \iota^\ast T_{inf} X \simeq T_{inf} \mathbb{A}^n \,.

    (Because by the definition of formal étalness and using the pasting law we have this equivalence of pasting diagrams of pullbacks:

    ι *T infX T inf X 𝔸 n X infXT inf𝔸 n 𝔸 n X 𝔸 n inf𝔸 n infX \array{ \iota^\ast T_{inf} X &\longrightarrow& T_{inf} &\longrightarrow& X \\ \downarrow && \downarrow && \downarrow \\ \mathbb{A}^n &\longrightarrow& X &\longrightarrow& \int_{inf} X } \;\;\;\; \simeq \;\;\;\; \array{ T_{inf} \mathbb{A}^n &\longrightarrow& \mathbb{A}^n &\longrightarrow& X \\ \downarrow && \downarrow && \downarrow \\ \mathbb{A}^n &\longrightarrow& \int_{inf} \mathbb{A}^n &\longrightarrow& \int_{inf} X }

    )

    We need one more assumption on what it takes for a type XX to be a manifold/scheme with tangent bundle: in addition to there being a map i𝔸 nX\coprod_i \mathbb{A}^n \to X which is a 1-epimorphism and is formally etale, we should also assume that the infinitesimal disk bundles of the 𝔸 n\mathbb{A}^n are trivialized

    T inf𝔸 n𝔸 n×D n. T_{inf} \mathbb{A}^n \simeq \mathbb{A}^n \times D^n \,.

    (This is just an evident regularity condition on what counts as a local model. )

    Then it follows that T infXXT_{inf} X \to X trivializes when pulled back to the cover

    i𝔸 n×D n T infX i𝔸 n X. \array{ \coprod_i \mathbb{A}^n \times D^n &\longrightarrow& T_{inf} X \\ \downarrow && \downarrow \\ \coprod_i \mathbb{A}^n &\longrightarrow& X } \,.

    This exhibits T infXXT_{inf} X \to X as a D nD^n-fiber infinity-bundle and by the discussion there, these are classified (modulated) by maps

    XBAut(D n). X \longrightarrow \mathbf{B} \mathbf{Aut}(D^n) \,.

    This is the map that #1 was asking for. If inf\int_{inf} exhibits first order infinitesimal shape, then

    Aut(D n)GL n \mathbf{Aut}(D^n) \simeq GL_n

    and we are done.

    • CommentRowNumber84.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 17th 2014

    If inf\int_{inf} exhibits first order infinitesimal shape, then

    Aut(D n)GL n \mathbf{Aut}(D^n) \simeq GL_n

    and we are done.

    Where was this worked out? I lost it somewhere above, probably.

    • CommentRowNumber85.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2014

    A endomorphism of the first order neighbourhood of a point needs to preserve the unique global point and is otherwise a linear map on the remaining coordinates. It being invertible means it is in GL nGL_n.

    • CommentRowNumber86.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 17th 2014

    @Urs - ah excellent! So the question posed at the top is completely answered.

    • CommentRowNumber87.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2014
    • (edited Nov 25th 2014)

    I have now put the content of #83 into a new subsection GL(n)-tangent bundles in the entry differential cohesion.

    (Maybe I ought to call them “frame bundles”, rather.)

    • CommentRowNumber88.
    • CommentAuthorUrs
    • CommentTimeDec 2nd 2014
    • (edited Dec 2nd 2014)

    Here is the next question.

    Next I’d like to discuss manifolds equipped with differential form/differential cocycle structure such that on each chart it is equivalent to a given one.

    A classical example would be a G2 structure on a 7-manifold, where the 7-manifold is equipped with a differential 3-form which on each chart is equivalent (equal, in this case) to the “associative 3-form”.

    But there are more examples where the differential data is instead that of some line nn-bundle (i.e. in the “Brane Bouquet”-discussion).

    Let (𝔻 n𝔸 n 0B n𝔾 conn)H /B n𝔾 conn(\mathbb{D}^n \hookrightarrow \mathbb{A}^n \stackrel{\nabla_0}{\to} \mathbf{B}^n \mathbb{G}_{conn}) \in \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}} be the local differential cocycle data. Consider a manifold XX as above which also carries such a cocycle and such that its pullback to the etale chart is equipped with an equivalencece to 0\nabla_0.

    Then I expect to be able to produce, in generalization of the tangent bundle map constructed above, a map of the form

    XB𝔾 connAut( 0) X \longrightarrow \underset{\mathbf{B}\mathbb{G}_{conn}}{\prod} \mathbf{Aut}(\nabla_0)

    such that postcomposition with the forgetful map

    XB𝔾 connAut( 0)BAut(𝔻 n)BGL(n) X \longrightarrow \underset{\mathbf{B}\mathbb{G}_{conn}}{\prod} \mathbf{Aut}(\nabla_0) \longrightarrow \mathbf{B}\mathbf{Aut}(\mathbb{D}^n) \simeq \mathbf{B} GL(n)

    is the underlying tangent bundle.

    As before, it seems pretty clear how the construction should go, but again I need more thinking on how to formally produce it.

    • CommentRowNumber89.
    • CommentAuthorUrs
    • CommentTimeDec 2nd 2014
    • (edited Dec 2nd 2014)

    Ah, this should be easy.

    As before, we need a regularity assumption on the model space 𝔸 n\mathbb{A}^n. Namely the autoequivalences of the trivial ( 0:𝔻 nB𝔾 conn)(\nabla_0 \colon \mathbb{D}^n \to \mathbf{B}\mathbb{G}_{conn})-bundle over 𝔸 n\mathbb{A}^n need to be equivalent to the autoequivalences of 𝔸 nB𝔾 conn\mathbb{A}^n \to \mathbf{B}\mathbb{G}_{conn}. This says that this local differential cocycle is determined by its values on the infinitesimal neighbourhoods as seen by inf\int_{inf}. This is true in the models for all differential form data and first order neighbourhoods.

    We should says that 0\nabla_0-structure on a manifold XX is a lift of its XBGL(n)X \to \mathbf{B} GL(n) through BB𝔾 connAut( 0)\mathbf{B} \underset{\mathbf{B}\mathbb{G}_{conn}}{\prod} \mathbf{Aut}(\nabla_0). This implies that there is a trivializing cover by 𝔸 n\mathbb{A}^ns. By the above assumption their Cech nerve extends over B𝔾 conn\mathbf{B}\mathbb{G}_{conn} and hence their homotopy colomit, which is XX, inherits a compatible map to B𝔾 conn\mathbf{B}\mathbb{G}_{conn}.

    This is the abstract version of classical statements such as that G 2G_2-structure is equivalent to an atlas by 7\mathbb{R}^7s compatibly equipped with associative 3-forms.