Ah, this should be easy.
As before, we need a regularity assumption on the model space . Namely the autoequivalences of the trivial -bundle over need to be equivalent to the autoequivalences of . This says that this local differential cocycle is determined by its values on the infinitesimal neighbourhoods as seen by . This is true in the models for all differential form data and first order neighbourhoods.
We should says that -structure on a manifold is a lift of its through . This implies that there is a trivializing cover by s. By the above assumption their Cech nerve extends over and hence their homotopy colomit, which is , inherits a compatible map to .
This is the abstract version of classical statements such as that -structure is equivalent to an atlas by s compatibly equipped with associative 3-forms.
]]>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 -bundle (i.e. in the “Brane Bouquet”-discussion).
Let be the local differential cocycle data. Consider a manifold as above which also carries such a cocycle and such that its pullback to the etale chart is equipped with an equivalencece to .
Then I expect to be able to produce, in generalization of the tangent bundle map constructed above, a map of the form
such that postcomposition with the forgetful map
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.
]]>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.)
]]>@Urs - ah excellent! So the question posed at the top is completely answered.
]]>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 .
]]>If exhibits first order infinitesimal shape, then
and we are done.
Where was this worked out? I lost it somewhere above, probably.
]]>Finally coming back to the question in #1, here is a way to do it:
For any type, its “infinitesimal disk bundle” whose fiber over a point is the infintesimal disk around that point is the pullback
If is formally etale, then it follows that
(Because by the definition of formal étalness and using the pasting law we have this equivalence of pasting diagrams of pullbacks:
)
We need one more assumption on what it takes for a type to be a manifold/scheme with tangent bundle: in addition to there being a map which is a 1-epimorphism and is formally etale, we should also assume that the infinitesimal disk bundles of the are trivialized
(This is just an evident regularity condition on what counts as a local model. )
Then it follows that trivializes when pulled back to the cover
This exhibits as a -fiber infinity-bundle and by the discussion there, these are classified (modulated) by maps
This is the map that #1 was asking for. If exhibits first order infinitesimal shape, then
and we are done.
]]>I am really behind now with reacting. Getting back to #76:
I don’t know if is reduced. But at least it seems not to be equivalent to
because that sheaf does have nontrivial maps , namely those factoring through the smooth functions inside the continuous functions.
]]>so in particular you are saying that the internal reals in 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 , like the topos when is a smooth manifold, carries additional “smooth structure”, but nothing defined only in terms of the topos structure can “see” the smoothness.
Regarding : as we discussed elsewhere, it seems fine to assume that it is lex. Doesn’t that solve what you need?
No, the situation with is different than that for and because it is a comonad rather than a monad.
]]>Regarding the reals: so in particular you are saying that the internal reals in is the sheaf of continuous real valued functions?
(Have to rush off now. More later.)
]]>Regarding : as we discussed elsewhere, it seems fine to assume that it is lex. Doesn’t that solve what you need?
]]>I’m going to guess that this is fully faithful, i.e. that if there is only one map over .
Yes.
Thus, by the argument in the other thread, the real numbers object of the Cahiers topos is the sheaf taking to the set of continuous real-valued functions on .
Oh, That’s interesting.
This a coreduced object, right?
Yes.
]]>Ah, I didn’t see your comment before posting mine. Yes, that would work too.
Can we think a little bit about whether could by any chance be implemented directly internally (i.e. without )? I’m pretty well convinced that can’t be (in general), but I don’t have as good a feel for . Specifically, is there a “fiberwise” notion of reduction, and is it stable under pullback?
]]>Let’s see, so by the argument of C2.3.23, to have a local geometric morphism between sheaf toposes on sites, it suffices to have a fully faithful functor that both preserves and reflects covers.
Now for an object of ThCartSp (the site for the Cahiers topos), consider the functor that takes to . I’m going to guess that this is fully faithful, i.e. that if there is only one map over . And it clearly preserves and reflects covers. So we have a local geometric morphism . Thus, by the argument in the other thread, the real numbers object of the Cahiers topos is the sheaf taking to the set of continuous real-valued functions on . This a coreduced object, right? What is its reduction?
]]>Combining your first sentence with your second, would a local geometric morphism to a slice of do it, too?
(That could work by base changing with .)
]]>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 , does the slice topos admit a local geometric morphism to a topos where we understand the reals, like for some topological space ?
]]>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 even.
]]>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 ? Does the argument from go through here? (And did you meanwhile make any progress on closing the apparent gap in that argument, in the first place?)
]]>Yes, of course; I started out by saying “in any topos we have the internally defined real numbers object”.
]]>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.
]]>as I said, the SDG line in the Cahiers topos is the inclusion 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 .
]]>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 is reduced, but is not. Accordingly we have but .
Nevertheless, there “are infinitesimals inside ”, reflected by the fact that there are non-constant maps hence surjective algebra homomorphisms .
]]>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 is the inclusion 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 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.
]]>(Just to be clear, here and are what are elsewhere called and respectively, right?)
]]>