广义代数理论的范畴模型结构

中文摘要 AI 辅助

我们在Cartmell的广义代数理论（generalized algebraic theories，简称gats）范畴上构造了一个（组合的、幺半的、范畴富集的）Quillen模型结构；其同伦双范畴本质上由Taylor的带根显示映射范畴构成。这使我们能够比较gats的两类态射：一类严格保持种类依赖与代换，因此直接匹配语法；另一类则仅在同构意义上保持给定结构。我们证明了从上纤维化理论出发的态射的严格化结果，这类上纤维化理论是不含种类相等公理的理论的收缩。在此过程中，我们给出了语境范畴可在不含种类相等公理的情况下被表示的结构特征。我们的结果还表明，当限制到上纤维化对象时，gats的张量积具有预期的语义行为，即对应于配备了上纤维化生成弱分解系统的局部有限展示范畴的张量积。严格态射与弱态射分别对应gats模型A的两个熟知概念：一类取值于集合的迭代族，代换被解释为重索引；另一类是将语境范畴C(A)视为有限极限草图的集值模型。我们通过从A的语境投射范畴出发的某函子映射的无环条件，刻画了后一类模型的可严格化性。

英文摘要

We describe a (combinatorial, monoidal, Cat-enriched) Quillen model structure on the category of Cartmell's generalized algebraic theories (gats); its homotopy bicategory consists essentially of Taylor's rooted display map categories. This allows us to compare two kinds of morphisms of gats: one where sort dependency and substitution are preserved strictly, thus directly matching the syntax, and one where the given structure is preserved up to isomorphism. We prove a strictification result for morphisms out of cofibrant theories, which are the retracts of theories without sort equality axioms. Along the way, we give a structural characterization of when a contextual category can be presented without sort equality axioms. Our results also imply that when restricted to cofibrant objects, the tensor product of gats has the expected semantic behaviour, namely, it corresponds to the tensor product of locally finitely presentable categories equipped with a cofibrantly generated weak factorization system. Strict and weak morphisms specialize, respectively, to two familiar concepts of model of a gat A: ones valued in iterated families of sets, with substitution interpreted as reindexing, and set-valued models of the contextual category C(A) viewed as a finite-limit sketch. We characterize strictifiability of a model of the latter kind via a loop freeness condition on a certain map of functors out of the category of context projections of A.

补充信息

备注

59 pages