Orbits of a finitely generated group, computed

Let a group G act on a finite type α with decidable equality, and let S : Finset G. The orbit of a point x under the subgroup Subgroup.closure ↑S generated by S is a finite set, but Mathlib's MulAction.orbit offers no way to compute it: membership in Subgroup.closure ↑S carries no Decidable instance, and the subgroup itself is not a finset. This file computes the orbit by the usual closure procedure — start from {x}, and repeatedly add all translates by the generators — and proves that the result is the orbit. Since each round either enlarges the current finset or leaves it fixed forever, Fintype.card α rounds always suffice (Finset.isFixedPt_iterate_card), so the definition iterates that many times and is executable by decide and #eval.

Applied to a group acting on itself by left multiplication, the orbit of 1 is the subgroup generated by S; this gives the generated subgroup as a finset, and its order as a computation.

Main definitions

• Finset.orbitStep S s: one round of closure, the finset s ∪ S • s.
• Finset.orbitFinset S x: the orbit of x under Subgroup.closure ↑S, as a finset.
• Finset.closureFinset S: the subgroup Subgroup.closure ↑S of a finite group, as a finset.

Main results

• Finset.coe_orbitFinset, Finset.mem_orbitFinset: the finset is the orbit of x under the subgroup generated by S.
• Finset.isPretransitive_closure_iff_orbitFinset_eq_univ: the generated subgroup acts transitively exactly when the computed orbit of a point is everything. This is what makes transitivity of a finitely generated permutation group decidable.
• Finset.mem_closureFinset, Finset.card_closureFinset: the finset presentation of the generated subgroup, and its order.

def Finset.orbitStep {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] (S : Finset G) (s : Finset α) : Finset α

One round of closure of a finset s under the group elements in S: the finset s together with all translates g • y of its elements by generators g ∈ S.

Equations

• S.orbitStep s = s ∪ S • s

@[simp]

theorem Finset.mem_orbitStep {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] {S : Finset G} {s : Finset α} {y : α} : y ∈ S.orbitStep s ↔ y ∈ s ∨ ∃ g ∈ S, ∃ x ∈ s, g • x = y

theorem Finset.subset_orbitStep {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] (S : Finset G) (s : Finset α) : s ⊆ S.orbitStep s

theorem Finset.smul_finset_subset_orbitStep {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] {S : Finset G} {g : G} (hg : g ∈ S) (s : Finset α) : g • s ⊆ S.orbitStep s

def Finset.orbitFinset {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] (S : Finset G) (x : α) : Finset α

The orbit of x under the subgroup generated by S, computed by Fintype.card α rounds of closure under the generators starting from {x}. That many rounds always suffice, by Finset.isFixedPt_iterate_card; the identification with MulAction.orbit is Finset.coe_orbitFinset.

Equations

• S.orbitFinset x = S.orbitStep^[Fintype.card α] {x}

theorem Finset.orbitStep_orbitFinset {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] (S : Finset G) (x : α) : S.orbitStep (S.orbitFinset x) = S.orbitFinset x

The computed orbit is closed under one more round of closure.

@[simp]

theorem Finset.mem_orbitFinset_self {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] (S : Finset G) (x : α) : x ∈ S.orbitFinset x

@[simp]

theorem Finset.coe_orbitFinset {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] (S : Finset G) (x : α) : ↑(S.orbitFinset x) = MulAction.orbit (↥(Subgroup.closure ↑S)) x

The computed orbit is the orbit of x under the subgroup generated by S.

@[simp]

theorem Finset.mem_orbitFinset {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] {S : Finset G} {x y : α} : y ∈ S.orbitFinset x ↔ y ∈ MulAction.orbit (↥(Subgroup.closure ↑S)) x

A point lies in the computed finset Finset.orbitFinset S x exactly when it lies in the orbit of x under the subgroup generated by S.

theorem Finset.isPretransitive_closure_iff_orbitFinset_eq_univ {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] (S : Finset G) (x : α) : MulAction.IsPretransitive (↥(Subgroup.closure ↑S)) α ↔ S.orbitFinset x = univ

The subgroup generated by S acts transitively exactly when the computed orbit of a point is the whole type.

theorem Finset.isPretransitive_closure_iff_forall_orbitFinset_eq_univ {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] (S : Finset G) : MulAction.IsPretransitive (↥(Subgroup.closure ↑S)) α ↔ ∀ (x : α), S.orbitFinset x = univ

The subgroup generated by S acts transitively exactly when the computed orbit of every point is the whole type. The universally quantified form is the one that is decidable without choosing a point.

The generated subgroup of a finite group, as a finset

def Finset.closureFinset {G : Type u_1} [Group G] (S : Finset G) [Fintype G] [DecidableEq G] : Finset G

The subgroup of a finite group generated by S, as a finset: the orbit of 1 under the generated subgroup acting by left multiplication, computed by Finset.orbitFinset.

Equations

• S.closureFinset = S.orbitFinset 1

@[simp]

theorem Finset.mem_closureFinset {G : Type u_1} [Group G] (S : Finset G) [Fintype G] [DecidableEq G] {g : G} : g ∈ S.closureFinset ↔ g ∈ Subgroup.closure ↑S

A group element lies in the computed finset Finset.closureFinset S exactly when it lies in the subgroup generated by S.

@[simp]

theorem Finset.coe_closureFinset {G : Type u_1} [Group G] (S : Finset G) [Fintype G] [DecidableEq G] : ↑S.closureFinset = ↑(Subgroup.closure ↑S)

The computed finset Finset.closureFinset S, as a set, is the subgroup generated by S.

@[simp]

theorem Finset.card_closureFinset {G : Type u_1} [Group G] (S : Finset G) [Fintype G] [DecidableEq G] : S.closureFinset.card = Nat.card ↥(Subgroup.closure ↑S)

The order of the subgroup generated by S, as the cardinality of a computed finset.