Wandering points

Stream: maths

[Yury G. Kudryashov]

I've just noticed that the definition of a wandering point of a group action in Wikipedia is incorrect. Take V = univ to see that every point is a wandering point according to this definition. I only used wandering points of self-maps, so never thought carefully about the right definition for a monoid/group action. Am I right that the correct definition is this one?

def MulAction.IsWanderingPoint (M : Type*) [One M] [TopologicalSpace M]
    {X : Type*} [TopologicalSpace X] [SMul M X] (x : X) : Prop :=
  ∀ V ∈ 𝓝 (1 : M), ∃ U ∈ 𝓝 x, ∀ g ∉ V, Disjoint (g • U) U

Also, should we have both the predicate and the set, or only one of them?

[Sébastien Gouëzel]

I think your definition makes sense. Another one would be: there exists a compact neighborhood V of the identity such that ..., but this one only makes sense in locally compact groups so your definition is better. It would be good to check that, in this case, the two definitions are equivalent, though.

[Yury G. Kudryashov]

I think that equivalence needs M to be a locally compact (monoid? group?) and X to be a locally compact topological space (didn't check all the details yet).

[Antoine Chambert-Loir]

I have looked up for definitions, but what you suggest does not seem to coincide with the definition given there, for example, http://arxiv.org/pdf/1608.06921v2,
of a non-wandering point of an action of a self-map

A point $p \in T^2$ is a non-wandering point for $f$ if for every neighborhood $B_p$ of $p \in T^2$ there exists an integer $n \geq 1$ such that $f_n(B_p) \cap B_p$ is nonempty.

or there https://math.stackexchange.com/questions/1719232/prove-a-group-action-is-wandering :

Definition: Let G be a topological group acting on a topological space X. The action is called wandering if for every 𝑥∈𝑋 there exists a neighborhood 𝑈𝑥 of 𝑥 such that the set {𝑔∈𝐺:(𝑔⋅𝑈𝑥)∩𝑈𝑥≠∅} is finite.

[Yury G. Kudryashov]

For the first definition, they coincide: in this case M = IterateAct f (isomorphic to Multiplicative Nat) and you can take V = {Multiplicative.ofAdd 0}. Note that I'm defining wandering points while the paper defines non-wandering points.

[Yury G. Kudryashov]

The second definition makes no sense, if G is something like Multiplicative Real, because this set will contain a neighbourhood of (1 : G).

[Yury G. Kudryashov]

I'm not sure what difficulties they avoid by allowing the set to be larger than {1} for a discrete group G.