Additive Enrichment from Coderelictions

This paper demonstrates that even in a non-additive setting, the existence of a codereliction within a monoidal coalgebra modality inherently induces an additive enrichment via bialgebra convolution, thereby uniquely characterizing differential linear categories and establishing the uniqueness of coderelictions.

The Gist

Imagine you are trying to build a universal translator between two very different worlds: Computer Science (specifically, the logic behind how computers process information) and Calculus (the math of change, rates, and slopes).

For a long time, mathematicians thought that to translate "change" into the language of computers, you needed a very specific, heavy-duty foundation: a world where you could freely add things together, subtract them, and have a "zero" (like a blank slate). They called this an additive world.

This paper, written by Jean-Simon Pacaud Lemay, asks a simple but profound question: "Do we actually need that heavy foundation to define 'change' in the first place?"

Here is the story of the paper, explained without the jargon.

1. The Setup: The "Magic Box"

In the world of computer logic (specifically something called Linear Logic), there is a concept called a Coalgebra Modality. Think of this as a Magic Box.

• You put a piece of data (a "proof") into the box.
• The box spits out a version of that data that has been "exponentiated" or "duplicated" in a very specific way.
• In the old days, to make this box work with calculus, the box had to live in a world where you could add numbers. If you wanted to know how the box changed when you tweaked the input, you needed to be able to say, "This change plus that change equals a total change."

2. The Problem: The "Leibniz Rule"

In calculus, there is a famous rule called the Product Rule (or Leibniz rule). It says that if you have two things changing at once, the total change is the sum of their individual changes.

• Analogy: Imagine you are baking a cake. The taste depends on the sugar and the flour. If you change the sugar and the flour, the total change in taste is the sum of the sugar-change and the flour-change.
• To write this rule down in the computer logic, the old definitions required the ability to add and subtract. It seemed impossible to have a "differentiation" (a way to measure change) without a "plus" sign.

3. The Twist: The "Codereliction"

The paper focuses on a specific tool called a Codereliction.

• Analogy: Imagine the Magic Box is a complex machine. A Codereliction is a special "undo" button or a "linearization" tool. It takes a complex, non-linear process and flattens it out so you can see exactly how it reacts to a tiny nudge.
• The author noticed something strange: The rules that define this "undo" button (the Codereliction) don't actually use the plus sign. They only use the structure of the box itself.

So, the big question was: Can we have this "undo" button in a world where we can't add or subtract?

4. The Discovery: The "Self-Assembling" Foundation

The author proves a surprising result: No, you can't.

Even if you try to build a system where you don't have addition, the moment you install this "Codereliction" (the undo button), the system automatically builds addition for you.

• The Metaphor: Imagine you are building a house. You try to build it without a foundation, thinking you can just hang the walls in the air. But the moment you install the front door (the Codereliction), the laws of physics kick in, and a concrete foundation pours itself out of the door frame.
• The paper shows that the "Codereliction" acts like a mold. When you use it to measure change, it forces the computer logic to create "sums" and "zeros" out of thin air using a mathematical trick called convolution (which is like mixing ingredients in a specific recipe to get a new flavor).

The Result: You cannot have a "differentiable" system without an "additive" system. The ability to differentiate creates the ability to add.

5. The Bonus: The "Negative" Button

The paper goes one step further. What if you want to do subtraction? In math, that means having "negatives" (like -5).

• The author introduces a new concept called a Hopf Coalgebra Modality.
• Analogy: If the "Codereliction" is the button that creates addition, the Antipode (part of the Hopf structure) is the button that creates negatives.
• The paper proves that if your system has this "Antipode" button, you automatically get a world where you can subtract. If you don't have it, you can't.

6. The "Uniqueness" Surprise

Perhaps the most satisfying part of the paper is the conclusion about uniqueness.

• In many areas of math, there are many ways to define a concept. You might have five different ways to define "differentiation," and they all work slightly differently.
• The author proves that for this specific type of computer logic, there is only ONE way to differentiate.
• Analogy: Imagine trying to find the "true north" on a map. You might think there are many compasses, but this paper proves there is only one needle that points true north. If you have a system that allows differentiation, there is only one single, unique way to do it.

Summary: What Does This Mean?

1. Addition is Inevitable: You cannot define "change" (differentiation) in computer logic without also defining "addition." The ability to measure change forces the system to become additive.
2. Simpler Definitions: Because addition is forced to appear, we can now define these complex systems using fewer rules. We don't need to list "addition" as a separate requirement; the "change" rule brings it with it.
3. One True Path: There is only one correct way to differentiate non-linear proofs in this logic. It's not a matter of choice; it's a matter of mathematical necessity.

In a nutshell: The paper shows that the "magic" of calculus isn't just something you add to a computer system; it's a force that, once introduced, reshapes the entire system to support it. You can't have the derivative without the sum.

Technical Summary

Here is a detailed technical summary of the paper "Additive Enrichment from Coderelictions" by Jean-Simon Pacaud Lemay.

1. Problem Statement

The paper addresses a foundational question in the categorical semantics of Differential Linear Logic (DiLL): Is the additive enrichment (the ability to sum morphisms and have zero morphisms) an intrinsic, independent requirement for defining differential linear categories, or is it a consequence of other structural axioms?

• Context: Differential linear categories provide the semantics for the multiplicative and exponential fragments of DiLL. Traditionally, they are defined as symmetric monoidal categories enriched over commutative monoids (additive) equipped with a monoidal coalgebra modality (the exponential !) and a codereliction (a map $\eta: A \to !A$ representing differentiation).
• The Conflict: The axioms defining a codereliction (specifically the linear rule, chain rule, and monoidal rule) can be formulated without explicitly invoking sums or zero maps. Only the "constant rule" and "product rule" (Leibniz rule) historically required additive structure.
• The Question: Can one define a "non-additive" version of a differential linear category (i.e., in a general symmetric monoidal category without pre-existing sums) that still supports differentiation? If so, does the existence of a codereliction force the category to become additive?

2. Methodology

The author employs categorical algebra and string diagram calculus (graphical calculus for symmetric monoidal categories) to analyze the structural dependencies between coderelictions and additive enrichment.

• Intermediate Concepts:

  • Pre-codereliction: A natural transformation $\eta: A \to !A$ satisfying only the linear rule and the monoidal rule (excluding the chain rule). This allows the definition to be applied to a monoidal coalgebra modality without assuming additive structure.
  • Monoidal Bialgebra Modality: A generalization of the coalgebra modality where the object $!(A)$ possesses a compatible bimonoid structure (both comonoid and monoid structures). In additive settings, this structure arises naturally; in non-additive settings, it must be explicitly postulated to express the chain rule.
  • Bialgebra Convolution: The core mathematical tool used to construct sums. The paper utilizes the convolution product of a bialgebra to define addition on hom-sets.

• Logical Flow:

  1. Define pre-coderelictions and monoidal bialgebra modalities in a general symmetric monoidal category.
  2. Construct a sum operation ($+$) and a zero map ($0$) on the hom-sets using the bialgebra convolution of the monoidal bialgebra modality, pre-composed with the pre-codereliction and post-composed with the dereliction.
  3. Prove that these constructed operations satisfy the axioms of an additive symmetric monoidal category.
  4. Investigate the extension to Abelian groups (negatives) by introducing Hopf coalgebra modalities (bialgebras with an antipode).
  5. Revisit the full definition of differential linear categories to show that the existence of a codereliction implies the existence of the additive structure, rendering the "non-additive" definition equivalent to the standard additive one.

3. Key Contributions

A. Induction of Additive Enrichment (Main Theorem)

The paper proves that the existence of a pre-codereliction on a monoidal bialgebra modality is sufficient to induce an additive enrichment on the base category.

• Mechanism: The sum of two maps $f, g: A \to B$ is defined via the composite:
  $$f + g := \varepsilon_B \circ \nabla_B \circ (!f \otimes !g) \circ \Delta_A \circ \eta_A$$
  (where $\nabla$ is the multiplication of the bialgebra, $\Delta$ is the comultiplication, $\eta$ is the pre-codereliction, and $\varepsilon$ is the dereliction).
• Result: This construction turns the hom-sets into commutative monoids, satisfying all additive axioms (associativity, commutativity, unit, and compatibility with composition and tensor product).
• Significance: This demonstrates that additive structure is not an independent axiom but a derived property of the interaction between the bialgebra modality and the codereliction.

B. Uniqueness of Coderelictions

The paper establishes that coderelictions are unique for any monoidal coalgebra modality.

• Proof: Since pre-coderelictions are unique (proven via the monoidal rule and linearity), and a codereliction is a specific type of pre-codereliction, the codereliction itself must be unique.
• Implication: In any categorical model of Differential Linear Logic, there is exactly one way to differentiate non-linear (smooth) maps. This resolves ambiguity in modeling DiLL.

C. Characterization of Differential Linear Categories

The paper provides a novel, equivalent axiomatization of differential linear categories:

• New Definition: A differential linear category is a symmetric monoidal category with a monoidal bialgebra modality equipped with a codereliction.
• Advantage: This definition does not require the category to be pre-enriched over commutative monoids. The enrichment is a consequence of the other axioms.

D. Extension to Abelian Groups (Negatives)

The paper extends the results to categories enriched over Abelian groups (allowing subtraction).

• Hopf Coalgebra Modalities: It introduces monoidal Hopf coalgebra modalities, which include an antipode $S$.
• Result: A monoidal Hopf coalgebra modality with a pre-codereliction induces an Abelian group enrichment. The negative of a map $-f$ is constructed using the antipode: $-f := \varepsilon \circ S \circ !f \circ \eta$.
• Equivalence: It proves that an additive bialgebra modality has an antipode if and only if the base category has negatives, linking the algebraic property of the modality directly to the categorical property of the hom-sets.

4. Key Results

1. Theorem 5.1: A monoidal bialgebra modality with a pre-codereliction induces an additive symmetric monoidal category structure via bialgebra convolution.
2. Proposition 3.3: Pre-coderelictions are unique.
3. Theorem 8.1: A differential linear category is equivalently a symmetric monoidal category with a monoidal bialgebra modality equipped with a codereliction (removing the explicit requirement for additive enrichment in the definition).
4. Theorem 8.3: Coderelictions are unique for any monoidal coalgebra modality.
5. Proposition 7.3 & Lemma 7.5: The existence of an antipode in the modality is equivalent to the existence of negatives in the base category.

5. Significance

• Foundational Clarification: The paper resolves a long-standing ambiguity regarding the necessity of additive axioms in the definition of differential categories. It shows that the "additive" nature of differentiation is not an external constraint but an internal consequence of the codereliction interacting with the bialgebra structure.
• Simplification of Axioms: By showing that additive enrichment is induced, the definition of differential linear categories can be streamlined. One no longer needs to assume the category is additive; one only needs to assume the existence of the modality and the codereliction.
• Uniqueness of Differentiation: The proof of uniqueness for coderelictions is a major theoretical result. It implies that in the categorical semantics of DiLL, the concept of "differentiation" is rigid and canonical; there are no alternative, non-equivalent ways to define the derivative of a smooth map within these models.
• Bridge to Hopf Algebras: The work deepens the connection between Linear Logic and Hopf algebra theory, showing how the presence of an antipode (Hopf structure) corresponds precisely to the ability to perform subtraction in the logic.

In summary, Lemay demonstrates that coderelictions generate additive structure. This unifies the algebraic and categorical perspectives on differentiation, proving that the ability to differentiate non-linear maps inherently forces the underlying logical framework to support addition and, if an antipode is present, subtraction.