An algebra modality admitting countably many deriving transformations

Fuente: arXiv
Saved in:
Bibliographic Details
Main Author: Vienney, Jean-Baptiste
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866916994495807488
author Vienney, Jean-Baptiste
author_facet Vienney, Jean-Baptiste
contents A differential category is an additive symmetric monoidal category, that is, a symmetric monoidal category enriched over commutative monoids, with an algebra modality, axiomatizing smooth functions, and a deriving transformation on this algebra modality, axiomatizing differentiation. Lemay proved that a comonoidal algebra modality has at most one deriving transformation, thus differentiation is unique in models of differential linear logic. It was then an open problem whether this result extends to arbitrary algebra modalities. We answer this question in the negative. We build a free "commutative rig with a self-map" algebra modality on the category of commutative monoids, where the self-map can be seen as an arbitrary smooth function. We then define a countable family of distinct deriving transformations $({}_{n}\mathsf{d})_{n \in \mathbb{N}}$ on this algebra modality where the parameter $n$ controls the derivative of the self-map. It shows that in a differential category, a single algebra modality may admit multiple, inequivalent notions of differentiation.
format Preprint
id arxiv_https___arxiv_org_abs_2510_03953
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle An algebra modality admitting countably many deriving transformations
Vienney, Jean-Baptiste
Category Theory
Logic in Computer Science
A differential category is an additive symmetric monoidal category, that is, a symmetric monoidal category enriched over commutative monoids, with an algebra modality, axiomatizing smooth functions, and a deriving transformation on this algebra modality, axiomatizing differentiation. Lemay proved that a comonoidal algebra modality has at most one deriving transformation, thus differentiation is unique in models of differential linear logic. It was then an open problem whether this result extends to arbitrary algebra modalities. We answer this question in the negative. We build a free "commutative rig with a self-map" algebra modality on the category of commutative monoids, where the self-map can be seen as an arbitrary smooth function. We then define a countable family of distinct deriving transformations $({}_{n}\mathsf{d})_{n \in \mathbb{N}}$ on this algebra modality where the parameter $n$ controls the derivative of the self-map. It shows that in a differential category, a single algebra modality may admit multiple, inequivalent notions of differentiation.
title An algebra modality admitting countably many deriving transformations
topic Category Theory
Logic in Computer Science
url https://arxiv.org/abs/2510.03953