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
    • CommentTimeJan 21st 2015
    • (edited Jan 21st 2015)

    Warning: What follows is just trivia. But since we had related discussion here before, maybe I am excused to waste time with this.

    Way back, we (maybe mostly Mike and me) had agreed on symbols for the three modalities of cohesionʃ,,ʃ, \flat, \sharp – and seemed to have been happy with ever since.

    Moreover, in the last months I have been stabilizing myself on writing \Re and \Im for the reduction modality and the infinitesimal flat modality of differential cohesion. The choice of \Re works really well, I think, both with the “re” in “reduction” as well as with the intuitive meaning that the reduced types are what is real about a formal geometry. This suggests to use \Im for one of the other two. It doesn’t really seem to work for the infinitesimal shape, but using it for infinitesimal flat seems okay.

    In any case, that leaves the infinitesimal shape modality in need of a good symbol.

    Originally (and still on several nnLab pages) I had denoted it Π inf\mathbf{\Pi}_{inf}, alluding to the fact that it produces “infinitesimal path \infty-groupoids”. I still think that’s a great way to think about it, but since finite shape has come to be called ʃʃ and also since now the other two differential modalities don’t carry an inf{}_{inf}-subscript anymore, it feels a bit anachronistic now.

    Better would be one single nice symbol for infinitesimal shape. Which one?

    One idea I have is this: the modal types of infinitesimal shape in the slice over XX are precisely the (formally) étale types over XX. Maybe there is a nice 1-symbol reflection of “étale”.

    And there is, of sorts: a ligature of the two letters “et” is what became “&”. Aren’t there also some other versions of a ligature of “et” somewhere in the common TeX collection of symbols?

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 22nd 2015

    Unrelated to your ét idea, but what about δ? It has connotations of infinitesimal variation (as in, variational calculus).

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    On https://en.wikipedia.org/wiki/Ampersand are mentioned some related Unicode ligatures like 🙰 and 🙲.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    David, I’ll think about that. However the risk is that it looks like a differentiation operation, which is not really what infinitesimal shape is.

    Mike, thanks. Unfortunately, all of these appear as boxes on my system, and hence probably on many other people’s system. Actually I like the look of “&” here, which (at least on my system) comes out as in this picture. I like this because it is most easily recognized as coming from “Et”.

    In LaTeX, I see that

      \it \&
    

    comes out as a very curly symbol that still has some resemablance wit “Et”.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    Huh, that’s funny; they look fine to me. Maybe I have better Unicode fonts installed than the average person? I would have expected European computers in general to be more Unicode-aware than American ones. Can you see 🙵?

    The LaTeX \textit{\&} looks nice too; I guess it is to be attributed to the Computer Modern fonts. (WP says “The Computer Modern fonts replace it with an “E.T.” symbol in the cmti#(text italic) fonts, so it can be entered as {\it\&} in running text when using the default (Computer Modern) fonts.”) But we need to have something to use on the lab (and forum, and blogs, etc.) too.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 22nd 2015

    This European computer saw all three as boxes.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    Thanks, Mike. Yes, I know that I could install font packages that would make all this display. But after I did this twice on two computers once, I ran out of energy on the third, and on my handheld it didn’t work anyway. (The EU is notorious for standardizing cucumber curvature radii, but it’s much more shy when it comes to enforcing useful standards ;-)

    But this italic ampersand is maybe good. To try it out, I have implemented it at infinitesimal shape modality. Does that look like a sustainable choice of symbols?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    Well, I’m wary of using an ordinary ampersand (which is I guess all we have available in iTeX) as a unary operator; it looks pretty weird to me.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    Okay, thanks for giving feedback. That’s what I was looking for. I’ll sleep over it. Further alternative suggestions are very welcome, too.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    It’s frustrating because I do like the idea of an ampersand-like symbol, and the other funny Unicode symbols look perfect to me. (-:

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    Hm. I just googled around and downloaded and installed something. Still doesn’t work. Would have to google around more and install more, I suppose.

    On the other hand, even if it displayed on your and on my system, we don’t want to be typing unicode numbers all the time. Already the shape modality is a pain in this respect.

    What we’d need is a simple macro functionality on the nLab. Such that we could declare something like “\et” and specify that on systems with fonts available it should display as character #49541229464549 and otherwise as &

    • CommentRowNumber12.
    • CommentAuthoradeelkh
    • CommentTimeJan 22nd 2015

    I can’t see the characters in #3 either, but they should be the ones labelled 1F670 and 1F672 on the second page of this pdf. These “ornamental dingbats” were apparently added to the Unicode standard in June 2014, which is probably why many of us can’t see them.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015

    A simple global macro functionality would be awesome! Can we put in a request?

    • CommentRowNumber14.
    • CommentAuthoradeelkh
    • CommentTimeJan 23rd 2015

    Global macros wouldn’t be too difficult to implement, I think, but I am not sure how to achieve the behaviour Urs mentioned in #11 (showing different characters based on browser support). That would have to be done client-side, while iTeX is compiled server-side. But I’ll think about it.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJan 23rd 2015
    • (edited Jan 23rd 2015)

    Global macros would already be quite excellent!

    But, so what does a client have to do (to install) to see those ampersands?

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015

    I wish I knew!

    • CommentRowNumber17.
    • CommentAuthoradeelkh
    • CommentTimeJan 23rd 2015

    Mike, what operating system are you using?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015

    Ubuntu Linux

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015

    And RHEL, at work.

    • CommentRowNumber20.
    • CommentAuthoradeelkh
    • CommentTimeJan 24th 2015

    Strange. I’ve tried it on a machine running Linux Mint, which is closely related to Ubuntu. It might not be an operating system issue after all. But I have no idea what’s going on.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2016

    Another possibility might be the “Tironian et”:

    \Re \dashv \Im\dashv ⁊

    http://www.fileformat.info/info/unicode/char/204a/index.htm

    https://en.wikipedia.org/wiki/Tironian_notes#Support_on_computers

    Unfortunately, it probably looks too much like a number 77.

    • CommentRowNumber22.
    • CommentAuthorNikolajK
    • CommentTimeJan 21st 2016

    @Mike: Good thing the number 7 hardly makes it into any articles on the nLab.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2016
    • (edited Jan 21st 2016)

    Good thing the number 7 hardly makes it into any articles on the nLab.

    The number 7 is a key player in entries such as 7-sphere, quaternionic Hopf fibration, octonionic Hopf fibration, H-space, Hopf invariant one problem, G2-manifold, M-theory on G2-manifolds, etc.

    Then there are D7-branes playing a pivotal role in the M/F-theory story, see the F-branes – table.

    In many other articles the number 7 appears in lists labeled by low lying integers, such as homotopy groups of spheres, spin group, orthogonal group, Whitehead tower, etc.

    • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 21st 2016

    Perhaps someone ought to write seven trees in one.

    The Tironian et doesn’t look that much like a 7 to my eyes. It looks closer to ¬\neg (but still quite distinct). Meanwhile, those Gothic letters always seem to confound me (the first looks like an RR; the second might be an II, or might be a TT – I never seem to remember these things).

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2016

    According to wikipedia,

    Some applications … substitute the Tironian et with the box-drawing character U+2510 ┐, as it displays widely.

    The Gothic letters are \Re and \Im, which were named I guess because some people use them for Real and Imaginary parts of a complex number. So the second is an II (Urs is using it to stand for “infinitesimal”), but I agree that it’s often hard to identify Gothic letters.

    What do you think, Urs, does ⁊ look too much like 77? It may depend somewhat on the fonts people’s browsers are using.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2016
    • (edited Jan 21st 2016)

    What do you think, Urs, does ⁊ look too much like 77?

    I’d be happy with the look of it in itself, but of course only the most erudite of readers will feel reminded of “étale” when seeing “⁊” – a connection which I had hoped an Et-ligature would help to make.

    I don’t know. Might it make sense to just wait… until the unicode characters that you suggested in #3 are more widely supported?

    Or let’s come back to #4: The curious thing is that here on the nForum – but not on the nLab – the plain ampersand from my keyboard comes out just right (on my system at least), namely as the Trebuchet ampersand. If this works here, should it not somehow be possible to make this work more generally?

    • CommentRowNumber27.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 22nd 2016
    • (edited Jan 22nd 2016)

    Testing an idea:

    EtE\! t

    hmm, doesn’t really work. I was thinking you might be able to make a home-made ligature using an upright capital E and t, but I can’t get the forum to recognise \mathrm.

    • CommentRowNumber28.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 22nd 2016

    Of course I’m half-kidding about Gothic letters in mathematics, which have been around forever (and of course I can always, and did in fact, check up on the ones Mike explained in #25). More seriously, I will ask: what word beginning with R does the \mathrm{E\\Re stand for, in Urs’s context? (And less seriously but truthfully: I did for the longest time think that the Gothic A was a U, and the Gothic P was a B.)

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2016
    • (edited Jan 22nd 2016)

    what word beginning with R does the \Re stand for, in Urs’s context?

    Reduction, in the traditional sense of reduced scheme. It is the symbol for the reduction modality.

    id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& Rh & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& ʃ &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }

    I thought \Re was a pretty good symbol for this, because besides alliterating the technical term of “reduction”, its pronounciation as “real part” harmonizes with the nature of reduced spaces: an infinitesimal thickening of a space is an etheral halo around its reduced part, invisible for any map into it out of a reduced space.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2016
    • (edited Jan 24th 2016)

    When writing a paper, of course, we should be fine as long as whoever is compiling the TeX file has the appropriate fonts installed.

    In poking around regarding what the appropriate font might be, I now have a guess as to why the nice ligatures work for me and no one else: I have the Symbola font installed. Would anyone else care to try installing it and see whether that makes 🙰 display for you?

    With that font installed, we can then get the character in a LaTeX document as well, as long as we compile with xelatex:

    \documentclass{amsart}
    \usepackage{fontspec}
    \newcommand{\et}{\text{\fontspec{Symbola} ?}}
    \begin{document}
    \[ \Re \dashv \Im \dashv \et \]
    \end{document}
    

    with the appropriate UTF-8 character inserted after the fontspec command – the nforum software doesn’t seem able to handle that actual character. Unfortunately, arXiv and journals probably don’t have Symbola installed or support xetex.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2016

    Re #4, even if we could get that to work for everyone reliably, I would still prefer not to use any kind of ampersand as a unary operator.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2016

    We could, of course, just make it with an image file…

    • CommentRowNumber33.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 24th 2016

    I installed Symbola on OS X 10.10.5 as per #30 and I can get the fancy ligature Mike’s been using.

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeMay 22nd 2017

    I’m confused. #1 of this thread suggests using & or a version of it for infinitesimal shape, because its modal morphisms are the etale ones. But on various nLab pages it seems that I now see \Im being used for the infinitesimal shape and & for the infinitesimal flat. Was there a switch at some point? What does & have to do with infinitesimal flat?

    (In general I’m lacking in intuition for infinitesimal flat; what for instance does it do when applied to a reduced object like RR?)

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeMay 22nd 2017
    • (edited May 22nd 2017)

    Hi Mike,

    that’s true, at some point I switched to using \Im for infinitesimal shape. I have to admit that I forget when this happened, but it’s now all over the place.

    The rationale for writing some form of ampersand for infinitesimal flat came from this observation, showing that ampersand(X)*ampersand(X) \to \ast is formally étale for every XX.

    On the poisitive side, my system finally shows me the unicode characters that you suggested in #3. I like them, especially the second one there.

    Regarding intuition for infinitesimal flat, I am going entirely by the adjunction with infinitesimal shape, and the good intuition that I have for that (infinitesimal path infinity-groupoid).

    I don’t have an explicit description for infinitesimal flat of reduced objects. Indeed I haven’t used infinitesimal flat much at all beyond the fact that its existence implies that infinitesimal shape preserves colimits.

    • CommentRowNumber36.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 22nd 2017

    If it’s ’just’ the infinitesimal version of \flat, why can’t we use out intuitions from the latter? After all, from shape, one can see how infinitesimal shape goes.

    Is it that passage to the infinitesimal version has lost flat’s right adjoint, so we’re thrown back on viewing infinitesimal flat through its relation to the left adjoint, hence just as some modification of coefficients necessary to make sense of the effect of infinitesimal shape?

    Is there an intuitive reason why flat has a right adjoint, but infinitesimal flat doesn’t?

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeMay 22nd 2017
    • (edited May 22nd 2017)

    If it’s ’just’ the infinitesimal version of \flat, why can’t we use out intuitions from the latter?

    Yes, that’s what works for me. But for the plain flat modality one may develop two kinds of intuitions, and only one seems to generalize: On the one hand X\flat X is the moduli space for finite flat parallel transport with coefficients in XX. On the other hand X\flat X is the locally constant object on the underlying object of XX with its cohesion forgotten.

    The former intuition generalizes: “infinitesimal flat X” is the moduli object for infinitesimal parallel transport with coefficients in XX.

    That’s what i was referring to when saying we get the intuition on infinitesimal flat from its adjunction to infinitesimal shape.

    • CommentRowNumber38.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 22nd 2017
    • (edited May 22nd 2017)

    and only one seems to generalize

    My hunch was to link that to infinitesimal flat’s lack of right adjoint.

    Is it easy to see how X\flat X as

    the locally constant object on the underlying object of XX with its cohesion forgotten

    preserves colimits, where infinitesimal flat fails?

    [Similarly, I remember looking but not finding an intuitive way to see why infinitesimal shape gets a left adjoint, when shape doesn’t have one.]

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeMay 22nd 2017
    • (edited May 22nd 2017)

    I don’t really buy the intuition of \Im as an infinitesimal version of shape. The cohesive ʃʃ builds new equalities from continuous paths; in particular, it creates new higher \infty-groupoid structure where there wasn’t any before. But \Im doesn’t do that — it’s left exact, so it preserves nn-types for all nn. It makes more sense to me to think of \Im as forgetting the existing infinitesimal directions entirely and then stipulating that the only infinitesimal directions are constant, dual to how \Re forgets the existing infinitesimal directions and then stipulates that there are exactly the “canonical” ones induced from the smooth structure.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeMay 22nd 2017

    Formally, it’s the adjunction \Re \dashv \Im that’s analogous to \flat \dashv \sharp, so in that sense \Im is more like \sharp than it is like ʃʃ. Both \flat and \sharp forget the cohesion and then add it back in universally; similarly, both \Re and \Im forget the infinitesimal directions and then add them back in universally.

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeMay 22nd 2017
    • (edited May 22nd 2017)

    I don’t really buy the intuition of \Im as an infinitesimal version of shape.

    While it’s true that some aspects of \Im are crucially different from ʃʃ, this intuition is justified from crystals: Just like maps out of ʃʃ are modeled by parallel transport along finite paths, so maps out of a “de Rham stack “X\Im X are modeled by parallel transport along infintesimal paths (“crystalline cohomology”). For a quick reference see item (3) on p. 2 of Lurie’s note .

    The reason that \Im does not change the tuncation degree is because the infinitesmal paths are “too short” to wind around cycles.

    • CommentRowNumber42.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 22nd 2017
    • (edited May 22nd 2017)

    Isn’t it the case that the modalities will reveal different similarities depending what you look for? Down that vertical central axis of the staggered version there are three localisations for kinds of dimension: =loc ,=loc 𝔻,R=loc 0|1\int = loc_{\mathbb{R}}, \Im = loc_{\mathbb{D}}, R = loc_{\mathbb{R}^{0|1}}.

    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2017

    Yes, that’s a good way to think about it. Where loc 𝔻loc_{\mathbb{D}} is shorthand for localization at all the infinitesimally thickened points.

    • CommentRowNumber44.
    • CommentAuthorMike Shulman
    • CommentTimeMay 23rd 2017

    I suppose maybe that’s helpful if you already know about crystals, but to me it just sounds more confusing.

    • CommentRowNumber45.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 23rd 2017

    There’s David Speyer’s introductory Three ways of looking at a local system: the infinitesimal perspective and his follow-up The infinitesimal site.

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeMay 23rd 2017

    Let me rephrase that in a more productive way. If I don’t already know what crystals are, can I use my existing intuition that \Im simply “declares the only infinitesimal directions to be constant” to understand crystaline cohomology?

    (By the way, for anyone who doesn’t know, one of the groups at the HoTT MRC next month will be working on differential cohesive HoTT. The goal is basically to do for differential cohesion what BFP RCoHoTT did for continuous cohesion. Maybe this will result in my finally understanding differential cohesion!)

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2017
    • (edited May 23rd 2017)

    declares the only infinitesimal directions to be constant” to understand crystaline cohomology?

    I’d think so. The key is to make that declaration propositionally, i.e. to impose the constancy not by saying that a step in an infinitesimal direction is equal to a constant step, but to say that there is a “path” connecting the two.

    That’s what is described on that page in the note by Lurie that I pointed to.

    (I believe (but never checked) that because these infintiesimal paths are so short that there is no further information in them besides their endpoints, hence because these infinitesimal paths are all straight edges that one imagines that all these infinitesimal meighbour points with all these straight paths connecting them look like a “crystal”.)

    Anyway, just as cohomology with local coefficients is equivalently the cohomology of the shape of XX, hence of the infinity-groupoid of finite paths in XX, so crystalline cohomology is equivalently the cohomology of this groupoid of infinitesimal paths in XX.

    • CommentRowNumber48.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2017

    By the way, for anyone who doesn’t know, one of the groups at the HoTT MRC next month will be working on differential cohesive HoTT. The goal is basically to do for differential cohesion what BFP RCoHoTT did for continuous cohesion. Maybe this will result in my finally understanding differential cohesion!

    Felix Wellen had recently told me about this. I am (positively) surprised. There is no indication of this activity on the MRC page.

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeMay 23rd 2017

    The public MRC announcement page isn’t going to change; the project assignments and so on are being done internally between the organizers and the participants.

    I think I do now see that my intuition for \Im needs some modification. I usually think about local toposes mainly in terms of cohesive and similar models, where a good intuition comes from thinking about concrete objects, where AAA \to \sharp A is monic. But it seems that it is more rare for i:AAi:A\to \Im A to be monic. In particular, Felix just mentioned to the MRC group the interpretation of its kernel-pair i(x)=i(y)i(x)=i(y) as the relation “xx is infinitesimally close to yy”, whose equivalence classes are tangent spaces.

    On the other hand, this example also makes me wary of the “shape” analogy for a different reason, namely that AAA\to \Im A, unlike AʃAA\to ʃ A, is not usually going to be surjective either. (In particular, (x=y)=(i(x)=i(y))\Im(x=y) = (i(x)=i(y)) since \Im is lex, but infinitesimally close points are not generally equal.) It doesn’t seem right to think of AAA\to \Im A as “quotienting out infinitesimal paths” if A\Im A can be inhabited even when AA is empty.

    Here’s a suggestion for a related but perhaps better intuition. A good general intuition for A\sharp A in cohesion is “discontinuously AA”, i.e. an element of AA that is not required to depend continuously on the context, and inherits only (co)trivial cohesion from AA. Similarly, could we say that A\Im A means “infinitesimally AA”, meaning an element of AA that is defined “up to infinitesimal variation in the context” and moreover ignores all infinitesimal differences in AA? For instance, in the context of x:A,y:Ax:A,y:A, we may not be able to inhabit x=yx=y, but if xx and yy are infinitesimally close then we can “almost” do so, and hence we can inhabit (x=y)\Im(x=y). And the second clause is similar to quotienting out infinitesimal paths, but perhaps makes it more clear that we shouldn’t expect to get any higher homotopy thereby.

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2017
    • (edited May 23rd 2017)

    namely that AAA\to \Im A, unlike AʃAA\to ʃ A, is not usually going to be surjective

    That’s right, in fact there is established terminology for this: If AAA \to \Im A is surjective then AA is called formally smooth.

    All objects are formally smooth in the differential geometric models such as formal smooth infinity-groupoids, but it is not generally the case in algebraic geometry. There one needs Noetherian-ness.

    • CommentRowNumber51.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2017

    Here’s a suggestion for a related but perhaps better intuition. […] could we say that A\Im A means “infinitesimally AA”, meaning an element of AA that is defined “up to infinitesimal variation in the context” and moreover ignores all infinitesimal differences in AA?

    Sounds good to me!

    • CommentRowNumber52.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 23rd 2017

    That sounds like Curry’s idea that ϕ\bigcirc \phi is an internalisation into a stricter system of what is true in a more relaxed (stronger) system. Neel Krishnaswami seemed to be reinventing that here.

    I give (here) a simple analogous case in which all dogs have an (individual) owner, where that a dog is a ’possible’ pug means there is a co-owned dog which is a pug.

    • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeMay 24th 2017

    All objects are formally smooth in the differential geometric models

    I was wondering about that. I don’t have any intuition for “global” objects (in the empty context) that aren’t formally smooth, but I guess that makes sense since I don’t have much intuition for algebraic geometry. But the example of x=yx=y shows that even in differential geometry this can fail in nonempty contexts, right?

    • CommentRowNumber54.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 24th 2017

    From C^\infty-Differentiable Spaces

    A differentiable space XX is formally smooth if and only if each pXp \in X has an open neighbourhood which is isomorphic to the Whitney subspace of a closed subset of some n\mathbb{R}^n. (p. 124)

    Now, given a closed subset YY of n\mathbb{R}^n, the Whitney subspace W Y\mathbf{W}_Y is the differentiable subspace of n\mathbb{R}^n defined by the Whitney ideal of all differentiable functions on n\mathbb{R}^n whose Taylor expansion at any point yYy \in Y is null.

    • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeMay 24th 2017

    @Mike,

    this can fail in nonempty contexts, right?

    That sounds right. I haven’t thought about this is non-empty contexts much.

    @David,

    the statement I am referring to, that XXX \to \Im X is epi in the differential geometric model, is prop. 2.18 in arXiv:1701.06238.

    • CommentRowNumber56.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 24th 2017

    I thought we were trying to think up non-formally smooth spaces in a differential geometric context. Doesn’t what I quoted suggest what would be need there for formal smoothness to fail?

    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeMay 24th 2017
    • (edited May 24th 2017)

    we were trying to think up non-formally smooth spaces in a differential geometric context.

    Oh, okay. So then first you need to specify a model of differential cohesion inside which to find such examples. Do you want a model still to be a topos?

    • CommentRowNumber58.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 25th 2017

    Re #46,

    The goal is basically to do for differential cohesion what BFP RCoHoTT did for continuous cohesion.

    Since choosing an accessible, prominent target theorem, the BFP, was an important feature of that work, what might you choose as a target in the differential case?

    • CommentRowNumber59.
    • CommentAuthorMike Shulman
    • CommentTimeMay 25th 2017

    Not sure; maybe Urs has some suggestions? The first step is to set up the type theory; depending on how difficult that is, it might take a lot of the week.

    • CommentRowNumber60.
    • CommentAuthorMike Shulman
    • CommentTimeMay 25th 2017

    Felix Wellen is in the group, so he may be able to help us with goals to aim for too.

    • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeMay 25th 2017
    • (edited May 25th 2017)

    As you will know, Felix Wellen’s thesis will be the solution to the first of the list of formalization probems that I had advertized in Some thoughts on the future of modal homotopy type theory. The others listed there concern other modalities.

    To my mind, the central application where everything about cohesion and differential cohesion in \infty-toposes comes together is the theory of “infinitesimally integrable definite globalizations of differential cocycles” in section 5.3.13 of dcct (v2).

    This is about fixing a differential cocycle on a cohesive group VV and then, given a “VV-manifold” XX (étale \infty-stack modeled on VV), ask for the obstructions to having a differential cocycle on all of XX which suitably restricts on the infinitesimal neighbourhood of each point to the given cocycle on VV, restricted to the infinitesimal neighbourhood of the neutral element.

    This is the homotopy theoretic version of what Bryant calls definite forms, controlling for instance the theory of G 2G_2-manifolds.

    Theorem 5.3.129 in dcct (v2) states that an obstruction to the existence of such globalizations is the existence of integrable GG-structure on the VV-manifold (the way Felix discusses at the end of his thesis) for GG the “quantomorphism” group of the given differential cocycles, namely the differential concretification of its automorphism \infty-group.

    I think this is an absolutely central statement to higher differential geometry, though its consequences need to be fleshed out further.

    It’s remarkable how all the modalities interact here: shape and flat control the existence of the differential cocycle in the first place, sharp controls the differential concretification of its automorphism group and infinitesimal shape governs the concepts of VV-manifolds, definite globalizations and torsion-free GG-stuctures.

    On the other hand, this theorem takes a fair bit of prerequisite definitions and lemmas. This will be a bit of work to formalize. But the effort would certainly be worth it.

    • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeMay 25th 2017

    Thanks!

    • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2017

    sharp controls the differential concretification of its automorphism group

    Is this the \sharp of H\mathbf{H} or of H th\mathbf{H}_{th}? I am currently rather confused about how these are related to each other, if at all.

    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2017
    • (edited Jun 2nd 2017)

    You are right, something needs to be adjusted here. For the construction to come out as intended, it needs to be the sharp on H\mathbf{H}. Otherwise the result is \Im of the intended result.

    I need to look into this.

    Incidentally, my formula for the differential concretification using the \sharp operator also contained a mistake, in that it did not actually produce the claimed object in the model. This was thankfully pointed out to me by Alexander Schenkel and Marco Benini. We fixed the formula for the 1-truncated case in arXiv:1704.01378, and I fixed it for the general case in the nnLab’s Sandbox (of all places). But then I got overwhelmed with other duties. I need to get back to this and eventually produce a coherent writeup.

    • CommentRowNumber65.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2017

    What is the correct definition? I don’t see any \sharp’s in prominence on the Sandbox.

    • CommentRowNumber66.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2017
    • CommentRowNumber67.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2017

    Thanks. Is some of the notation confused there? Are the “conn” subscripts the same as the Conn boldface?

    • CommentRowNumber68.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2017

    Oh, no, wait, I see, it is something else, some chain complex. Can that be defined synthetically?

    • CommentRowNumber69.
    • CommentAuthorUrs
    • CommentTimeJun 3rd 2017

    Right, so the boldface GConn(X)G\mathbf{Conn}(X) is used for the moduli stacks of connections, while the connconn-subscript on BG conn\mathbf{B}G_{conn} denotes the classifying stacks. So GConn(X)G \mathbf{Conn}(X) is to denote the concretification of [X,BG conn][X, \mathbf{B}G_{conn}].

    I don’t know that these Deligne chain complexes may be defined synthetically. The argument in the Sandbox is less ambitious: It just means to show that there is a construction formulated abstractly using just cohesion (that def 3.1) which in the standard model applied to these chain complexes yields the expected result.

    • CommentRowNumber70.
    • CommentAuthorMike Shulman
    • CommentTimeJun 3rd 2017

    Can you say more, then, about what you were suggesting in #61 as a goal for formalization? If one of the main inputs to the result can’t be defined synthetically, what exactly would you like to see done synthetically?

    • CommentRowNumber71.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2017

    The result I was pointing to expresses the obstruction to a definite globalization of any (differential) cocycle, it is not specific to cocycles in Deligne cohomology.

    • CommentRowNumber72.
    • CommentAuthorMike Shulman
    • CommentTimeJun 6th 2017

    The theorem involves differential concretification, and you said in #64 that your formula for differential concretification was wrong. Is there a correct formula for differential concretification that works for arbitrary cocycles?

    • CommentRowNumber73.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2017

    That formula which I had pointed you to above (now here) gives the right answer for ordinary differential cocycles. That’s the only case for which we know a priori what the answer should be. So then from there one would be inclined to turn this around and take that formula, which now applies generally, to be the definition of differential concretification.

    • CommentRowNumber74.
    • CommentAuthorMike Shulman
    • CommentTimeJun 6th 2017

    How does that formula apply generally? It uses the Deligne complex.

    • CommentRowNumber75.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2017
    • (edited Jun 7th 2017)

    Sorry, Mike, if I am being unclear. I see that the note in the Sandbox was a bit terse.

    The general formula needs as input a type AA equipped with a filtration A=A nA n1A 0A = A_n \to A_{n-1} \to \cdots \to A_0, thought of as degreewise forgetting connection data (a “Hodge filtration”). Given this, then the concretification of AA on a geometrically contractible type Σ\Sigma is defined starting with

    AConn 0(Σ)[Σ,A 0]A \mathbf{Conn}_0(\Sigma) \coloneqq [\Sigma, A_0] and

    and then inductively

    AConn k+1(Σ)im nk([Σ,A k+1][Σ,A k+1]×[Σ,A k]AConn k(Σ))A \mathbf{Conn}_{k+1}(\Sigma) \coloneqq im_{n-k}\left( [\Sigma, A_{k+1}] \to \sharp [\Sigma, A_{k+1}] \underset{\sharp [\Sigma, A_k]}{\times} A \mathbf{Conn}_k(\Sigma)\right).

    • CommentRowNumber76.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 7th 2017
    • (edited Jun 7th 2017)

    It sounds like this is heading close to some of the issues appearing in that inconclusive discussion we had on FTC. Perhaps there is something there for eager young differentially cohesive HoTT-ers in Snowbird to develop, such as that intriguing idea that the solid cohesion of the super-world might be used to characterise constructions at the differential (elastic) stage. (But perhaps the solid modalities are for a later date.)

    • CommentRowNumber77.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2017
    • (edited Jun 7th 2017)

    Right, let me recall:

    If we do have the “first oder infinitesimal interval” D 1={x|x 2=0}D^1 = \{x \in \mathbb{R}\vert x^2 = 0\} \subset \mathbb{R} in hand, then there is the usual SDG Yoga: define microlinear spaces XX, then say what it means for a map TXX D 1T X \coloneqq X^{D^1} \longrightarrow \mathbb{R} to be fiberwise linear. These fiberwise linear maps TXT X \to \mathbb{R} then are the differential 1-forms on XX. Then one defines the wedge products and with this finally higher degree forms.

    This is not very elegant, though, first of all due to that requirement to restrict by hand to fiberwise linearity. (Which is also why the “amazing right adjoint() D 1(-)_{D^1} to () D 1(-)^{D^1} is not all that useful: D 1\mathbb{R}_{D^1} does not modulate differential 1-forms, only a sub-object Ω 1 D 1\Omega^1 \subset \mathbb{R}_{D^1} of it does, which takes work to carve out.)

    If however we pass to the super-geometric version of D 1D^1, the superpoint 0|1\mathbb{R}^{0\vert 1}, then this problem goes away: For every XX then the full type of functions X 0|1X^{\mathbb{R}^{0\vert 1}} \longrightarrow \mathbb{R} is, externally, the full de Rham complex of differential forms on XX (regarded as a super-space by its canonical /2\mathbb{Z}/2-grading of even/odd-degree forms). It even automatically knows the de Rham differential: that is given by the canonical action of the odd component of Aut( 0|1)Aut(\mathbb{R}^{0\vert 1}) on X 0|1X^{\mathbb{R}^{0\vert 1}} \to \mathbb{R}.

    • CommentRowNumber78.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2017

    Re #75: okay, great, thanks. That pullback is just the fiberwise \sharp, so it has a nice type-theoretic interpretation if we regard the filtration as a tower of dependent types.

    Re #77: that’s neat, but it’s turning out to be hard enough to write down a type theory for differential cohesion, so I don’t think we’ll try solid cohesion yet.

    • CommentRowNumber79.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2017
    • (edited Jun 7th 2017)

    That pullback is just the fiberwise \sharp

    Ah, right. So that’s some improvement already! I bet you’ll see many more improvements. I wish I had time to further think about this stuff with you right now.

    I don’t think we’ll try solid cohesion yet.

    I understand, this was in reaction to David’s suggestion.

    The punchline is just that if you do want to see explicit differential forms in a synthetic treatment (as opposed to just knowing that for every stable type EE the types ¯E\overline{\flat}E and ʃ¯E\overline{ʃ} E behave like those of closed and co-closed EE-valued differential forms, respectively ) then there are these two options:

    1. axiomatize D 1D^1 via a Kock-Lawvere axiom scheme and proceed in the established fashion – this works but is not elegant,

    2. pass to solid cohesion, require that there is an object 0|1\mathbb{R}^{0 \vert 1} such that the “rheonomy modality” RhRh is 0|1\mathbb{R}^{0\vert 1}-localization and then obtain the full de Rham complex in one go as

      Ω () (() 0|1) \Omega^\bullet(-) \;\coloneqq\; \mathbb{R}^{ \left( (-)^{\mathbb{R}^{0\vert 1}} \right)}

    I am not saying that you should do (either of) this. On the contrary, I have been advocating all along the perspective that it is not urgent to consider a synthetic axiomatization of exactly the standard differential forms if we already have the “general differential forms” ¯E\overline{\flat} E and ʃ¯E\overline{ʃ} E.

    This is maybe analogous to the story of Euclid’s synthetic axioms: There it is not too urgent to impose the parallel postulate, even if classical experience seems to suggest otherwise. On the contrary, it is useful to first prove things in more generality and only consider the axiom later.

    • CommentRowNumber80.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2017

    Are either (1) or (2) an instance of ¯E\overline{\flat}E or ʃ¯E\overline{ʃ} E (when restricted to closed or co-closed forms)? I mean, I presume so in the model, but is it provable synthetically that they are?

    • CommentRowNumber81.
    • CommentAuthormaxsnew
    • CommentTimeJun 8th 2017

    Sorry, but what do ¯E\overline{\flat}E and ʃ¯E\overline{ʃ} E mean here?

    • CommentRowNumber82.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 8th 2017
    • (edited Jun 8th 2017)

    For a comonadic modality

    ¯Xcofib(XX). \overline{\Box} X \coloneqq cofib(\Box X \to X).

    (See Definition 2.2.14 of dcct.)

    For a monadic one, it’s the fiber of the unit, though I’m not sure this is made explicit anywhere. It appears in the differential cohomology diagram in Proposition 2.2.17 at the same point in dcct.

    Notation is certainly not consistent across nLab.

    • CommentRowNumber83.
    • CommentAuthorUrs
    • CommentTimeJun 8th 2017

    is it provable synthetically that they are?

    I haven’t tried. That would certainly be a worthwhile question to look into.

    The key step in the proof would presumeably not be so much concerned with the nature of the differential forms as such, but with the interalization of the Dold-Kan corespondence: One will need way to turn a chain complex of stable types into a stable type and show that this construction behaves properly.

    Once this is established the remainder should be immediate.

    • CommentRowNumber84.
    • CommentAuthorUrs
    • CommentTimeJun 8th 2017
    • (edited Jun 8th 2017)

    what do ¯E\overline{\flat}E and ʃ¯E\overline{ʃ} E mean here?

    Sorry, my bad. Yes, as David says, I am using this sometimes to denote the homotopy (co-)fiber of the (co-)unit of the given (co-)monad. (Def. 2.7 in arXiv:1402.7041 or def. 0.13 here).

    And the statement which I was referring to, that for a stable cohesive type EE the types ¯E\overline{\flat}E and ʃ¯E\overline{ʃ} E have the interpretation of the (co-)closed EE-valued differential forms is discussed in some detail at differential cohomology diagram. Unfortunately, there I write instead dRE{\flat}_{dR} E and ʃ dRE{ʃ}_{dR} E for these (co-)fibers.

    • CommentRowNumber85.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 8th 2017

    Since we don’t have an official definition for monads, can we just imitate def 0.13:

    The negative of a comonadic moment \Box is what remains after taking away the piece of pure \Box-quality, hence is the cofiber (nlab) of the counit map:

    ¯(X)cofib(XX). \overline{\Box}(X) \coloneqq cofib(\Box X \to X) \,.

    So how about this?

    The negative of a monadic moment \bigcirc is what results from quotienting out the pure \bigcirc-quality, hence is the fiber (nlab) of the unit map:

    ¯(X)fib(XX). \overline{\bigcirc}(X) \coloneqq fib(X \to \bigcirc X) \,.
    • CommentRowNumber86.
    • CommentAuthorUrs
    • CommentTimeJun 8th 2017
    • (edited Jun 8th 2017)

    Yes. Maybe not “quotienting out” for the fiber. On the other hand if we do this on stable types, then the fiber of a morphism is of course also the cofiber of a shifted morphism.

    • CommentRowNumber87.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 8th 2017

    Ok, so what could we have to parallel the comonadic “is what remains after taking away the piece of..” ? Or just drop it and have

    The negative of a monadic moment \bigcirc is the fiber (nlab) of the unit map

    • CommentRowNumber88.
    • CommentAuthorUrs
    • CommentTimeJun 8th 2017

    Maybe we could say “co-quotient” for the fiber.

    • CommentRowNumber89.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 9th 2017

    Ok, have put something in as Definition 0.17.

    • CommentRowNumber90.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 22nd 2017

    Re #79 and the superalgebra approach to the de Rham complex, I see that Buium uses this approach in arithmetic differential geometry. If you can see page 33 of his book, he points out that there is no de Rham calculus available, but he can then use the Lie superalgebra formalism.

    • CommentRowNumber91.
    • CommentAuthorUrs
    • CommentTimeJun 22nd 2017

    Thanks for the alert. That’s really interesting.