Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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$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.
1 to 3 of 3