Documentation

TauCeti.GroupTheory.GroupAction.Free

Free actions #

A descent principle #

Let a monoid G act freely on X, and let E, P ⊆ G with 1 ∈ P be such that e * p ∈ P and e * p ≠ 1 for all e ∈ E and p ∈ P. Then a finite subset s ⊆ X in which every point is moved back into s by some element of E is empty: following such moves from a point of s, some point must return to itself under a product e * p ≠ 1, which freeness forbids.

Counting #

If a group G acts freely on X, every orbit is a copy of G, so Nat.card G divides Nat.card X.

Orbit decomposition #

Mathlib's MulAction.selfEquivOrbitsQuotientProd identifies X with the product of its orbit space and G; its inverse sends (q, g) to the translate g • q.out of the chosen representative.

Main results #

References #

This is the descent in the proof of Lemma 2 of A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327, §3, with G = PSL(2, ℤ), E = {T, T′} and P the classes of matrices with non-negative entries.

source
theorem MulAction.eq_empty_of_forall_exists_smul_mem {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] [IsCancelSMul G X] {E P : Set G} (hP : 1 ∈ P) (hE : ∀ e ∈ E, ∀ p ∈ P, e * p ∈ P ∧ e * p ≠ 1) {s : Finset X} (hs : ∀ x ∈ s, ∃ e ∈ E, e • x ∈ s) :
s = ∅

Descent for free actions. If G acts freely on X, 1 ∈ P, and e * p ∈ P with e * p ≠ 1 for all e ∈ E, p ∈ P, then a finite set s in which every point is moved back into s by an element of E is empty.

source
theorem MulAction.natCard_dvd_natCard_of_isCancelSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] :
Nat.card G ∣ Nat.card X

The order of a group acting freely divides the number of points: every orbit of a free action of G is a copy of G. No finiteness is needed, as Nat.card vanishes on infinite types, and a free action on a nonempty finite type is by a finite group.

source
@[simp]
theorem MulAction.selfEquivOrbitsQuotientProd'_symm_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {φ : orbitRel.Quotient G X → X} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : X), stabilizer G b = ⊥) (q : orbitRel.Quotient G X) (g : G) :
(selfEquivOrbitsQuotientProd' hφ h).symm (q, g) = g • φ q

For a free action, the inverse of the orbit decomposition selfEquivOrbitsQuotientProd' attached to a choice φ of orbit representatives sends (q, g) to g • φ q.

source
@[simp]
theorem AddAction.selfEquivOrbitsQuotientProd'_symm_apply {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] {φ : orbitRel.Quotient G X → X} (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : X), stabilizer G b = ⊥) (q : orbitRel.Quotient G X) (g : G) :
(selfEquivOrbitsQuotientProd' hφ h).symm (q, g) = g +ᵥ φ q

For a free additive action, the inverse of the orbit decomposition selfEquivOrbitsQuotientProd' attached to a choice φ of orbit representatives sends (q, g) to g +ᵥ φ q.

source
@[simp]
theorem MulAction.selfEquivOrbitsQuotientProd_symm_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (h : ∀ (b : X), stabilizer G b = ⊥) (q : orbitRel.Quotient G X) (g : G) :
(selfEquivOrbitsQuotientProd h).symm (q, g) = g • Quotient.out q

For a free action, the inverse of the orbit decomposition selfEquivOrbitsQuotientProd sends (q, g) to the translate g • q.out of the chosen representative of the orbit q.

source
@[simp]
theorem AddAction.selfEquivOrbitsQuotientProd_symm_apply {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] (h : ∀ (b : X), stabilizer G b = ⊥) (q : orbitRel.Quotient G X) (g : G) :
(selfEquivOrbitsQuotientProd h).symm (q, g) = g +ᵥ Quotient.out q

For a free additive action, the inverse of the orbit decomposition selfEquivOrbitsQuotientProd sends (q, g) to the translate g +ᵥ q.out of the chosen representative of the orbit q.