Jean-Simon Pacaud Lemay - Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories

lmcs:4475 - Logical Methods in Computer Science, November 7, 2019, Volume 15, Issue 4 - https://doi.org/10.23638/LMCS-15(4:8)2019
Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore CategoriesArticle

Authors: Jean-Simon Pacaud Lemay ORCID

    A categorical model of the multiplicative and exponential fragments of intuitionistic linear logic ($\mathsf{MELL}$), known as a \emph{linear category}, is a symmetric monoidal closed category with a monoidal coalgebra modality (also known as a linear exponential comonad). Inspired by Blute and Scott's work on categories of modules of Hopf algebras as models of linear logic, we study categories of algebras of monads (also known as Eilenberg-Moore categories) as models of $\mathsf{MELL}$. We define a $\mathsf{MELL}$ lifting monad on a linear category as a Hopf monad -- in the Brugui{รจ}res, Lack, and Virelizier sense -- with a special kind of mixed distributive law over the monoidal coalgebra modality. As our main result, we show that the linear category structure lifts to the category of algebras of $\mathsf{MELL}$ lifting monads. We explain how groups in the category of coalgebras of the monoidal coalgebra modality induce $\mathsf{MELL}$ lifting monads and provide a source for such groups from enrichment over abelian groups. Along the way we also define mixed distributive laws of symmetric comonoidal monads over symmetric monoidal comonads and lifting differential category structure.


    Volume: Volume 15, Issue 4
    Published on: November 7, 2019
    Accepted on: June 4, 2019
    Submitted on: May 1, 2018
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1675 times.
    This article's PDF has been downloaded 430 times.