Borel Jet Extensions

Abstract

We develop the theory of Borel jet extensions within $\mathbf{Gpd}_{\infty}$ of groupoids and higher toposes. Equality is treated as a path space, in accordance with the groupoid hypothesis. Recursive constructions of jets and their smooth realizations are internalized in Martin-Löf intensional type theory, yielding homotopical interpretations of formal specifications. Jet-order optimization is the case in which a descent step is a partial map on a finite truncation of the Borel jet: the Borel map is an algebra homomorphism, methods factor through that truncation, and naturality under coordinate change is the Faà di Bruno formula.

1. Definitions

1.1 Borel jet

Let $E$ be a smooth manifold and $p\in E$ . The Borel jet $j^{\infty}_{p}(f)$ of a smooth function $f\colon E\to\mathbb{R}$ at $p$ is the formal power series

j^{\infty}_{p}(f)=\sum_{\alpha\in\mathbb{N}^{n}}\frac{1}{\alpha!}\,\partial^{\alpha}f(p)\,x^{\alpha}

(1)

in the stalk of the structure sheaf. Equivalently, it is the image of $f$ under the Borel map

B_{p}\colon C^{\infty}(E)\longrightarrow\mathbb{R}[[x_{1},\ldots,x_{n}]]

(2)

1.2 Borel jet extension

A Borel jet extension of a formal series $s\in\mathbb{R}[[x]]$ is a smooth function $f$ such that $j^{\infty}_{p}(f)=s$ . Borel’s theorem asserts that every formal series admits such an extension in the $C^{\infty}$ category — that is, in non-quasianalytic classes. The extension is a right inverse of the Borel map:

B_{p}\circ\operatorname{ext}=\mathrm{id}

(3)

Flat functions account for the failure of uniqueness: the kernel of $B_{p}$ is nontrivial, so the path from a series to a realization is a space, not a point.

1.3 Higher categorical setting

Let $\mathbf{Gpd}_{\infty}$ be any model of $\infty$ -categories of groupoids — quasi-categories, complete Segal spaces, and the like — satisfying the groupoid hypothesis: the identity type is a path space, and higher equalities are higher paths. A Borel jet extension is an object of the $\infty$ -category of formal series together with a path, an equality, to a smooth realization.

Equality as a path

Formal series

$s$

\mathsf{Id}

path

Smooth realization

$f$

2. Theorems

Theorem 2.1 Internalization

Every recursive specification of a Borel jet and its extension interprets as a higher homotopy type in a model of homotopy type theory.

Proof. Martin-Löf intensional type theory provides inductive types for the jet data — the coefficients of the formal series — and recursive definitions for the extension term. The identity type $\mathsf{Id}$ supplies the path space of equalities between the formal jet and its realization. Higher coherences arise as higher paths, yielding the required homotopical structure. Conservative extensions of recursive terms remain inside the inductive-recursive fragment, preserving the interpretation.

Theorem 2.2 Groupoid-hypothesis compatibility

The construction is independent of the choice of model of $\infty$ -categories, provided the model respects the groupoid aspect of equality.

Proof. All standard models of $\infty$ -categories — Joyal quasi-categories, Lurie $\infty$ -categories, Rezk complete Segal spaces — are equivalent on groupoids and implement equality via path spaces. The Borel map and its right inverse, the extension, are functors that preserve these path spaces, hence the higher homotopical data are transported equivalently.

3. Application to formal specifications

Any formal development whose constructions are inductive or recursive admits a homotopical reading: each recursive clause defines a term, each equality is a path, and the specification as a whole is a homotopy type.

This applies in particular to the axis-regularity jets appearing in constructions of singular solutions of the Navier–Stokes equations, where right jets at the axis ensure Cartesian smoothness.

4. Optimization by jet order

An optimization step that consults derivatives only up to order $k$ is an algebraic operation on a truncation of the Borel jet. This section records the algebra, the resulting class of algorithms, and the sense in which a descent step is a path. Nothing here is a convergence rate: factorization and naturality are formal, not analytic. The construction is also not Borel summation, which assigns sums to divergent series and is not used.

Proposition 4.1 Algebra of the Borel map

The Borel map is a homomorphism of commutative unital $\mathbb{R}$ -algebras. It intertwines partial differentiation with formal differentiation of series. Its kernel is the ideal of flat germs. If $\varphi$ is a diffeomorphism germ with $\varphi(p)=p$ , jets compose by the Faà di Bruno formula.

\begin{aligned} B_{p}(f+g)&=B_{p}(f)+B_{p}(g),\\ B_{p}(fg)&=B_{p}(f)\,B_{p}(g). \end{aligned}

(4)

B_{p}(\partial_{i}f)=\partial_{i}B_{p}(f)

(5)

\begin{aligned} j^{k}_{p}&=\pi_{\le k}\circ B_{p},\\ \pi_{\le k}&\colon\mathbb{R}[[x]]\longrightarrow\mathbb{R}[[x]]/\mathfrak{m}^{k+1}. \end{aligned}

(6)

B_{p}(f\circ\varphi)=B_{p}(f)\circ B_{p}(\varphi)

(7)

Proof. Linearity of differentiation gives additivity. The Leibniz rule gives multiplicativity, and constants are fixed, so $B_{p}$ is a unital algebra homomorphism. The coefficient of $x^{\alpha}$ in $B_{p}(f)$ is $\partial^{\alpha}f(p)/\alpha!$ , so formal differentiation of the series reproduces $B_{p}(\partial_{i}f)$ . The kernel is the set of germs with every derivative zero at $p$ , an ideal because a product with a smooth germ still has vanishing derivatives. Faà di Bruno is the chain rule at every order, packaged as composition in $\mathbb{R}[[x]]$ , once both series are centered at $p$ .

Definition 4.2 Jet-order method

A jet-order method of order $k$ is a partial map $\Phi_{k}$ from the truncated jet space $P_{k}=\mathbb{R}[[x]]/\mathfrak{m}^{k+1}$ to the tangent space, defined by polynomial equations in the jet coefficients, together with the recursion

x_{t+1}=x_{t}+\Phi_{k}\!\left(j^{k}_{x_{t}}(f)\right)

(8)

The method is jet-pure when $\Phi_{k}$ depends on no structure beyond the jet. It is structured when it also depends on a chosen metric or norm. Partiality records the open condition that a minor be invertible; several roots of the same polynomial system are several paths, not a failure of the algebra.

Order 1 · structured
Gradient descent
$\Phi_{1}=-\eta\,g^{\sharp}(df)$
The 1-jet supplies $df$ . A metric $g$ raises the index. Changing the metric changes the step, so the method is not a function of the jet alone.
Order 2 · jet-pure
Newton
$\Phi_{2}(j^{2}f)=-(\nabla^{2}f)^{-1}\nabla f$
Defined where the Hessian is invertible. The step is the inverse, in the matrix algebra, of the linear part of $\nabla f$ . No auxiliary metric enters.
Order ≥ 3
Taylor models and tensor steps
The degree- $k$ Taylor polynomial is the class $j^{k}f$ . A critical point of that polynomial in the displacement is jet-pure, and generally multi-valued. Cubic regularization minimizes the same polynomial plus a penalty built from a chosen norm, so it is structured in the same sense as gradient descent.

Proposition 4.3 Factorization and affine naturality

An order- $k$ step depends on the objective only through $j^{k}_{p}$ . In particular it is unchanged by addition of a germ flat at the current point. Newton’s method is natural under affine coordinate changes: if $\varphi(x)=Ax+b$ with $A$ invertible, the displacement transforms by $(D\varphi)^{-1}$ .

\Phi_{2}(j^{2}(f\circ\varphi))=(D\varphi)^{-1}\Phi_{2}(j^{2}f)

(9)

Proof. By definition $\Phi_{k}$ takes a class in $P_{k}$ , and $j^{k}_{p}=\pi_{\le k}\circ B_{p}$ , so germs congruent modulo $\mathfrak{m}^{k+1}$ produce the same step. A flat germ lies in every power of the maximal ideal. For the affine claim, the gradient and Hessian transform by $g\mapsto A^{\mathsf{T}}g$ and $H\mapsto A^{\mathsf{T}}HA$ . Then $(A^{\mathsf{T}}HA)^{-1}A^{\mathsf{T}}g=A^{-1}H^{-1}g$ , which is (9). Naturality can fail for a general diffeomorphism: derivatives of $\varphi$ beyond order one appear in Faà di Bruno, and Newton does not consult them. Gradient descent is natural only for isometries of its metric.

Flatness at the current point does not constrain the jet at the next iterate. Agreement is one step at a time, unless the two objectives remain congruent modulo $\mathfrak{m}^{k+1}$ along the orbit.

Theorem 4.4 Descent is transport

A jet-order recursion interprets as a recursive term on the inductive type of coefficients of degree at most $k$ . Identity of $k$ -jets induces identity of steps by transport. A Borel extension of a formal displacement, when the step map extends along the tower of truncations, realizes the recursion as a smooth path.

Proof. Coefficients of degree $\le k$ are a finite product of copies of the ground ring, hence an inductive type. $\Phi_{k}$ is defined by polynomial equations on that type, so it is a term of the theory. Given a path $\mathsf{Id}(j^{k}(f),j^{k}(\tilde f))$ , transport of the displacement along that path is the identity of steps, because both sides are $\Phi_{k}$ of the same class in $P_{k}$ . If a coherent family of steps $(\Phi_{k})_{k}$ defines a formal series of displacements, Theorem 2.1 supplies a smooth realization. The realization is a path in the space of points; reparameterizations of step size are higher paths. Distinct roots of the same jet equations are distinct path components, which is the groupoid reading of a multi-valued higher-order step.

Where a step reads the jet

Smooth objective
$f$
Borel map
$B_{p}$
Formal series
$\mathbb{R}[[x]]$
Truncation
$\pi_{\le k}$
Order-k step
$\Phi_{k}$

5. Conclusion

The theory of Borel jet extensions is fully compatible with higher categorical and homotopy-theoretic foundations. Recursive constructions are canonically interpreted in Martin-Löf type theory, furnishing higher homotopical structure that can be analyzed within any model conforming to the groupoid hypothesis. Jet-order optimization is the same pattern: a descent step factors through a truncation of the Borel jet, naturality is composition of series, and equality of steps is transport along a path of jets.

Borel jet extensions via higher categories and homotopy type theory