带作用域计算路径的拓扑语义
Topological Semantics for Scoped Computational Paths
浏览论文内容
中文总结 AI 辅助
本文为带作用域的重写表示给出拓扑语义，构造带典范上域群胚结构的商箭头空间，证明拓扑一致性准则与充分条件，给出同伦类实现映射性质，以圆、环面为例分类，Lean开发包验证定理。
中文摘要 AI 辅助
计算路径将等式记录为原始步骤的显式有限迹。我们为一种带作用域的重写表示给出拓扑语义，其步骤具有连续的几何实现，且命名重写带有端点固定的同伦。对于每一种表示，我们构造一个商箭头空间，它具有典范的上域群胚结构：乘法在显式可复合代表元的商上是连续的。我们证明了一个精确的四方准则，用于判定该上域可复合拓扑是否与普通拉回拓扑一致，同时给出了紧豪斯多夫的充分条件。因此，无条件构造揭示而非隐藏了普通拓扑群胚中的积-商问题。到几何同伦类的实现映射是连续群胚态射，且仅在单独的几何完备性条件下是忠实的。在通用表示中，一个连续截面将协调路径商同胚地等同于通常带商拓扑的基本群胚。随后我们给出有限生成圆和实环面的例子，带有基于环绕的范式及由Z和Z²进行的分类。Lean 4.24.0开发包验证了定理包，数学表示独立于实现。
英文摘要
Computational paths record the steps of an equality derivation. We give them a topological semantics that distinguishes derivable rewrites from arbitrary homotopies. Coherent representatives pair traces with paths homotopic to their realizations. We compare a topology retaining the entire trace with one observing only endpoints, length, and paths. Quotienting by the declared rewrites gives a groupoid. Multiplication is continuous when composable pairs carry the quotient topology inherited from composable representatives. This topology can differ from the usual subspace topology on pairs of quotient arrows. We characterize when they agree, give compact-Hausdorff and discrete sufficient conditions, and use the Hawaiian earring to exhibit a failure of agreement. The comparison with geometric homotopy classes is injective exactly when the presentation is geometrically complete. Normal-form certificates give a criterion for completeness. In the universal presentation, all paths are primitive steps and all endpoint-fixed homotopies are allowed rewrites; its quotient recovers the quotient-topologized fundamental groupoid. Circle and torus examples recover the classical based-loop classifications by $\mathbb Z$ and $\mathbb Z^2$. A Lean development supports the construction. A focused Lean 4.32.0 result registered in Palomar covers the topology comparison, additive circle and torus classifications, and a conditional Hawaiian-earring obstruction transfer. We distinguish that result from the earlier Lean 4.24.0 development and from the mathematical exposition.
