发表机构
U. of Massachusetts Lowell; U. of Denver（马萨诸塞大学洛厄尔分校; 丹佛大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明交换半群极小作用的区域近端与等连续结构关系为等价关系且重合，并利用自然扩张机制表明其最大等连续因子与嵌入群作用相同，且在Lean中完成形式化验证。
AI 中文摘要
区域近端和等连续结构关系是拓扑动力学中的基本关系，它们捕捉拓扑动力系统及其因子中的等连续行为。对于阿贝尔群的极小作用，这些关系已知是等价关系并且已知是重合的。在本文中，我们将这些事实推广到半群作用：对于交换半群的极小作用，区域近端和等连续结构关系是等价关系并且两者重合。我们还为通过满射作用的交换半群作用发展了自然扩张的机制，得出结论：交换半群的极小作用的最大等连续因子与其嵌入的群作用的最大等连续因子相同。我们在Lean中正式验证了本文的所有结果。主要结果在一个Palomar提交中得到了验证，并且我们链接到一个包含完整验证代码的Github仓库。
英文摘要
The regionally proximal and equicontinuous structure relations are fundamental relations in topological dynamics that capture the equicontinuous behavior in a topological dynamical system and its factors. For minimal actions of abelian groups, these relations are known to be equivalence relations and are known to coincide. In this paper, we generalize these facts to semigroup actions: for minimal actions of commutative semigroups, the regionally proximal and equicontinuous structure relations are equivalence relations and the two coincide. We also develop the machinery of natural extensions for commutative semigroup actions that act by surjections, concluding that the maximal equicontinuous factor of a minimal action of a commutative semigroup is the same as the maximal equicontinuous factor of the group action into which it embeds. We formally verify all of the results in this paper in Lean. The main results are verified in a Palomar submission, and we link to a Github repository containing code for the complete verification.
Comments43 pages; verification code at https://github.com/dglasscockUML/NSF_LEAPS
