Paths and cylinders
Synthetic differential geometry
An infinitesimal interval object is like an interval object that is an infinitesimal space.
Where maps out of an interval object model paths that may arrange themselves into path ∞-groupoids, maps out of infinitesimal interval object model infinitesimal paths that may arrange themselves into infinitesimal path ∞-groupoid.
In any lined topos the line object is naturally regarded as a cartesian interval object.
If the lined topos is also a smooth topos in that it satisfies the Kock-Lawvere axiom it makes sense to consider the subobject of defined as the equalizer
or equivalently expressed in topos logic as
and think of as the infinitesimal interval object of the smooth topos inside its finite interval object . By the axioms satisfied by a smooth topos it is in particular an infinitesimal object.
Various constructions induced by a finite interval object have their infinitesimal analog for infinitesimal interval objects.
Infinitesimal path -groupoid induced from infinitesimal interval
Recall the discussion at interval object of how the interval in alone gave rise to the cosimplicial object
of (collared) -simplices modeled on , and how that induces for each object the simplicial object
Here as an object in the -simplex is actually a -cube , but equipped with face and degeneracy maps that identify the boundary of a -simplex inside the -cube thus realizing the interior of that boundary as the -simplex proper and the exterior as its collar .
We want to mimic that construction with the finite interval replaced by the infinitesimal interval object , to get a simplicial object for every object .
While the infinitesimal situation is formally very similar to the finite situation, one technical diference is that the infinitesimal interval does not fit into a nontrivial cospan as the finite interval does. This is because typically has a unique morphism from the terminal object, as a consequence of the fact that all the infinitesimal elements it contains are genuinely generalized elements.
The natural way to encode an infinitesimal path between two elements in an object in the smooth topos is therefore not as an element of but of , which we may think of as the space of pairs consisting of infinitesimal paths in and infinitesimal parameter lengths of these paths.
This naturally yields the span
the left leg is the projection followed by the tangent bundle projection
the right leg is the evaluation map, i.e. the inner hom-adjunct of .
With this setup a pair of (generalized) elements may be thought of as connected by an infinitesimal path if there is an element such that
But not all elements define different pairs of infinitesimal neighbour elements this way: specifically in the case that is a microlinear space, the tangent bundle object is fiberwise -linear, and thus for any the elements and define the same pair of infinitesimal neighbours, and .
We may identify such elements and by passing to the tensor product , i.e. the coequalizer of
where here denotes the monoid-action of on (by the embedding ) and on (by the fact that is assumed to be microlinear).
In this same fashion we can then define infinitesimal analogs of the finite higher path object .
(infinitesimal path simplicial object)
Let be a microlinear space in the smooth topos with infinitesimal interval object .
Then define the simplicial object
in degree it assigns the object
whose generalized elements we write with or for short; where indicates the fiber of that the element lives in
the face maps are
given on generalized elements by
where the element on the right denotes the evaluation of the map in its first argument on , regarded as an element in the fiber over .
the degeneracy maps act by inserting the 0-vector in position i:
This is straightforward checking that proceeds entirely analogously as the proof of the simplicial identities for the finite path -groupoid discussed at interval object. See also the following remark.
The inclusion of infinitesimal paths into finite paths
Recall the finite path -groupoid induced from the interval object
as discussed there. On object this assigns
(inclusion of infinitesimal into finite paths)
For define a morphism
on generalized elements by
These morphism respect the face and degeneracy maps on both sides and hence induce an inclusion of simplicial objects
Let be a microlinear space.
Sketch of Proposition
We want to show that the morphism of simplicial sets
induced by pullback along is a weak homotopy equivalence.
Sketch of proof
First consider the case that itself has no infinitesimal directions in that . Then we claim that the morphism is an acyclic Kan fibration in that all squares
For this says that the map is surjective on vertices, which it is, since any is in the image of .
For we need to check that every homotopy downstairs with fixed lifts over the endpoints may be lifted. But by assumption factors through the point, so that the homotopy has the same source as target . This means the two lifts of its endpoints are morphisms for and tangent vectors. A homotopy between these is given by a map defined by .
Finally, for we have unique flllers, because by construction every morphism is uniquely fixed by the restriction to its boundary.
The case for replaced with works analogously.