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.

• 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_\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

$\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

$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 $\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.

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)