从依赖类型理论到高阶代数结构
摘要:本论文的第一部分定义了“依赖类型代数理论”,它是Cartmell广义代数理论(GATs)的一个严格子类。我们将依赖类型代数理论刻画为在某些预层范畴上的有限单子范畴,推广了Lawvere、B''enabou和Linton针对普通多元排序代数理论的一个著名结果。我们利用这一结果识别了依赖类型代数理论在一些代数结构类中的应用,例如小范畴、n-范畴、严格和弱ω-范畴、平面彩色操作符和opetopic集合。然后我们证明了每个局部有限表示范畴都是某个依赖类型代数理论的模型范畴。因此,就其集合模型而言,这些理论与GATs、本质代数理论和有限极限草图同样具有表达能力。然而,依赖类型代数理论通过对简单预层上全局模型结构的左Bousfield局部化,提供了对空间中同伦模型的良好定义。一些情况下(如特定的“幂等opetopic理论”),同伦模型与(严格)单纯模型之间存在一个刚性化定理。 本论文的第二部分关注可表示($(\infty,1)$-范畴的局部化)。我们给出了“pre-modulator”的定义,并证明了每个可达到的正交分解系统都可以通过迭代类似于层化的加性构造从pre-modulator产生。我们给出了“modulator”和“left-exact modulator”的定义,并证明了它们对应于那些满足模态性和左精确模态性的分解系统。因此,每个$infty$-topos的左精确局部化都可以通过迭代与左精确modulator相关的加性构造获得。
作者:Chaitanya Leena Subramaniam
论文ID:2110.02804
分类:Category Theory
分类简称:math.CT
提交时间:2021-10-07