一句话:证明线性范畴结构可提升到 MELL 提升单子的 Eilenberg-Moore 代数范畴,并给出由余代数群诱导提升单子的来源。
本文研究直觉主义线性逻辑的乘法与指数片段(MELL)的范畴模型。已知模型为线性范畴,即带幺半余代数模态(线性指数余单子)的对称幺半闭范畴。受 Blute 与 Scott 关于 Hopf 代数模范畴作为线性逻辑模型的工作启发,作者将单子的代数范畴(Eilenberg-Moore 范畴)视为 MELL 模型。论文定义线性范畴上的 MELL 提升单子:它是 Bruguières-Lack-Virelizier 意义的 Hopf 单子,并对幺半余代数模态满足特殊混合分配律。主要结果是线性范畴结构可提升到这类单子的代数范畴。作者进一步说明幺半余代数模态的余代数范畴中的群如何诱导 MELL 提升单子,并从阿贝尔群富集给出此类群的来源;还定义了相关混合分配律与微分范畴结构的提升。
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{\`e}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.Comment: An extend abstract version of this paper appears in the conference proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), under the title "Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories"
@article{paperbot744,
title = {Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories},
author = {Jean-Simon Pacaud Lemay},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:8)2019}
}