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 $(\mathcal{T},(R,+,\cdot))$ the line object $R$ is naturally regarded as a cartesian interval object.
If the lined topos $(\mathcal{T}, R)$ is also a smooth topos in that it satisfies the Kock-Lawvere axiom it makes sense to consider the subobject $D$ of $R$ defined as the equalizer
or equivalently expressed in topos logic as
and think of $D$ as the infinitesimal interval object of the smooth topos $(\mathcal{T},R)$ inside its finite interval object $R$. 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.
Urs Schreiber: the following should be checked
Recall the discussion at interval object of how the interval ${*}\sqcup {*} \stackrel{\to}{\to} R$ in $\mathcal{T}$ alone gave rise to the cosimplicial object
of (collared) $k$-simplices modeled on $R$, and how that induces for each object $X \in \mathcal{T}$ the simplicial object
Here as an object in $\mathcal{T}$ the $k$-simplex is actually a $k$-cube $\Delta_R^k := R^k$, but equipped with face and degeneracy maps that identify the boundary of a $k$-simplex inside the $k$-cube thus realizing the interior of that boundary as the $k$-simplex proper and the exterior as its collar .
We want to mimic that construction with the finite interval $R$ replaced by the infinitesimal interval object $D$, to get a simplicial object $\Pi^{inf}(X)$ for every object $X$.
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 $D$ typically has a unique morphism ${*} \to D$ 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 $X$ in the smooth topos $\mathcal{T}$ is therefore not as an element of $X^D$ but of $X^D \times D$, which we may think of as the space of pairs consisting of infinitesimal paths in $X$ and infinitesimal parameter lengths of these paths.
This naturally yields the span
where
the left leg is the projection $X^D \times D \to X^D$ followed by the tangent bundle projection $p_{T X} = X^{(* \to D)} : X^D \to X$
the right leg is the evaluation map, i.e. the inner hom-adjunct of $Id : X^D \to X^D$.
With this setup a pair of (generalized) elements $x,y \in X$ may be thought of as connected by an infinitesimal path if there is an element $(v,\epsilon) \in X^D \times D$ such that
and
But not all elements $(v,\epsilon)$ define different pairs of infinitesimal neighbour elements this way: specifically in the case that $X$ is a microlinear space, the tangent bundle object $X^D$ is fiberwise $R$-linear, and thus for any $t \in R$ the elements $(v,t \epsilon)$ and $(t v, \epsilon)$ define the same pair of infinitesimal neighbours, $x = v(0)$ and $y = (t v)(\epsilon) = v(t \epsilon)$.
We may identify such elements $(t v, \epsilon)$ and $(v, t \epsilon)$ by passing to the tensor product $X^D \otimes_R D$, i.e. the coequalizer of
where $\cdot$ here denotes the monoid-action of $(R,\cdot)$ on $D$ (by the embedding $D \hookrightarrow R$) and on $X^D$ (by the fact that $X$ is assumed to be microlinear).
In this same fashion we can then define infinitesimal analogs of the finite higher path object $X^{\Delta_R^k} = X^{R^{\times k}}$.
(infinitesimal path simplicial object)
Let $X \in \mathcal{T}$ be a microlinear space in the smooth topos $(\mathcal{T},R)$ with infinitesimal interval object $D$.
Then define the simplicial object
as follows:
in degree $n$ it assigns the object
whose generalized elements we write $(\epsilon_i v_i)_x$ with $\vec \epsilon \in D(n)$ or $(\nu_i)_x$ for short; where $x \in X$ indicates the fiber of $X^{D(n)} \to X$ that the element lives in
the face maps $d_i : (X^D \times_R D)^{\times_X^{n+1}} \to (X^D \times_R D)^{\times_X^{n}}$ are
for $0 \lt i \lt n+1$
given on generalized elements by
for $i = 0$
given by
where the element on the right denotes the evaluation of the map $(\nu_i) : D(n) \to X$ in its first argument on $\epsilon_0$, regarded as an element in the fiber over $v_0(\epsilon_0)$.
for $i = n+1$
given by
$d_{n+1} : (\nu_0, \cdots, \nu_{n+1}) \mapsto (\nu_0, \cdots, \nu_n)$
the degeneracy maps $\sigma_i$ act by inserting the 0-vector in position i:
$\sigma_i : (\ni_i) \mapsto (\nu_0, \cdots, \nu_{i-1}, 0, \nu_{i+1}, \cdots, \nu_{n})$.
These face and degeneracy maps indeed satisfy the simplicial identities.
This is straightforward checking that proceeds entirely analogously as the proof of the simplicial identities for the finite path $\infty$-groupoid $\Pi(X)$ discussed at interval object. See also the following remark.
By thinking of the $v_i : D \to X$ as infinitesimal collared curves in $X$ with source $v_i(0)$ and target $v_i(\epsilon_i)$ the above definition is an immediate analog of the definition of the path $\infty$-groupoid $\Pi(X)$ of finite paths as discussed at interval object.
This is made manifest by the following construction that embeds $\Pi^{inf}(X)$ into $\Pi(X)$.
Recall the finite path $\infty$-groupoid $\Pi(X)$ induced from the interval object
as discussed there. On object this assigns
(inclusion of infinitesimal into finite paths)
For $n \in \mathbb{N}$ define a morphism
on generalized elements by
These morphism $(\iota_n)$ respect the face and degeneracy maps on both sides and hence induce an inclusion of simplicial objects
Straightforward checking on generalized elements.
under construction
Let $X$ be a microlinear space.
Sketch of Proposition
We want to show that the morphism of simplicial sets
induced by pullback along $U \simeq U \times * \to U \times D$ is a weak homotopy equivalence.
Sketch of proof
First consider the case that $U$ itself has no infinitesimal directions in that $Hom(U,D) = *$. Then we claim that the morphism $[\Delta^{op},\mathcal{T}](U \times D, X^{(\Delta_\inf^\bullet)}) \to [\Delta^{op},\mathcal{T}](U , X^{(\Delta_\inf^\bullet)})$ is an acyclic Kan fibration in that all squares
have lifts.
For $n = 0$ this says that the map is surjective on vertices, which it is, since any $U \to X$ is in the image of $U \times D \to U \times * \simeq U \to X$.
For $n=1$ we need to check that every homotopy $U \to X^D \times D$ downstairs with fixed lifts $U \times D \to X$ over the endpoints may be lifted. But by assumption $U \to D$ factors through the point, so that the homotopy $U \to X^D \times D \stackrel{\to}{\to} X$ has the same source as target $f : U \to X$. This means the two lifts of its endpoints are morphisms $(u,\epsilon) \mapsto (f(u) + \epsilon \nu_i(u)$ for $i=1,2$ and $\nu_i$ tangent vectors. A homotopy between these is given by a map $U \times D \to X^D \times D$ defined by $(u,\epsilon) \mapsto (f(u)+ (-)\nu_1(u) + (\epsilon-(-))\nu_2(u), \epsilon)$.
Finally, for $n \geq 2$ we have unique flllers, because by construction every morphism $\Delta[n]\cdot Y \to X^{(\Delta^\bullet_{inf})}$ is uniquely fixed by the restriction $\partial \Delta[n] \to \Delta[n]\cdot Y \to X^{(\Delta^\bullet_{inf})}$ to its boundary.
The case for $U \times D$ replaced with $U \times D^n$ works analogously.