Extracting an mathbb{N}-filtered differential modality from a differential modality

Jean-Baptiste Vienney

Pith reviewed 2026-05-10 07:11 UTC · model grok-4.3

classification 🧮 math.CT cs.LO

keywords differential modalitiesN-filtered comonadspolynomial mapsdifferential operatorsadditive symmetric monoidal categoriesdegree filtrationsmooth mapscomonad extraction

0 comments

The pith

Every differential modality on an additive symmetric monoidal category yields an N-filtered differential modality under mild conditions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a construction that turns any differential modality into a graded version. A differential modality consists of a comonad ! on an additive symmetric monoidal category together with a differential operator that lets morphisms out of !A stand for smooth maps from A. The graded version supplies a sequence of functors !≤n such that morphisms out of !≤n A stand for smooth maps from A whose degree is strictly less than n. This refinement is obtained directly from the original modality whenever certain mild conditions hold. The result matters because it equips the categorical model of smooth maps with an explicit notion of polynomial degree.

Core claim

We prove that under mild conditions, every differential modality on an additive symmetric monoidal category with underlying functor ! : C → C yields an N-filtered differential modality with underlying functors !≤n : C → C. A morphism f : !≤n A → B corresponds to a polynomial map of degree less than n from A to B, in the sense that the (n+1)-th derivative of f is 0.

What carries the argument

The family of functors !≤n obtained by filtering the single comonad ! according to the differential operator, so that each !≤n truncates maps to those whose (n+1)th derivative vanishes.

Load-bearing premise

The differential modality and the underlying additive symmetric monoidal category satisfy the mild conditions that let the extracted functors !≤n inherit the comonad and differential operator axioms.

What would settle it

A concrete differential modality on an additive symmetric monoidal category where the constructed !≤n fail to satisfy the comonad or differential operator axioms for the filtered structure.

read the original abstract

A differential modality is a comonad on an additive symmetric monoidal category $(\mathsf{C},\otimes,I)$, whose underlying functor we denote $!\colon\mathsf{C} \rightarrow \mathsf{C}$, together with some additional structure including a differential operator $\partial\colon!A \otimes A \rightarrow !A$. A morphism $f\colon !A \rightarrow B$ is interpreted as a smooth function from $A$ to $B$. The notion of an $\mathbb{N}$-filtered differential modality is a variant in which a notion of degree is present. Instead of a single functor $!\colon \mathsf{C} \rightarrow \mathsf{C}$, we ask for a family of functors $!_{\le n}\colon\mathsf{C} \rightarrow \mathsf{C}$ where $n \in \mathbb{N}$. Now, a morphism $f\colon !_{\le n} A \rightarrow B$ is interpreted as a smooth function from $A$ to $B$, with degree less than $n$ for some notion of degree. We prove that under mild conditions, every differential modality on an additive symmetric monoidal category with underlying functor $!\colon \mathsf{C} \rightarrow \mathsf{C}$ yields an $\mathbb{N}$-filtered differential modality with underlying functors $!_{\le n}\colon\mathsf{C} \rightarrow \mathsf{C}$. A morphism $f\colon !_{\le n}A \rightarrow B$ corresponds to a polynomial map of degree less than $n$ from $A$ to $B$, in the sense that the $(n+1)$-th derivative of $f$ is $0$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a direct construction turning any differential modality into an N-filtered one by iterating the differential operator to isolate bounded-degree maps.

read the letter

The main takeaway is that this paper extracts an N-filtered differential modality from a standard one. It defines the functors !≤n by applying the differential operator ∂ repeatedly together with the comonad counit and comultiplication, then shows these satisfy the filtered axioms and that the (n+1)th derivative vanishes on the resulting maps. The argument is plain diagram chasing that uses only the usual differential modality axioms plus additivity and symmetry of the monoidal structure. No extra data or fitting is introduced. That is the actual new piece: an explicit link between the two notions with a clear interpretation of morphisms as polynomials of degree less than n. The construction is straightforward and the verification steps line up without gaps or circularity. The mild conditions turn out to be the standard ones already required for a differential modality, so nothing surprising is hidden there. The result stays firmly inside differential categories and does not claim broader applications. That limits its reach, but within the subfield the extraction is useful and cleanly executed. A reader who already works with differential modalities or categorical models of differentiation will see the value right away. Someone outside that niche will find little to engage with. The paper is short, focused, and formally grounded enough to deserve referee time. I would send it for peer review.

Referee Report

0 major / 3 minor

Summary. The paper proves that under mild conditions, every differential modality (a comonad ! on an additive symmetric monoidal category together with a differential operator ∂ : !A ⊗ A → !A) yields an ℕ-filtered differential modality whose underlying functors !≤n are constructed explicitly from iterated applications of ∂, the counit, and comultiplication. Morphisms f : !≤n A → B are shown to be precisely the maps whose (n+1)th derivative vanishes, i.e., polynomial maps of degree less than n.

Significance. The result supplies an explicit, axiomatically grounded extraction of a filtered variant from any differential modality, thereby furnishing a categorical account of polynomial maps of bounded degree inside the same framework used for smooth maps. The construction relies only on the standard differential-modality axioms plus additivity and monoidal symmetry, with all verifications performed by direct diagram chasing; this directness and the absence of extra parameters or circularity constitute a clear technical strength.

minor comments (3)

§2 (or wherever the filtered comonad axioms are stated): the precise list of mild conditions on the original differential modality should be collected in a single numbered theorem statement rather than distributed across the construction and verification paragraphs.
Notation: the family !≤n is introduced before its explicit definition via the iterated differential; a forward reference or a displayed equation defining !≤n in terms of ∂^k, ε, and δ would improve readability.
The interpretation paragraph after the main theorem could usefully include a small commutative diagram illustrating how the (n+1)th derivative is obtained from the filtered structure.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and for recommending acceptance of the manuscript. The referee's summary accurately captures the main result: that every differential modality induces an ℕ-filtered differential modality under the stated mild conditions, with the explicit construction via iterated derivatives and the characterization of morphisms as polynomial maps of bounded degree.

Circularity Check

0 steps flagged

Direct construction with no circularity

full rationale

The paper defines the filtered functors !≤n explicitly via iterated application of the differential operator ∂ combined with the comonad counit and comultiplication, then verifies the filtered comonad axioms, restricted differential operator, and (n+1)th derivative vanishing by direct diagram chasing. All steps rely only on the given differential modality axioms plus additivity and symmetric monoidal structure; no self-definitional loops, fitted inputs renamed as predictions, load-bearing self-citations, uniqueness theorems imported from prior work, or ansatz smuggling appear. The derivation is self-contained against the stated assumptions.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on the standard axioms of category theory together with the definitions of additive symmetric monoidal categories and differential modalities (comonad plus differential operator).

axioms (2)

domain assumption The base category is additive symmetric monoidal
Explicitly required by the abstract for the differential modality to be defined.
domain assumption The differential modality consists of a comonad with differential operator ∂
Stated as the additional structure in the definition.

pith-pipeline@v0.9.0 · 5594 in / 1071 out tokens · 64658 ms · 2026-05-10T07:11:17.033651+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

7 extracted references · 5 canonical work pages

[1]

R. F. Blute, J. R. B. Cockett, J. S. P. Lemay, and R. A. G. Seely. Differential categories revisited. Applied Categorical Structures, 28(2):171–235, 2020.doi:10.1007/s10485-019-09572-y

work page doi:10.1007/s10485-019-09572-y 2020
[2]

R. F. BLUTE, J. R. B. COCKETT, and R. A. G. SEELY. Differential categories.Mathematical Structures in Computer Science, 16(6):1049–1083, 2006.doi:10.1017/S0960129506005676

work page doi:10.1017/s0960129506005676 2006
[3]

Bourbaki.Algebra I

N. Bourbaki.Algebra I. Springer Berlin, Heidelberg, 1989

1989
[4]

J.-S. P. Lemay and J.-B. Vienney. Graded differential categories and graded differential linear logic. 39th Conference on Mathematical Foundations of Programming Semantics, 2023. doi:10.46298/entics.12290. 42

work page doi:10.46298/entics.12290 2023
[5]

1998 , publisher =

S. MacLane.Categories for the Working Mathematician. Springer-Verlag, New York, 1971. Graduate Texts in Mathematics, Vol. 5.doi:10.1007/978-1-4757-4721-8

work page doi:10.1007/978-1-4757-4721-8 1971
[6]

Natural associativity and commutativity.Rice Institute Pamphlet - Rice University Studies, 49:28–46, 1963

Saunders Maclane. Natural associativity and commutativity.Rice Institute Pamphlet - Rice University Studies, 49:28–46, 1963

1963
[7]

Weibel, An Introduction to Homological Algebra Cambridge University Press (1994), [ doi:10.1017/CBO9781139644136 https://doi.org/10.1017/CBO9781139644136]

Charles A. Weibel.An Introduction to Homological Algebra. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1994.doi:10.1017/CBO9781139644136. A Deferred proofs Proof of (4.1.3):The proof is by induction onn≥0. •Base case (n= 0): We have∂ 0; ∆ = 1 !A; ∆ = ∆and the RHS is equal to(∆⊗1 I); (1!A⊗γ!A,I⊗ 1I);∂0⊗∂0 = ∆;∂0⊗∂0 = ∆; 1 !A⊗1!A =...

work page doi:10.1017/cbo9781139644136 1994