I don’t know if there is a slick modal homotopy theory proof of de Rham theorem (there is of the Stokes theorem, though, here).

But I’ll say that in the cohesive infinity-topos of smooth infinity-groupoids the role of the de Rham theorem is to be invisible:

Here is says that the infinity stack presented (under Dold-Kan followed by infinity-stackification) by the shifted and
truncated de Rham complexes (regarded as presheaves of chain complexes concentrated in degrees $\leq n$ with smooth functions in degree $n$ and de Rham differential going down from there) is equivalent to $\flat B^n \mathbb{R}$ – it’s just a nice presentation of the latter by a fibrant simplicial presheaf (Lemma 4.30 in *The Character Map in Twisted Non-Abelian Cohomology (schreiber)*).
And so forgetting about presentations and regarding only intrinsic stacky homotopy types the de Rham theorem becomes invisible.

But this presentation provides an atlas of $\flat B^n \mathbb{R}$ by the sheaf of closed $n$-forms, and the homotopy pullback of this atlas along the character mapis the moduli $\infty$-stack of ordinary differential cohomology in degree $n$.

That’s not what you were asking for, of course.

]]>I was wondering, does your approach here (or possibly related work) have a slick proof of de Rham’s theorem?

Once again, I am a real fan of your insights here. Thanks so much for your time. ]]>

Just notice that the infinitesimal interval has only a single point, so it’s not actually an “interval” (and the nLab entry that calls it an interval might want to be renamed or have a caveat added).

Also, when speaking about intervals being homotopy equivalences, one should really bring in cohesion to clarify the terminology:

In real cohesion we have the actual interval $[0,1]$, which is a non-contractible 0-type, And then there is its shape $Shp([0,1])$ and this what is contractible. hence which “is a homotopy equivalence from 0 to 1”.

In infinitesimal real cohesion we could moreover find the infinitesimal neighbourhood of $1/2$ in $[0,1]$. Its shape would, again, be contractible. But it doesn’t have endpoints, hence isn’t really an “interval”.

]]>Wow, I really like this view of geometry.

A somewhat separate thought:

In homotopy type theory, we can form an interval object in Type. Univalence requires this to be a homotopy equivalence.

This makes me wonder what univalence would mean in the infinitesimal case. Maybe the associated infinitesimal singular simplicial complexes would be homotopy equivalent in some sense?

]]>Maybe to clarify:

Functions out of the “first order infinitesimal disk”, algebraically given by your $(\mathfrak{m}/\mathfrak{m}^2)^*$, are equivalently Taylor series truncated at order 1, hence a value and a first derivative.

Functions out of the “second order infinitesimal disk”, algebraically given by $(\mathfrak{m}/\mathfrak{m}^3)^*$, are equivalently Taylor series truncated at order 2, hence a value, a first derivative and a second derivative.

…

Functions out of the “infinite order infinitesimal disk”, algebraiclly given by the filtered colimit over the $(\mathfrak{m}/\mathfrak{m}^n)^*$ (e.g. Prop. 3.7 in 1701.06238), are equivalently formal power series , hence a value, a first derivative, a second derivative, a third derivative, and so on, ad infinitum.

]]>The functions on the “infinitesimal singular simplicial complex” are equivalent to the de Rham complex! (See master thesis Stel for an account). So this gives higher form degree, but stays with first order derivatives.

To get higher order derivatives, turn attention to a close cousin of the infinitesimal simplicial complex: the jet bundle: Jet bundles are something like classifying spaces (or maybe co-classifying spaces) for higher order derivatives.

And they have a nice synthetic/homotopy-theoretic incarnation, too: they are formed by the jet comonad that is induced by base change along the unit of the infinitesimal shape modality.

]]>This is a basic question (my apologies), but I was wondering how an infinitesimal path between infinitesimal paths relates to second derivatives. Suppose I am working with a smooth manifold $M$ and I take $C^\infty (M)$. The infinitesimal paths on $M$ at the point $p: C^\infty (M) \rightarrow \mathbb{R}$ are identifiable with $(\mathfrak{m}/\mathfrak{m}^2)^*$, with $\mathfrak{m}$ the kernel of $p$. How do the infinitesimal paths between paths relate to the higher terms in the cotangent complex?

Thanks very much.

]]>*Here is what Kock writes (I guess there is no harm done in reproducing this here):*

the question you raise is interesting, and some theory does exist, but have not really been put together into a uniform theory, so far I know.

Let me quote some sources:

- Breen and Messing, Combinatorial differential forms, Advances in Math 164 (2001)
- Dubuc and Kock, On 1-form classifiers, Communications in Algebra 12 (1984)
- Dubuc, C^{\infty}-schemes, Amer. J. of Math. 103 (1981)
- Kock, Synthetic geometry of manifolds, Cambridge U.P., to appear (preprint version on my home page)
- Kumpera and Spencer, Lie Equations, Annals of Math. Studies 73 (1973)

[1] and [2] take the viewpoint of algebraic geometry that a "space" M is given by the ring A of functions on it (so spaces are affine schemes). In this case, the space M_(1) is given by (A tensor A)/I^2, where I is the kernel of the multiplication map A tensor A --> A. See e.g. [2] p. 1493. (This immediately leads to Kaehler's notion of the module of differential 1-forms, I/I^2, see [2].) However, as pointed out there, this only works for affine schemes. In algebraic geometry, the most interesting schemes are not affine (to wit: projective space), so instead of a ring of functions, one uses a sheaf or rings. [3] and [5] combine these viewpoints - in [3], you have topological spaces with a sheaf of C^{\infty} rings.

In [4] (p. 41 in the preprint version), I describe (in an axiomatic setting) a general "covariant" and a general "contravariant" determination of the neighbourhood relation on any object M; if M is a R^n (or a manifold), these two determinations agree. (I was interested in the case where the space is a function space, say R^R.)

The notion you describe is certainly good, and probably the unique good one, if one assumes that every function M-->R extends to a function R^n-->R.

]]>I have contacted Anders Kock asking him about that definition of the infinitesimal singular simplicial complex of a smooth locus. He says it's not in the literature explicitly as such but should make good sense.

Unwrapping it this should be pretty much verbatim the C^oo-ring analog of the construction of the simplicial object that Breen-Messing construct in their "Combinatorial differential forms" for affine schemes, i.e. for plain rings.

I'll try to work that relation out tomorrow, when I am more awake.

]]>All right, thanks Toby!

]]>Done. You can always move them back if you change your mind later!

]]>I am a bit embarrassed here that I created entries only to remove them a week later and move them to other pages. But the reason is that my thoughts about how to best organize this material were changing.

So, yes, if this is stabilizing now, and probably it is, then let's add a 'history' marker.

]]>Is there a reason not to make them redirects within Instiki? Are you going to put stuff on those pages again?

I'm inclined to add ‘history’ to their names and put redirects in infinitesimal interval object, but I won't if you have other plans.

]]>I have expanded infinitesimal singular simplicial complex now:

made the construction of the infinitesimal complex for smooth loci now a formal definition and its properties formal propositions. Also gave the inclusion map of infinitesimal simplices into finite one formally.

I decided that this discussion with the previous one at infinitesimal interval object now superceded the previous entry infinitesimal neighbour, so I made that redirect. I also made infinitesimal path infinity-groupoid in a smooth topos redirect to this.

]]>I couldn't get that relation between the above construction and Kock's infinitesimal singular simplicial complex to work. There must be some close relation, but I can't seem to be able to nail it down at the moment.

But I want the Kock-style definition at least for any smooth locus. There seems to be an obvious definition for that:

since any smooth locus X is a subobject of R^n, just say that elements of X are infinitesimal neighbours if they are after injection into R^n.

That seems so very obvious that it worries me a bit why that case is not in the literature. See what I typed now at

]]>I have typed into infinitesimal interval object a detailed description of the simplicial object inuced on a microlinear space from the infinitesimal interval in immediate analogy to the construction of the finite path simplicial object induced from an interval object (as discussed there).

I also give the inclusion of the infinitesimal simplicial object into the finite one.

All the proofs here are straightforward checking, which I think I have done rather carefully on paper, but not typed up. What I would appreciate, though, is if somebody gave me a sanity check on the definition of the infinitesimal simplicial object (which is typed in detail).

In the very last section, which is the one that is still just a sketch, I am hoping to describe an isomorphism from my simplicial infinitesimal object to that considered by Anders Kock, which is currently described at infinitesimal singular simplicial complex in the case that the space X satisfies Kock's assumptions (it must be a "formal manifold").

The construction I discuss at infinitesimal interval object is supposed to generalize Kock's construction to all microlinear spaces and motivated by having that canonical obvious inclusion into the finite version at interval object.

The isomorphism should be evident: my construction evidently yields in degree k k-tuples of pairwise first oder neighbours if the space X admits that notion. But I want to sleep over this statement one more night...

]]>