Poles of group actions

DefinitionPoles of a group action#✓fully proved

A pole of a group action is a point fixed by some nonidentity element.

def poles (G : Type*) (X : Type*) [Group G] [MulAction G X] : Set X :=
  {x : X | ∃ g : G, g ≠ 1 ∧ g • x = x}

Used by 4

Used byThe poles are invariant under the action · Characterization of poles · The poles as a union of fixed-point sets · The action sends poles to poles

TheoremCharacterization of poles#✓fully proved

Let a group \(G\) act on a set \(X\). A point \(p \in X\) is a pole of the action if and only if there is some \(g \in G\) with \(g \neq 1\) and \(g \cdot p = p\).

theorem mem_poles {p : X} : p ∈ poles G X ↔ ∃ g : G, g ≠ 1 ∧ g • p = p

Uses 1

Statement usesPoles of a group action

TheoremThe action sends poles to poles#✓fully proved

Let a group \(G\) act on a set \(X\). If \(p \in X\) is a pole of the action, then \(g \cdot p\) is a pole for every \(g \in G\).

If \(p\) is fixed by \(h \neq 1\), then \(g \cdot p\) is fixed by the conjugate \(g h g^{-1} \neq 1\).

theorem smul_mem_poles (g : G) {p : X} (hp : p ∈ poles G X) :
    g • p ∈ poles G X

Uses 1 · Used by 1

Statement usesPoles of a group action

Used byThe poles are invariant under the action

TheoremThe poles are invariant under the action#✓fully proved

Let a group \(G\) act on a set \(X\) and let \(P \subseteq X\) be the set of poles of the action. For every \(g \in G\), the image of \(P\) under the map \(x \mapsto g \cdot x\) is \(P\).

theorem image_smul_poles (g : G) : (g • ·) '' poles G X = poles G X

Uses 2

Statement usesPoles of a group action

Proof usesThe action sends poles to poles

TheoremThe poles as a union of fixed-point sets#✓fully proved

Let a group \(G\) act on a set \(X\). The set of poles equals \(\bigcup_{g \in G,\, g \neq 1} \{x \in X : g \cdot x = x\}\), the union of the fixed-point sets of the nonidentity elements of \(G\).

theorem poles_eq_iUnion_fixedBy :
    poles G X = ⋃ g ∈ {g : G | g ≠ 1}, MulAction.fixedBy X g

Uses 1

Statement usesPoles of a group action

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.