lin-0106

8.2 Internal model spaces and parametrized maps

The finite-product formalism of functorial backpropagation begins with a parametrized smooth map

\[ f:P\times X\longrightarrow Y. \]

This is enough to compose parameterized modules: serial composition combines parameter spaces, and the monoidal product places modules in parallel [ Fong et al. , 2019 ] . It is not, however, enough for the semantics intended here. In the category of finite-dimensional smooth manifolds, the exponential object \(Y^X\) generally does not exist. Consequently, one cannot in general internalize the same family as a morphism

\[ \widehat f:P\longrightarrow Y^X. \]

Deep LINCS therefore takes its primary ambient semantics to be a suitable smooth topos \(\mathcal E\), following the Kock–Lawvere approach to synthetic differential geometry [ Kock , 2006 , Lawvere , 1980 , Moerdijk and Reyes , 1991 ] . Cartesian closedness supplies the natural bijection

\[ \mathcal E(P\times X,Y) \; \cong \; \mathcal E(P,Y^X), \]

so a parameterized implementation is equivalently an internal map into the space of models. The parameter object \(P\) need not equal all of \(Y^X\); the transpose \(\widehat f\) records which internal family of models is available. This is the same structural role played by internal function spaces in topos causal models.

The smooth topos and the tangent structure do different jobs. Cartesian closure supplies internal function spaces and currying. Infinitesimal structure supplies an object \(D\) and, on the appropriate infinitesimally linear or microlinear objects, a tangent construction represented by \(TX=X^D\). A general tangent category need not be Cartesian closed; DLINCS requires these structures to coexist compatibly rather than deriving either one from the other.

Write \(\mathbf{Para}_{\mathcal E}\) for the category whose parametrized arrows are pairs \((P,f)\) internal to \(\mathcal E\), modulo the chosen isomorphisms of parameter objects, and abbreviate it to \(\mathbf{Para}\) below. The finite-dimensional Euclidean category of parametrized maps is a computational realization of this semantics, not its categorical foundation. A feed-forward network becomes a composite

\[ X \xrightarrow {f_{\theta _1}} H_1 \xrightarrow {f_{\theta _2}} \cdots \xrightarrow {f_{\theta _L}} Y, \]

while branches, skip connections, adapters, critics, and local predictors are represented by a richer symmetric monoidal graph.

Definition 8.1 Smooth learner

A smooth learner from \(X\) to \(Y\) is a tuple

\[ (P,I,U,r), \]

consisting of an implementation \(I:P\times X\to Y\), an update

\[ U:P\times X\times Y\longrightarrow P, \]

and a request map

\[ r:P\times X\times Y\longrightarrow X. \]

The update changes local parameters; the request communicates desired change to the preceding interface.

Internally, the three displayed arrows are morphisms of \(\mathcal E\). Cartesian closedness makes the implementation a map \(P\to Y^X\), while a compatible reverse differential or reverse tangent structure supports the update and request operations. In the finite-dimensional Euclidean realization, a chosen loss and step size recover the functorial backpropagation construction of Fong et al. [ 2019 ] . That construction is an important operational model of DLINCS, but the internal smooth-topos semantics is strictly stronger than its finite-product baseline.