Van Kampen 余极限与路径唯一性
Van Kampen Colimits and Path Uniqueness
AI总结：
本文提出在预层拓扑斯中高效检查 Van Kampen 性质的充要条件，基于路径状结构唯一性，补充了该性质的结构唯一性特征。
摘要：
纤维语义是软件工程中模型-实例模式的基础。软件模型通常可以被形式化为预层拓扑斯中的对象，即可以被表示为代数以及余代数的对象范畴，例如有向图范畴。多建模要求构造模型的余极限，分解由拉回给出。组合性要求这些运算之间存在精确的相互作用，即图表必须满足 Van Kampen 性质。然而，基于其定义以算法方式检查 Van Kampen 性质的有效性通常是不可行的。在本文中，我们陈述了在预层拓扑斯中 Van Kampen 性质成立的一个必要且充分但可高效检查的条件。该条件基于构成模型余极限余锥的定义同余类中路径状结构的唯一性性质。因此，我们在 Heindel 和 Sobociński 的陈述“成为 Van Kampen 是一个普遍性质”之上补充了以下事实：Van Kampen 性质揭示了基于预层的结构唯一性特征。
英文摘要：
Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, i.e, categories of objects that can be represented as algebras as well as coalgebras, e.g., the category of directed graphs. Multimodeling requires to construct colimits of models, decomposition is given by pullback. Compositionality requires an exact interplay of these operations, i.e., diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible. In this paper we state a necessary and sufficient yet efficiently checkable condition for the Van Kampen property to hold in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Sobociński the fact that the Van Kampen property reveals a presheaf-based structural uniqueness feature.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
