Effros' theorem on transitive group actions with a glimpse into descriptive set theory
Jochen Wengenroth
TL;DR
The paper generalizes Effros' open-mapping result from metrizable settings to non-metrizable contexts by leveraging Suslin spaces and descriptive set theory. It establishes the openness and regularity of group-action orbits under Suslin-topology actions, and derives several open-mapping and factorization theorems in this broader framework. Additionally, it develops the measure-theoretic side by proving tightness and outer regularity for finite Borel measures on Suslin spaces. The work is framed as a self-contained introduction to descriptive set theory with applications to analysis, and it includes a Lean-formalized verification of the main result.
Abstract
The main aim of this note is to prove a version of a celebrated theorem of Effros about transitive group actions in a non-metrizable setting, these parts have been formalized and verified with Lean by Lara Toledano. We do not claim any originality since the given proof is in fact very close to one of van Mill. Our presentation is however completely self-contained and may serve as an appetizer to descriptive set theory. It also contains a few results about Suslin spaces (continuous images of separable completely metrizable spaces, which are often called analytic) which are extremely useful in measure theory.