Monoidal closure of Grothendieck constructions via Σ-tractable monoidal structures and Dialectica formulas
Fernando Lucatelli Nunes and Matthijs Vákár
我们研究了索引范畴𝖫𝖢^op→𝖢𝖠𝖳的格罗滕迪克构造Σ_𝖢𝖫的范畴结构。我们的分析从纤维极限、余极限和幺半（闭）结构的特征化开始。对纤维余极限的研究自然地引出了在CHAD中为表达性全语言引入的扩展索引范畴概念的推广，并产生了左Kan可扩展性的概念，这为计算格罗滕迪克构造中的余极限提供了一个统一框架。然后我们建立了总范畴Σ_𝖢𝖫的（非纤维）幺半闭包的充分条件。这扩展了哥德尔的Dialectica解释，并基于一个新的Σ-可处理幺半结构概念。在这一概念下，Σ-可处理余积统一并扩展了余笛卡尔余闭结构、双积和扩展余积。最后，我们考虑了诱导闭结构何时是纤维的，表明即使在存在纤维幺半结构的情况下，这通常也不成立。
We examine the categorical structure of the Grothendieck construction Σ_𝖢𝖫 of an indexed category 𝖫𝖢^op→𝖢𝖠𝖳. Our analysis begins with characterisations of fibred limits, colimits, and monoidal (closed) structures. The study of fibred colimits leads naturally to a generalisation of the notion of extensive indexed category introduced in CHAD for Expressive Total Languages, and gives rise to the concept of left Kan extensivity, which provides a uniform framework for computing colimits in Gro...