ora-0136

10.6.2 The first LINCS–UDL theorem

10.6.2 The first LINCS–UDL theorem

Theorem 10.4 Finite Kan accumulation and tangent stability

Under the declaration above:

  1. The pointwise enriched left Kan extension exists and

    \[ (\operatorname {Lan}_JF)(t)\cong \bigoplus _{s\le t}E_d. \]

    Applying \(\sigma _t\) to the revealed family gives

    \[ \left(\sum _{s\le t}Q_s,\, \sum _{s\le t}b_s,\, \sum _{s\le t}c_s\right). \]

  2. For a \(C^1\) family \(e_s(\theta )\), with fixed finite indexing shape, the canonical comparison

    \[ \chi _t^L: \bigoplus _{s\le t}T(E_d) \xrightarrow {\cong } T\left(\bigoplus _{s\le t}E_d\right) \]

    is an isomorphism and is compatible with the fold:

    \[ T(\sigma _t)\circ \chi _t^L=\sigma _t^T. \]

    Consequently,

    \[ D_\theta \left(\sum _{s\le t}e_s(\theta )\right)[v] = \sum _{s\le t}D_\theta e_s(\theta )[v]. \]
Proof ▼

The enriched pointwise formula is

\[ (\operatorname {Lan}_JF)(t) \cong \int ^{s\in \mathcal{O}_T}\mathcal{P}_T(Js,t)\otimes F(s). \]

This is the standard weighted-colimit formula for an enriched pointwise Kan extension [ Kelly , 1982 ] . The source category is discrete, so the coend has no nonidentity relations. Furthermore,

\[ \mathcal{P}_T(Js,t)\otimes F(s) \cong \begin{cases} E_d,& s\le t,\\ 0,& s{\gt}t. \end{cases} \]

The coend is therefore the finite coproduct \(\bigoplus _{s\le t}E_d\).

To see the universal property directly, let \(G:\mathcal{P}_T\to \mathbf{Vect}_k\). A transformation \(\alpha :F\Rightarrow J^\ast G\) provides maps \(\alpha _s:E_d\to G(s)\). For each \(s\le t\), compose with \(G(s\le t)\). The coproduct property yields a unique

\[ \overline\alpha _t: \bigoplus _{s\le t}E_d\longrightarrow G(t). \]

These maps are natural in \(t\), and their uniqueness is componentwise. They are exactly the factorization required by \(\operatorname {Lan}_J\dashv J^\ast \). Applying the linear fold to the registered local family yields the displayed cumulative statistic.

For the tangent claim, finite-dimensional vector spaces form an additive category and finite coproducts are biproducts. The standard tangent construction is \(T(V)\cong V\oplus V\), which preserves finite biproducts [ Cockett and Cruttwell , 2014 , Kock , 2006 ] . Hence

\[ \bigoplus _{s\le t}T(E_d) \cong T\left(\bigoplus _{s\le t}E_d\right). \]

Since \(\sigma _t\) is linear, its tangent folds base and tangent components separately. This proves the commuting comparison. Evaluation on the registered \(C^1\) evidence family gives the finite-sum derivative formula.

Remark 10.5 What the theorem actually says

The universal part constructs formal accumulation. Numerical accumulation is a declared algebra on that universal carrier. Omitting the fold would incorrectly identify a coproduct with vector addition.