Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

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 19th 2012
    • (edited Oct 19th 2012)

    While working at geometry of physics on the next chapter Differentiation I am naturally led back to think again about how to best expose/introduce infinitesimal cohesion. To the reader but also, eventually, to Coq.

    First the trivial bit, concerning terminology: I am now tending to want to call it differential cohesion, and differential cohesive homotopy type theory. What do you think?

    Secondly, I have come to think that the extra right adjoint in an infinitesimally cohesive neighbourhood need not be part of the axioms (although it happens to be there for Sh (CartSp)Sh (CartSp th)Sh_\infty(CartSp) \hookrightarrow Sh_\infty(CartSp_{th}) ).

    So I am now tending to say

    Definition. A differential structure on a cohesive topos is an ∞-connected and locally ∞-connected geometric embedding into another cohesive topos.

    And that’s it. This induces a homotopy cofiber sequence

    CohesiveType InfThickenedCohesiveType InfinitesimalType DiscreteType \array{ CohesiveType &\hookrightarrow& InfThickenedCohesiveType &\to& InfinitesimalType \\ & \searrow & \downarrow & \swarrow \\ && DiscreteType }

    Certainly that alone is enough axioms to say in the model of smooth cohesion all of the following:

    So that seems to be plenty of justification for these axioms.

    We should, I think, decide which name is best (“differential cohesion”?, “infinitesimal cohesion”?) and then get serious about the “differential cohesive homotopy type theory” or “infinitesimal cohesive homotopy type theory” or maybe just “differential homotopy type theory” respectively.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 19th 2012

    So these axioms are at least a tad more general than what is strictly subsumed by “infinitesimal” theory, but in a good way:

    I think these axioms also capture “germ structure” and in fact can resolve the full hierarchy:

    • first order infintiesimals

    • second order infinitesimals

    • orbitrary order infinitesimals

    • germs

    To which corresponds the hierarchy

    • Lie algebra / Lie algebroid

    • formal group

    • local group

    So that’s good. All of this can be captured by a hierarchy of differential cohesion structures

    CohesiveTypeFirstOrderInfThickenedCohesiveTypehookrightorderSecondOrderInfThickenedCohesiveTypeFormallyThickenedCohesiveTypeLocallyThickenedCohesiveType CohesiveType \hookrightarrow FirstOrderInfThickenedCohesiveType \hookrightorder SecondOrderInfThickenedCohesiveType \hookrightarrow \cdots \hookrightarrow \cdots \hookrightarrow FormallyThickenedCohesiveType \hookrightarrow LocallyThickenedCohesiveType
    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeOct 19th 2012

    I haven’t thought at all about this thickening business; I need to spend some time looking at it. A priori, “differential cohesion” seems a reasonable name.

    I’m not quite sure that “∞-connected and locally ∞-connected” is what you want to say, though. When its codomain isn’t Gpd\infty Gpd, having a left adjoint to the inverse image isn’t sufficient to make a geometric morphism locally connected. And if it isn’t locally connected, then being connected (i.e. the inverse image functor being fully faithful) isn’t equivalent to the left adjoint preserving the terminal object. And of course, an embedding can never be connected (in the usual sense) without being an equivalence.

  1. to parallel the naming of cohesive (infinity,1)-topos and cohesive homotopy type theory, we have differential cohesive (infinity,1)-topos and differential cohesive homotopy type theory.


    diff, v5, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2022

    Okay. Yet later I had changed my mind to calling this elastic homotopy theory – have added the remark here.

    diff, v6, current

  2. this added text was from the HoTT wiki on differential cohesive homotopy type theory, I don’t know how accurate it is.


    diff, v7, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2022

    Who is it who has been working on or thinking about this syntactic formulation of the theory? I wasn’t aware that anyone looked into this.

    • CommentRowNumber8.
    • CommentAuthorGuest
    • CommentTimeJun 18th 2022
    I have no idea, looking at the history of the corresponding page on the HoTT wiki it was some anonymous editor from the beginning of April 2022
    • CommentRowNumber9.
    • CommentAuthorGuest
    • CommentTimeJun 18th 2022

    Last revision before merger:

    • CommentRowNumber10.
    • CommentAuthorGuest
    • CommentTime7 days ago

    This looks very incomplete, the given rules in the article seem to only be formation rules.

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

  • (Help)