nLab linear-non-linear adjunction

Idea

A linear-non-linear adjunction is an adjunction between a cartesian and a non-cartesian monoidal categories:

Here $\mathbf{L}$ is symmetric monoidal, $\mathbf{M}$ is cartesian monoidal. The adjunction takes place in the 2-category of symmetric monoidal categories and lax monoidal functors, thus by doctrinal adjunction $L$ is in fact strong monoidal.

Such a situation forms the ground on which practically all categorical semantics of linear logic (of various kinds) are built. Specifically, the comonad $!=L M$ on $\mathbf{M}$ is the exponential modality of linear logic. A survey can be found in (Mellies ‘09, Chapter 7).

Related

• linear-non-linear logic

• LNL polycategory

References

• Paul-André Melliès, Categorical semantics of linear logic. Panoramas et syntheses, 27:15–215, 2009, (citeseerx)