nLab graded Seely isomorphism

Idea

This is a generalization of the Seely isomorphism to graded modalities. A graded exponential modality $(!_{r}:\mathcal{C} \rightarrow \mathcal{C})_{r \in R}$ graded by some rig $R$ and in a CMon-enriched symmetric monoidal category $\mathcal{C}$ verifies the graded Seely isomorphism iff we have:

$$!_{r}(A \oplus B) \cong \underset{s+t=r}{\bigoplus} !_{s}A \otimes !_{t}A$$

One needs to combine graded linear logic? and differential linear logic to go from the usual Seely isomorphism of linear logic to the more general graded Seely isomorphism. The usual Seely isomorphism is obtained as a graded Seely isomorphism when one takes $R$ equal to the zero rig.

In sequent calculus

… to come …

In category theory

… to come …

Related concepts

• Seely isomorphism
• graded linear logic?

References

It will be discussed in a paper “Graded Differential Categories and Graded Differential Linear Logic” by JS Pacaud Lemay and J-B Vienney.