The regionally proximal relation for commutative semigroup actions
Angelina Blahodatna, Lauren Detmold, Daniel Glasscock, Anh N. Le
math.DS
Oct 7, 2026 · v1
TL;DR
All results on regionally proximal relations for commutative semigroup actions are formally verified in Lean, with main results submitted to Palomar and a GitHub repository.
Abstract
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.
Problem
For minimal actions of abelian groups, the regionally proximal and equicontinuous structure relations are known to be equivalence relations that coincide. The question is whether these facts extend to actions of commutative semigroups.
Approach
The regionally proximal relation RP and a backward variant RP^- are defined for semigroup actions. Their equality for minimal commutative semigroup actions is proved using a corner space, a simple instance of Host–Kra cubes, built from an S^2-action on X^3. A theory of natural extensions is developed for actions by surjections. Ultrafilters are used in place of enveloping semigroups and nets to simplify the Lean verification.
Results
For minimal commutative semigroup actions, RP and the equicontinuous structure relation are equivalence relations and coincide. The maximal equicontinuous factor equals that of the group action into which the semigroup action embeds. All results are verified in Lean.
